mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.OpenSubgroup
/-- The product of two open subgroups as an open subgroup of the product group.  -/
OpenAddSubgroup.prod : {G : Type u_1} →
  [inst : AddGroup G] →
    [inst_1 : TopologicalSpace G] →
      {H : Type u_2} →
        [inst_2 : AddGroup H] →
          [inst_3 : TopologicalSpace H] → OpenAddSubgroup G → OpenAddSubgroup H → OpenAddSubgroup (G × H)
-- Mathlib.Data.Nat.Factorization.Divisors
Nat.coe_divisors_eq_prod_pow_le_factorization : ∀ {n : ℕ}, n ≠ 0 → ↑n.divisors = {x | ∃ f ≤ n.factorization, (f.prod fun x1 x2 => x1 ^ x2) = x}
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.commRingEquiv_single_zero_single : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : AddMonoid M] [inst_2 : AddMonoid N]
  (m : M),
  AddMonoidAlgebra.commRingEquiv (AddMonoidAlgebra.single 0 (AddMonoidAlgebra.single m 1)) = AddMonoidAlgebra.single m 1
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ici_erase : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : DecidableEq α] (a : α),
  (Finset.Ici a).erase a = Finset.Ioi a
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] [inst_3 : SizeOf C] (X : C) [ringObj : CategoryTheory.RingObj X],
  sizeOf { X := X, ringObj := ringObj } = 1 + sizeOf X + sizeOf ringObj
-- Init.Data.Order.Lemmas
Std.Total.asymm_of_total_not : ∀ {α : Sort u_1} {r : α → α → Prop} [i : Std.Total fun x1 x2 => ¬r x1 x2], Std.Asymm r
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k k' : α) (f : Option (β k) → Option (β k))
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast? k' (Std.Internal.List.alterKey k f l) =
      if h : (k == k') = true then cast ⋯ (f (Std.Internal.List.getValueCast? k l))
      else Std.Internal.List.getValueCast? k' l
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Measure.integral_compProd : ∀ {α : Type u_5} {β : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] [ProbabilityTheory.IsSFiniteKernel κ] {E : Type u_8}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : α × β → E},
  MeasureTheory.Integrable f (μ.compProd κ) → ∫ (x : α × β), f x ∂μ.compProd κ = ∫ (a : α), ∫ (b : β), f (a, b) ∂κ a ∂μ
-- Init.Data.Ord.Basic
List.compareLex_cons_nil : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {xs : List α}, List.compareLex cmp (x :: xs) [] = Ordering.gt
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- Easy inclusion: a differentiability point with derivative in `K` belongs to `D f K`.  -/
RightDerivMeasurableAux.differentiable_set_subset_D : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {f : ℝ → F} (K : Set F),
  {x | DifferentiableWithinAt ℝ f (Set.Ici x) x ∧ derivWithin f (Set.Ici x) x ∈ K} ⊆ RightDerivMeasurableAux.D f K
-- Mathlib.Data.Set.Lattice
Set.union_distrib_iInter_right : ∀ {α : Type u_1} {ι : Sort u_5} (s : ι → Set α) (t : Set α), (⋂ i, s i) ∪ t = ⋂ i, s i ∪ t
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin_map : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E) {E' : Type u_3}
  [inst_3 : Field E'] [inst_4 : Algebra F E'] (f : E →ₐ[F] E'),
  IntermediateField.map f (IntermediateField.adjoin F S) = IntermediateField.adjoin F (⇑f '' S)
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instLawfulEqOrdOrdinal : Std.LawfulEqOrd Std.Time.Nanosecond.Ordinal
-- Mathlib.Algebra.Order.GroupWithZero.Basic
sq_le_one_iff₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀}
  [ZeroLEOneClass M₀], 0 ≤ a → (a ^ 2 ≤ 1 ↔ a ≤ 1)
-- Mathlib.Data.Int.GCD
/-- Helper function for the extended GCD algorithm (`Nat.xgcd`).  -/
Nat.xgcdAux : ℕ → ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ
-- Mathlib.Topology.MetricSpace.HolderNorm
nnHolderNorm_zero : ∀ (X : Type u_1) {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] [inst_2 : Zero Y]
  (r : NNReal), nnHolderNorm r 0 = 0
-- Mathlib.Data.List.Sort
/-- **Alias** of the forward direction of `List.sortedLE_iff_pairwise`. -/
List.SortedLE.pairwise : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLE → List.Pairwise (fun x1 x2 => x1 ≤ x2) l
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- If P is a localization of R, invertible R-submodules of P are all fractional
(expressed as an isomorphism of groups).  -/
FractionalIdeal.unitsMulEquivSubmodule : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] → [IsLocalization S P] → (FractionalIdeal S P)ˣ ≃* (Submodule R P)ˣ
-- Init.Data.Vector.Range
Vector.map_snd_add_zipIdx_eq_zipIdx : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {m k : ℕ},
  Vector.map (Prod.map id fun x => x + m) (xs.zipIdx k) = xs.zipIdx (m + k)
