mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Core
USize.ofBitVec.injEq : ∀ (toBitVec toBitVec_1 : BitVec System.Platform.numBits),
  ({ toBitVec := toBitVec } = { toBitVec := toBitVec_1 }) = (toBitVec = toBitVec_1)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
/-- `GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
Defined as a subtype of matrices  -/
Matrix.termGL : Lean.ParserDescr
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.underlyingIso_arrow_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f]
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.underlyingIso f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.mk f).arrow h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.AlgebraicTopology.ModelCategory.PathObject
/-- A pre-path object for `A : C` is the data of a morphism
`ι : A ⟶ P` equipped with two retractions.  -/
HomotopicalAlgebra.PrepathObject : {C : Type u} → [CategoryTheory.Category.{v, u} C] → C → Type (max u v)
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.right_measure_le_of_levyProkhorovEDist_lt : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] {μ ν : MeasureTheory.Measure Ω}
  {c : ENNReal},
  MeasureTheory.levyProkhorovEDist μ ν < c → ∀ {B : Set Ω}, MeasurableSet B → ν B ≤ μ (Metric.thickening c.toReal B) + c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp], t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → (t₁ ∩ t₂).getKey! k = default
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_mulEquiv_refl : ∀ (R : Type u_4) [inst : Mul R] [inst_1 : Add R], ↑(RingEquiv.refl R) = MulEquiv.refl R
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.vadd_re : ∀ (x : ℝ) (z : UpperHalfPlane), (x +ᵥ z).re = x + z.re
-- Mathlib.Control.EquivFunctor
EquivFunctor.mapEquiv_symm : ∀ (f : Type u₀ → Type u₁) [inst : EquivFunctor f] {α β : Type u₀} (e : α ≃ β),
  (EquivFunctor.mapEquiv f e).symm = EquivFunctor.mapEquiv f e.symm
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coe_div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] (s t : Finset α), ↑(s / t) = ↑s / ↑t
-- Mathlib.Topology.Constructible
/-- **Alias** of the forward direction of `Topology.isConstructible_compl`. -/
Topology.IsConstructible.of_compl : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, Topology.IsConstructible sᶜ → Topology.IsConstructible s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.instFaithfulCompPre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) [F.Faithful], (CategoryTheory.StructuredArrow.pre S F G).Faithful
-- Mathlib.Order.WellFoundedSet
Set.isPWO_singleton : ∀ {α : Type u_2} [inst : Preorder α] (a : α), {a}.IsPWO
-- Mathlib.Topology.Instances.Matrix
HasSum.matrix_blockDiag' : ∀ {X : Type u_1} {l : Type u_3} {R : Type u_8} {m' : l → Type u_9} {n' : l → Type u_10} [inst : AddCommMonoid R]
  [inst_1 : TopologicalSpace R] {L : SummationFilter X} {f : X → Matrix ((i : l) × m' i) ((i : l) × n' i) R}
  {a : Matrix ((i : l) × m' i) ((i : l) × n' i) R}, HasSum f a L → HasSum (fun x => (f x).blockDiag') a.blockDiag' L
-- Mathlib.Algebra.Group.Hom.Basic
AddHom.add_apply : ∀ {M : Type u_8} {N : Type u_9} [inst : Add M] [inst_1 : AddCommSemigroup N] (f g : M →ₙ+ N) (x : M),
  (f + g) x = f x + g x
-- Mathlib.Algebra.Order.Group.Synonym
isAddRegular_toDual : ∀ {α : Type u_1} [inst : AddMonoid α] {a : α}, IsAddRegular (OrderDual.toDual a) ↔ IsAddRegular a
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below : {α : Type u} →
  [inst : Ord α] →
    {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop} →
      {β : α → Type v} → {a : Std.DTreeMap.Internal.Impl α β} → a.WF → Prop
-- Mathlib.Algebra.Lie.Basis.Basic
LieAlgebra.Basis.A_diag_eq_two : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [IsAddTorsionFree L] (i : ι), b.A i i = 2
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- The family of 2-morphisms out of the left Kan extension `f⁺ g`.  -/
CategoryTheory.Bicategory.lanDesc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] →
            (s : CategoryTheory.Bicategory.LeftExtension f g) → CategoryTheory.Bicategory.lan f g ⟶ s.extension
-- Init.Data.BitVec.Lemmas
BitVec.le_zero_iff : ∀ {w : ℕ} {x : BitVec w}, x ≤ 0#w ↔ x = 0#w
-- Init.Data.Range.Polymorphic.RangeIterator
Std.IterM.step.eq_1 : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] (it : Std.IterM m β),
  it.step = Std.Iterator.step it
-- Mathlib.Data.EReal.Operations
EReal.neg_le_neg_iff : ∀ {a b : EReal}, -a ≤ -b ↔ b ≤ a
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.isGroupLikeElem_single_one : ∀ {R : Type u_1} {A : Type u_3} {G : Type u_5} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Bialgebra R A]
  (g : G), IsGroupLikeElem R (MonoidAlgebra.single g 1)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_X_add_C : ∀ {R : Type u_2} [inst : CommRing R] [Nontrivial R] {ι : Type u_3} (m : MonomialOrder ι) (i : ι) (r : R),
  m.degree (MvPolynomial.X i + MvPolynomial.C r) = fun₀ | i => 1
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B C : Set E}, IsExtreme 𝕜 A C → B ⊆ A → C ⊆ B → IsExtreme 𝕜 B C
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.State.mk.injEq : ∀ (usedFVarsMap : Lean.Elab.Term.MutualClosure.UsedFVarsMap) (modified : Bool)
  (usedFVarsMap_1 : Lean.Elab.Term.MutualClosure.UsedFVarsMap) (modified_1 : Bool),
  ({ usedFVarsMap := usedFVarsMap, modified := modified } =
      { usedFVarsMap := usedFVarsMap_1, modified := modified_1 }) =
    (usedFVarsMap = usedFVarsMap_1 ∧ modified = modified_1)
-- Mathlib.Tactic.Push
/-- Common entry point to the implementation of `pull`.  -/
Mathlib.Tactic.Push.pullCore : Mathlib.Tactic.Push.Head → Lean.Expr → Option Lean.Meta.Simp.Discharge → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Geometry.Manifold.StructureGroupoid
mem_groupoid_of_pregroupoid : ∀ {H : Type u_1} [inst : TopologicalSpace H] {PG : Pregroupoid H} {e : OpenPartialHomeomorph H H},
  e ∈ PG.groupoid ↔ PG.property (↑e) e.source ∧ PG.property (↑e.symm) e.target
-- Mathlib.Algebra.Regular.Defs
IsRegular.mk : ∀ {R : Type u_1} [inst : Mul R] {c : R}, IsLeftRegular c → IsRightRegular c → IsRegular c
-- Mathlib.Computability.Partrec
Nat.Partrec.left : Nat.Partrec ↑fun n => (Nat.unpair n).1
-- Std.Data.HashMap.Basic
/-- Internal implementation detail of the hash map  -/
Std.HashMap.Equiv.inner : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β},
  m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.Computability.StateTransition
/-- Transitivity of `EvalsToInTime` in the sum of the numbers of steps.  -/
StateTransition.EvalsToInTime.trans : {σ : Type u_1} →
  (f : σ → Option σ) →
    (m₁ m₂ : ℕ) →
      (a b : σ) →
        (c : Option σ) →
          StateTransition.EvalsToInTime f a (some b) m₁ →
            StateTransition.EvalsToInTime f b c m₂ → StateTransition.EvalsToInTime f a c (m₂ + m₁)
-- Lean.Environment
_private.Lean.Environment.0.Lean.readModuleDataPartsOfMod.unsafe_1 : System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxc.Iterator.nodup_toList : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.Rxc.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  {it : Std.Iter α}, it.toList.Nodup
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsFlat.iInter : ∀ {α : Type u_2} {M : Matroid α} {ι : Type u_3} [Nonempty ι] {Fs : ι → Set α},
  (∀ (i : ι), M.IsFlat (Fs i)) → M.IsFlat (⋂ i, Fs i)
-- Std.Internal.Do.Triple.SpecLemmas
/-- An invariant combinator for `String` loops with early return, for the new `do` elaborator
which uses `Prod` for the state tuple: `onContinue` is the invariant while iterating, `onReturn`
holds once the loop returned early with a value.  -/
Std.Internal.Do.StringInvariant.withEarlyReturnNewDo : {s : String} →
  {β γ : Type u} →
    (Pred : Type u) →
      [Std.Internal.Do.Assertion Pred] →
        (s.Pos → β → Pred) → (γ → β → Pred) → Std.Internal.Do.StringInvariant s (Option γ × β) Pred
-- Lean.Elab.Tactic.Omega.Frontend
/-- The `omega` tactic, for resolving integer and natural linear arithmetic problems. This
`TacticM Unit` frontend with default configuration can be used as an Aesop rule, for example via
the tactic call `aesop (add 50% tactic Lean.Elab.Tactic.Omega.omegaDefault)`.  -/
Lean.Elab.Tactic.Omega.omegaDefault : Lean.Elab.Tactic.TacticM Unit
-- Std.Http.Data.Method
Std.Http.Method.get.sizeOf_spec : sizeOf Std.Http.Method.get = 1
-- Std.Tactic.Do.Syntax
/-- If `true` (the default), we will try to prove VCs via `mvcgen_trivial`, which is extensible
via `macro_rules`.
 -/
Lean.Elab.Tactic.Do.VCGen.Config.trivial : Lean.Elab.Tactic.Do.VCGen.Config → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Given two pairs of limit cones corresponding to the parenthesisations of `X × Y × Z`,
we obtain an isomorphism between the cone points.  -/
CategoryTheory.Limits.BinaryFan.associator : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      {sXY : CategoryTheory.Limits.BinaryFan X Y} →
        {sYZ : CategoryTheory.Limits.BinaryFan Y Z} →
          CategoryTheory.Limits.IsLimit sXY →
            CategoryTheory.Limits.IsLimit sYZ →
              {s : CategoryTheory.Limits.BinaryFan sXY.pt Z} →
                CategoryTheory.Limits.IsLimit s →
                  {t : CategoryTheory.Limits.BinaryFan X sYZ.pt} → CategoryTheory.Limits.IsLimit t → (s.pt ≅ t.pt)
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_5 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) (fvarId : Lean.FVarId) (idx : ℕ)
  (y : Lean.FVarId) (h : pu = Lean.Compiler.LCNF.Purity.impure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_5 fvarId idx y h
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
/-- See `Real.one_sub_inv_le_log_of_pos` for the stronger version when `x ≠ 0`.  -/
Real.neg_inv_le_log : ∀ {x : ℝ}, 0 ≤ x → -x⁻¹ ≤ Real.log x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.mono : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Fork f g}
  (hs : CategoryTheory.Limits.IsLimit s), CategoryTheory.Mono s.ι
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
/-- This is a version of `IncidenceAlgebra.prod_mul_prod` that works over non-commutative rings.  -/
IncidenceAlgebra.prod_mul_prod' : ∀ {𝕜 : Type u_2} {α : Type u_5} {β : Type u_6} [inst : Ring 𝕜] [inst_1 : Preorder α] [inst_2 : Preorder β]
  (f₁ f₂ : IncidenceAlgebra 𝕜 α) (g₁ g₂ : IncidenceAlgebra 𝕜 β) [inst_3 : LocallyFiniteOrder α]
  [inst_4 : LocallyFiniteOrder β] [inst_5 : DecidableLE (α × β)],
  (∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
      f₁ a₁ a₂ * g₁ b₁ b₂ * (f₂ a₂ a₃ * g₂ b₂ b₃) = f₁ a₁ a₂ * f₂ a₂ a₃ * (g₁ b₁ b₂ * g₂ b₂ b₃)) →
    f₁.prod g₁ * f₂.prod g₂ = (f₁ * f₂).prod (g₁ * g₂)
-- Mathlib.Probability.Process.Adapted
/-- A sequence of functions `u` is adapted to a filtration `f` if for all `i`,
`u i` is `f i`-measurable.

The definition known as `Adapted` before 2026-01-13 is now `StronglyAdapted`.  -/
MeasureTheory.Adapted : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] →
        {β : ι → Type u_3} →
          [(i : ι) → MeasurableSpace (β i)] → MeasureTheory.Filtration ι m → ((i : ι) → Ω → β i) → Prop
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_smul' : ∀ {β : Type u_2} {α : Type u_1} [inst : SMul β α] (b : Colex β) (a : α), ofColex b • a = b • a
-- Lean.CoreM
Lean.instInhabitedDeclNameGenerator.default : Lean.DeclNameGenerator
-- Mathlib.RingTheory.PowerSeries.Evaluation
/-- The domain of evaluation of `MvPowerSeries`, as an ideal  -/
PowerSeries.hasEvalIdeal : {S : Type u_2} →
  [inst : CommRing S] → [inst_1 : TopologicalSpace S] → [IsTopologicalRing S] → [IsLinearTopology S S] → Ideal S
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.cast_divConst : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.divConst B) = ↑(A / B).card / ↑A.card
-- Mathlib.Algebra.Torsor.Defs
Equiv.constSDiv.eq_1 : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [inst_1 : Torsor G P] (p : P),
  Equiv.constSDiv p = { toFun := fun x => p /ₛ x, invFun := fun x => x⁻¹ • p, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Data.Prod.Lex
/-- A type synonym to equip a type with its lexicographic order.  -/
Prod.Lex.«term_×ₗ_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Maps.Strict.Basic
/-- **Alias** of `Homeomorph.comp_isStrictMap_iff`.

---

Strict maps are preserved when postcomposing with a homeomorphism.  -/
Topology.Homeomorph.comp_isStrictMap_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : Y ≃ₜ Z) {f : X → Y}, Topology.IsStrictMap (⇑e ∘ f) ↔ Topology.IsStrictMap f
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.morphismProperty_eq_top : ∀ {V : SSet.Truncated 2} {W : CategoryTheory.MorphismProperty V.HomotopyCategory} [W.IsMultiplicative],
  (∀ {x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
      (e : SSet.Truncated.Edge x y), W (SSet.Truncated.HomotopyCategory.homMk e)) →
    W = ⊤
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.inductionOn₂ : ∀ {motive : Cardinal.{u_1} → Cardinal.{u_2} → Prop} (c₁ : Cardinal.{u_1}) (c₂ : Cardinal.{u_2}),
  (∀ (α : Type u_1) (β : Type u_2), motive (Cardinal.mk α) (Cardinal.mk β)) → motive c₁ c₂
-- Mathlib.Tactic.FunProp.FunctionData
/-- Domain type of `f`.  -/
Mathlib.Meta.FunProp.FunctionData.domainType : Mathlib.Meta.FunProp.FunctionData → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Subsemigroup.Defs
MulMemClass.mul_def : ∀ {M : Type u_1} {A : Type u_3} [inst : Mul M] [inst_1 : SetLike A M] [hA : MulMemClass A M] (S' : A) (x y : ↥S'),
  x * y = ⟨↑x * ↑y, ⋯⟩