-- Mathlib.Geometry.Euclidean.SignedDist
signedDist_vadd_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (v w : V) (p q : P),
  ((signedDist v) p) (w +ᵥ q) = inner ℝ (NormedSpace.normalize v) w + ((signedDist v) p) q
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- The matrix `vecMulVec a (star a)` is always positive semi-definite.  -/
Matrix.posSemidef_vecMulVec_self_star : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [Finite n]
  [StarOrderedRing R] (a : n → R), (Matrix.vecMulVec a (star a)).PosSemidef
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.lt : ∀ {p q r : NNReal}, p.HolderTriple q r → r < p
-- Mathlib.Order.RelIso.Basic
/-- Two relations on empty types are isomorphic.  -/
RelIso.relIsoOfIsEmpty : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop) → (s : β → β → Prop) → [IsEmpty α] → [IsEmpty β] → r ≃r s
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.instWeakEquivalenceOppositeOp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] [HomotopicalAlgebra.WeakEquivalence f],
  HomotopicalAlgebra.WeakEquivalence f.op
-- Std.Http.Data.URI.Basic
/-- Appends a single segment to the path. The segment will be percent-encoded.
 -/
Std.Http.URI.Path.append : Std.Http.URI.Path → String → Std.Http.URI.Path
-- Init.Data.UInt.Lemmas
UInt16.toUSize_eq_mod_65536_iff : ∀ (a : UInt16) (b : USize), a.toUSize = b % 65536 ↔ a = b.toUInt16
-- Init.Data.BitVec.Lemmas
BitVec.msb_eq_decide : ∀ {w : ℕ} (x : BitVec w), x.msb = decide (2 ^ (w - 1) ≤ x.toNat)
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Presieve.FactorsThru.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} (S T : CategoryTheory.Presieve X),
  S.FactorsThru T = ∀ ⦃Z : C⦄ ⦃g : Z ⟶ X⦄, S g → ∃ W i e, T e ∧ CategoryTheory.CategoryStruct.comp i e = g
-- Mathlib.RingTheory.Jacobson.Ideal
/-- A ring `R` is local if and only if its Jacobson radical is maximal  -/
Ideal.IsLocal.out : ∀ {R : Type u} {inst : CommRing R} {I : Ideal R} [self : I.IsLocal], I.jacobson.IsMaximal
-- Std.Async.UDP
/-- Sets the TTL for outgoing packets.
 -/
Std.Async.UDP.Socket.setTTL : Std.Async.UDP.Socket → UInt32 → IO Unit
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Composing a formal multilinear series with an ordered partition extended by adding a left point
to an already existing atom of index `i` corresponds to updating the `i`th block,
using `p (c.partSize i + 1)` instead of `p (c.partSize i)` there.
This is one of the terms that appears when differentiating in the Faa di Bruno
formula, going from step `m` to step `m + 1`.  -/
_private.Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno.0.faaDiBruno_aux2 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {m : ℕ} (q : FormalMultilinearSeries 𝕜 F G)
  (p : FormalMultilinearSeries 𝕜 E F) (c : OrderedFinpartition m) (i : Fin c.length),
  (q.compAlongOrderedFinpartition p (c.extend (some i))).curryLeft =
    ((OrderedFinpartition.compAlongOrderedFinpartitionL 𝕜 E F G c) (q c.length)).toContinuousLinearMap
        (fun i => p (c.partSize i)) i ∘SL
      (p (c.partSize i + 1)).curryLeft
-- Mathlib.Algebra.Category.Grp.Yoneda
CommGrpCat.coyonedaForget_inv_app_app_hom_apply : ∀ (X : CommGrpCatᵒᵖ) (X_1 : CommGrpCat) (f : Opposite.unop X ⟶ X_1),
  (CategoryTheory.ConcreteCategory.hom ((CommGrpCat.coyonedaForget.inv.app X).app X_1)) f = CommGrpCat.Hom.hom f
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The forgetful functor from `𝒪ₓ`-modules to presheaves of modules is fully faithful.  -/
AlgebraicGeometry.Scheme.Modules.fullyFaithfulToPresheafOfModules : {X : AlgebraicGeometry.Scheme} → (AlgebraicGeometry.Scheme.Modules.toPresheafOfModules X).FullyFaithful
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat
QuadraticModuleCat.Hom.mk.inj : ∀ {R : Type u} {inst : CommRing R} {V W : QuadraticModuleCat R} {toIsometry' toIsometry'_1 : V.form →qᵢ W.form},
  { toIsometry' := toIsometry' } = { toIsometry' := toIsometry'_1 } → toIsometry' = toIsometry'_1
-- Mathlib.CategoryTheory.Comma.CardinalArrow
/-- The bijection `Arrow (Shrink C) ≃ Arrow C`.  -/
CategoryTheory.Arrow.shrinkEquiv : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : Small.{w, u} C] → CategoryTheory.Arrow (Shrink.{w, u} C) ≃ CategoryTheory.Arrow C
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The `ℤ`-linear map induced by precomposing with `CC'₁`  -/
Profinite.NobelingProof.Linear_CC'₁ : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} →
          Profinite.NobelingProof.contained C (Order.succ o) →
            (ho : o < Ordinal.type fun x1 x2 => x1 < x2) →
              LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `HasFDerivAtFilter.sub` -/
HasFDerivAtFilter.fun_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F}
  {f' g' : E →L[𝕜] F} {L : Filter (E × E)},
  HasFDerivAtFilter f f' L → HasFDerivAtFilter g g' L → HasFDerivAtFilter (fun i => f i - g i) (f' - g') L
-- Mathlib.Algebra.Lie.NonUnitalNonAssocAlgebra
/-- Regarding the `LieRing` of a `LieAlgebra` as a `NonUnitalNonAssocRing`, we can
regard a `LieHom` as a `NonUnitalAlgHom`.  -/
LieHom.toNonUnitalAlgHom : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {L₂ : Type w} →
            [inst_3 : LieRing L₂] →
              [inst_4 : LieAlgebra R L₂] → (L →ₗ⁅R⁆ L₂) → CommutatorRing L →ₙₐ[R] CommutatorRing L₂
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instInfFiniteIndexNormalSubgroup.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  FiniteIndexNormalSubgroup.instInfFiniteIndexNormalSubgroup =
    {
      min := fun U V =>
        let __Subgroup := U.toSubgroup ⊓ V.toSubgroup;
        { toSubgroup := __Subgroup, isNormal' := ⋯, isFiniteIndex' := ⋯ } }
-- Mathlib.Algebra.Group.Ext
CommGroup.ext : ∀ {G : Type u_1} ⦃g₁ g₂ : CommGroup G⦄, HMul.hMul = HMul.hMul → g₁ = g₂
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.coe_symm_comp_coe : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), (↑e.symm).comp ↑e = ContinuousAlgHom.id R A
-- Mathlib.Order.UpperLower.Closure
lowerClosure_univ : ∀ {α : Type u_1} [inst : Preorder α], lowerClosure Set.univ = ⊤
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves finite limits, then `F.unop : C ⥤ D` preserves finite
colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.PreservesFiniteLimits F],
  CategoryTheory.Limits.PreservesFiniteColimits F.unop
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
toWeakSpaceCLM_eq_toWeakSpace : ∀ (𝕜 : Type u_2) (E : Type u_4) [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x : E), (toWeakSpaceCLM 𝕜 E) x = (toWeakSpace 𝕜 E) x
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.eval_same : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {e : ι → M} {ε : ι → Module.Dual R M}, Module.DualBases e ε → ∀ (i : ι), (ε i) (e i) = 1
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : SizeOf α] [inst_3 : SizeOf β]
  (inner : Std.ExtDHashMap α fun x => β), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Data.Multiset.AddSub
Multiset.add_sub_cancel : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, t ≤ s → s - t + t = s
-- Mathlib.Analysis.Normed.Group.Uniform
dist_sub_sub_le : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E), dist (a₁ - a₂) (b₁ - b₂) ≤ dist a₁ b₁ + dist a₂ b₂
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Preimage of a subalgebra under an algebra homomorphism.  -/
Subalgebra.comap : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → Subalgebra R B → Subalgebra R A
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.instSub : Sub Lean.Omega.LinearCombo
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.eq_2 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none),
  (match some none with
    | some (some c) => h_1 c
    | some none => h_2 ()
    | none => h_3 ()) =
    h_2 ()
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.inv_apply : ∀ (G : Type v) [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G] (a : G), (IsometryEquiv.inv G) a = a⁻¹
-- Mathlib.Analysis.BoxIntegral.Box.SubboxInduction
BoxIntegral.Box.injective_splitCenterBox : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), Function.Injective I.splitCenterBox
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.comp_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {V W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.prod.lift g h) =
    CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.compl : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β}, e.IsImage s t → e.IsImage sᶜ tᶜ
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsPrenex.brecOn : ∀ {L : FirstOrder.Language} {α : Type u'} {motive : {n : ℕ} → (a : L.BoundedFormula α n) → a.IsPrenex → Prop} {n : ℕ}
  {a : L.BoundedFormula α n} (t : a.IsPrenex),
  (∀ {n : ℕ} (a : L.BoundedFormula α n) (t : a.IsPrenex),
      FirstOrder.Language.BoundedFormula.IsPrenex.below t → motive a t) →
    motive a t
-- Mathlib.Data.Ordmap.Invariants
Ordnode.eraseMin.eq_2 : ∀ {α : Type u_1} (size : ℕ) (x_1 : α) (r : Ordnode α), (Ordnode.node size Ordnode.nil x_1 r).eraseMin = r
-- Mathlib.Algebra.Category.FGModuleCat.Basic
FGModuleCat.instFiniteCarrier : ∀ (R : Type u) [inst : Ring R] (V : FGModuleCat R), Module.Finite R ↑V
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.splitter : (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) →
  (op : Std.Tactic.BVDecide.BVBinOp) →
    (Unit → motive Std.Tactic.BVDecide.BVBinOp.and) →
      (Unit → motive Std.Tactic.BVDecide.BVBinOp.or) →
        (Unit → motive Std.Tactic.BVDecide.BVBinOp.xor) →
          (Unit → motive Std.Tactic.BVDecide.BVBinOp.add) →
            (Unit → motive Std.Tactic.BVDecide.BVBinOp.mul) →
              (Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) →
                (Unit → motive Std.Tactic.BVDecide.BVBinOp.umod) → motive op
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.id_comp : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S), (MulSemiringActionHom.id N).comp f = f
-- Init.Grind.Config
/-- If `markInstances` is `true`, E-matching proofs are marked with instance IDs
for precise tracking of which theorems appear in the final proof.  -/
Lean.Grind.Config.markInstances : Lean.Grind.Config → Bool
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instInv.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Inv β],
  MeasureTheory.SimpleFunc.instInv = { inv := fun f => MeasureTheory.SimpleFunc.map Inv.inv f }
-- Init.Data.UInt.Bitwise
UInt8.or_neg_one : ∀ {a : UInt8}, a ||| -1 = -1
-- Mathlib.RingTheory.Finiteness.Defs
AddMonoid.FG.to_moduleFinite_int : ∀ {G : Type u_6} [inst : AddCommGroup G] [AddMonoid.FG G], Module.Finite ℤ G
-- Mathlib.Topology.Algebra.Support
mulTSupport_comp_eq : ∀ {X : Type u_1} {α : Type u_2} {β : Type u_4} [inst : One α] [inst_1 : TopologicalSpace X] [inst_2 : One β]
  {g : α → β}, (∀ {x : α}, g x = 1 ↔ x = 1) → ∀ (f : X → α), mulTSupport (g ∘ f) = mulTSupport f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_ric_succ_eq_append : ∀ {n : ℕ}, (*...=n + 1).toList = (*...=n).toList ++ [n + 1]
-- Init.Data.String.Basic
String.Slice.Pos.offset_ofSliceFrom : ∀ {s : String.Slice} {p₀ : s.Pos} {pos : (s.sliceFrom p₀).Pos},
  (String.Slice.Pos.ofSliceFrom pos).offset = pos.offset.offsetBy p₀.offset
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.symm_trans : ∀ {X Y : TopPair} {f₀ f₁ f₂ : X ⟶ Y} (F : TopPair.Homotopy f₀ f₁) (G : TopPair.Homotopy f₁ f₂),
  (F.trans G).symm = G.symm.trans F.symm
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_add : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Add β] (f g : MeasureTheory.SimpleFunc α β),
  ⇑(f + g) = ⇑f + ⇑g
-- Aesop.Forward.Match
/-- Fold over the hypotheses contained in a match.  -/
Aesop.ForwardRuleMatch.foldHyps : {σ : Type u_1} → (σ → Lean.FVarId → σ) → σ → Aesop.ForwardRuleMatch → σ
-- Lean.Declaration
Lean.InductiveVal.mk.sizeOf_spec : ∀ (toConstantVal : Lean.ConstantVal) (numParams numIndices : ℕ) (all ctors : List Lean.Name) (numNested : ℕ)
  (isRec isUnsafe isReflexive : Bool),
  sizeOf
      { toConstantVal := toConstantVal, numParams := numParams, numIndices := numIndices, all := all, ctors := ctors,
        numNested := numNested, isRec := isRec, isUnsafe := isUnsafe, isReflexive := isReflexive } =
    1 + sizeOf toConstantVal + sizeOf numParams + sizeOf numIndices + sizeOf all + sizeOf ctors + sizeOf numNested +
          sizeOf isRec +
        sizeOf isUnsafe +
      sizeOf isReflexive
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
/-- `G` is `IsCompleteMultipartite` iff non-adjacency is transitive  -/
SimpleGraph.IsCompleteMultipartite : {α : Type u} → SimpleGraph α → Prop
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqLambdaTheoremArgs.beq : Mathlib.Meta.FunProp.LambdaTheoremArgs → Mathlib.Meta.FunProp.LambdaTheoremArgs → Bool
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.eraseMin.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (Unit → motive Ordnode.nil) →
        ((size : ℕ) → (x : α) → (r : Ordnode α) → motive (Ordnode.node size Ordnode.nil x r)) →
          ((size sz : ℕ) →
              (l' : Ordnode α) →
                (y : α) →
                  (r' : Ordnode α) →
                    (x : α) → (r : Ordnode α) → motive (Ordnode.node size (Ordnode.node sz l' y r') x r)) →
            motive x
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_atom_pf : ∀ {α : Type u_1} [inst : AddCommMonoid α] (x x' : α), x = x' → x = Mathlib.Tactic.Abel.term 1 x' 0
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_add_natCast : ∀ {x : ℝ}, x ≠ 0 → ∀ (y : ℝ) (n : ℕ), x ^ (y + ↑n) = x ^ y * x ^ n
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.toQ_le : ∀ {α : Type u} [inst : Lean.Grind.NatModule α] [inst_1 : LE α] [inst_2 : Std.IsPreorder α]
  [inst_3 : Lean.Grind.OrderedAdd α] {a b : α},
  Lean.Grind.IntModule.OfNatModule.toQ a ≤ Lean.Grind.IntModule.OfNatModule.toQ b ↔ a ≤ b
-- Init.Data.Nat.Basic
Nat.le_of_eq : ∀ {n m : ℕ}, n = m → n ≤ m
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
Measurable.indicator : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {m : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : Zero β], Measurable f → MeasurableSet s → Measurable (s.indicator f)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.mk.inj : ∀ {R : Type u} {L : Type v} {M : Type w} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : AddCommGroup M}
  {inst_3 : Module R M} {inst_4 : LieRingModule L M} {toSubmodule : Submodule R M}
  {lie_mem : ∀ {x : L} {m : M}, m ∈ toSubmodule.carrier → ⁅x, m⁆ ∈ toSubmodule.carrier} {toSubmodule_1 : Submodule R M}
  {lie_mem_1 : ∀ {x : L} {m : M}, m ∈ toSubmodule_1.carrier → ⁅x, m⁆ ∈ toSubmodule_1.carrier},
  { toSubmodule := toSubmodule, lie_mem := lie_mem } = { toSubmodule := toSubmodule_1, lie_mem := lie_mem_1 } →
    toSubmodule = toSubmodule_1
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_single_mul_eq_image : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] [inst_2 : DecidableEq G] (f : AddMonoidAlgebra k G)
  {r : k},
  (∀ (y : k), r * y = 0 ↔ y = 0) →
    ∀ {x : G},
      IsAddLeftRegular x →
        (AddMonoidAlgebra.single x r * f).coeff.support = Finset.image (fun x_1 => x + x_1) f.coeff.support
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- This left homology map data expresses compatibilities of the left homology data
constructed by `LeftHomologyData.ofEpiOfIsIsoOfMono'`  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (h : S₂.LeftHomologyData) →
            [inst_2 : CategoryTheory.Epi φ.τ₁] →
              [inst_3 : CategoryTheory.IsIso φ.τ₂] →
                [inst_4 : CategoryTheory.Mono φ.τ₃] →
                  CategoryTheory.ShortComplex.LeftHomologyMapData φ
                    (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' φ h) h