mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Algebra.SMul
Prod.contMDiffSMul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {H' : Type u_4}
  [inst_4 : TopologicalSpace H'] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {H'' : Type u_6} [inst_7 : TopologicalSpace H''] {E'' : Type u_7}
  [inst_8 : NormedAddCommGroup E''] [inst_9 : NormedSpace 𝕜 E''] {I'' : ModelWithCorners 𝕜 E'' H''} {G : Type u_8}
  [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H G] {M : Type u_9} [inst_12 : TopologicalSpace M]
  [inst_13 : ChartedSpace H' M] {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace H'' N]
  [inst_16 : SMul G M] [inst_17 : SMul G N] {n : WithTop ℕ∞} [ContMDiffSMul I I' n G M] [ContMDiffSMul I I'' n G N],
  ContMDiffSMul I (I'.prod I'') n G (M × N)
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_empty_left_iff : ∀ {s : String} {p : s.Pos} {t : String}, p.Splits "" t ↔ p = s.startPos ∧ t = s
-- Mathlib.Data.Set.Function
Set.MapsTo.union_union : ∀ {α : Type u_1} {β : Type u_2} {s₁ s₂ : Set α} {t₁ t₂ : Set β} {f : α → β},
  Set.MapsTo f s₁ t₁ → Set.MapsTo f s₂ t₂ → Set.MapsTo f (s₁ ∪ s₂) (t₁ ∪ t₂)
-- Std.Data.DTreeMap.Raw.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.DTreeMap.Raw.toList : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → List ((a : α) × β a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblX_smul : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R) (u : R),
  W'.dblX (u • P) = (u ^ 4) ^ 2 * W'.dblX P
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- A continuous linear endomorphism `T` of a Hilbert space is **positive** if it is symmetric
and `∀ x, 0 ≤ re ⟪T x, x⟫`.  -/
ContinuousLinearMap.IsPositive : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → (E →L[𝕜] E) → Prop
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminormClass.toNonarchimedeanHomClass : ∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : AddGroup α} {inst_1 : FunLike F α ℝ}
  [self : NonarchAddGroupSeminormClass F α], NonarchimedeanHomClass F α ℝ
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.Cover.mem_propQCTopology : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S)
  [AlgebraicGeometry.QuasiCompactCover 𝒰.toPreZeroHypercover],
  CategoryTheory.Sieve.ofArrows 𝒰.X 𝒰.f ∈ (AlgebraicGeometry.Scheme.propQCTopology P) S
-- Std.Http.Data.Headers
Std.Http.instDecidableMemNameHeaders : (name : Std.Http.Header.Name) → (h : Std.Http.Headers) → Decidable (name ∈ h)
-- Mathlib.Topology.Category.TopCat.ULift
TopCat.instPreservesLimitsOfSizeUliftFunctor : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} TopCat.uliftFunctor
-- Std.Data.DHashMap.Raw
Std.DHashMap.Raw.WF.containsThenInsertIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {a : α} {b : β a},
  m.WF → (m.containsThenInsertIfNew a b).2.WF
-- Lean.LocalContext
Lean.instMonadLCtxOfMonadLift : {m n : Type → Type} → [MonadLift m n] → [Lean.MonadLCtx m] → Lean.MonadLCtx n
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- The descent of the identity morphism is homotopic to the identity cochain map.  -/
CategoryTheory.InjectiveResolution.descIdHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      (X : C) →
        (I : CategoryTheory.InjectiveResolution X) →
          Homotopy (CategoryTheory.InjectiveResolution.desc (CategoryTheory.CategoryStruct.id X) I I)
            (CategoryTheory.CategoryStruct.id I.cocomplex)
-- Aesop.Builder.Basic
/-- The transparency used by the rule tactic.  -/
Aesop.RuleBuilderOptions.transparency? : Aesop.RuleBuilderOptions → Option Lean.Meta.TransparencyMode
-- Mathlib.Combinatorics.Hindman
/-- Semigroup structure on `Ultrafilter M` induced by a semigroup structure on `M`.  -/
Ultrafilter.semigroup : {M : Type u_1} → [Semigroup M] → Semigroup (Ultrafilter M)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
/-- The inner product between a multiple of a `π / 2` rotation of a vector and a multiple of
that vector is zero.  -/
Orientation.inner_smul_rotation_pi_div_two_smul_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) (r₁ r₂ : ℝ), inner ℝ (r₁ • (o.rotation ↑(Real.pi / 2)) x) (r₂ • x) = 0
-- Mathlib.AlgebraicTopology.DoldKan.EquivalenceAdditive
CategoryTheory.Preadditive.DoldKan.N.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.Preadditive.DoldKan.N = AlgebraicTopology.DoldKan.N₂
-- Lean.Expr
Lean.Expr.Data.hasFVar : Lean.Expr.Data → Bool
-- Mathlib.Algebra.Algebra.Field
algebraMap.coe_zpow : ∀ {R : Type u_1} (A : Type u_2) [inst : Semifield R] [inst_1 : DivisionSemiring A] [inst_2 : Algebra R A] (r : R)
  (z : ℤ), ↑(r ^ z) = ↑r ^ z
-- Mathlib.Algebra.Order.AddTorsor
IsOrderedSMul.smul_le_smul : ∀ {G : Type u_1} {P : Type u_2} [inst : LE G] [inst_1 : Preorder P] [inst_2 : SMul G P] [IsOrderedSMul G P] {a b : G}
  {c d : P}, a ≤ b → c ≤ d → a • c ≤ b • d
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₁.brecOn.eq : ∀ {motive : Mathlib.Tactic.BicategoryLike.Mor₁ → Sort u} (t : Mathlib.Tactic.BicategoryLike.Mor₁)
  (F_1 : (t : Mathlib.Tactic.BicategoryLike.Mor₁) → Mathlib.Tactic.BicategoryLike.Mor₁.below t → motive t),
  Mathlib.Tactic.BicategoryLike.Mor₁.brecOn t F_1 = F_1 t (Mathlib.Tactic.BicategoryLike.Mor₁.brecOn.go t F_1).2
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_smul_ball : ∀ {G : Type v} {X : Type w} [inst : PseudoMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ℝ), (fun x => c • x) ⁻¹' Metric.ball x r = Metric.ball (c⁻¹ • x) r
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
/-- A vector field on a vector space is `C^n` in the manifold sense iff it is `C^n` in the vector
space sense.  -/
contMDiffWithinAt_vectorSpace_iff_contDiffWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V : (x : E) → TangentSpace (modelWithCornersSelf 𝕜 E) x} {s : Set E} {x : E},
  ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E).tangent n (fun x => ⟨x, V x⟩) s x ↔
    ContDiffWithinAt 𝕜 n V s x
-- Mathlib.Topology.UniformSpace.UniformConvergence
TendstoUniformlyOnFilter.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] (F : ι → α → β) (f : α → β) (p : Filter ι)
  (p' : Filter α),
  TendstoUniformlyOnFilter F f p p' = ∀ u ∈ uniformity β, ∀ᶠ (n : ι × α) in p ×ˢ p', (f n.2, F n.1 n.2) ∈ u
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.functorIsoMk'_inv_app_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} {mor₁ : obj₁ ⟶ obj₂}
  {mor₂ : obj₂ ⟶ obj₃} {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)}
  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} {mor₁' : obj₁' ⟶ obj₂'} {mor₂' : obj₂' ⟶ obj₃'}
  {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} (iso₁ : obj₁ ≅ obj₁') (iso₂ : obj₂ ≅ obj₂')
  (iso₃ : obj₃ ≅ obj₃')
  (comm₁ : CategoryTheory.CategoryStruct.comp mor₁ iso₂.hom = CategoryTheory.CategoryStruct.comp iso₁.hom mor₁')
  (comm₂ : CategoryTheory.CategoryStruct.comp mor₂ iso₃.hom = CategoryTheory.CategoryStruct.comp iso₂.hom mor₂')
  (comm₃ :
    CategoryTheory.CategoryStruct.comp mor₃
        (CategoryTheory.Functor.whiskerRight iso₁.hom (CategoryTheory.shiftFunctor C 1)) =
      CategoryTheory.CategoryStruct.comp iso₃.hom mor₃')
  (j : J),
  ((CategoryTheory.Pretriangulated.Triangle.functorIsoMk' iso₁ iso₂ iso₃ comm₁ comm₂ comm₃).inv.app j).hom₂ =
    iso₂.inv.app j
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokensOptions : Lean.ToJson Lean.Lsp.SemanticTokensOptions
-- Init.Meta.Defs
Lean.Meta.instReprConfig_1.repr : Lean.Meta.Simp.Config → ℕ → Std.Format
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq : ∀ {f g : ℝ → ℝ},
  f =ᶠ[Filter.atTop] g → (AkraBazziRecurrence.GrowsPolynomially f ↔ AkraBazziRecurrence.GrowsPolynomially g)
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- **Alias** of `Metric.Snowflaking.image_toSnowflaking_eball`. -/
Metric.Snowflaking.image_toSnowflaking_emetricBall : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1} [inst : PseudoEMetricSpace X] (x : X) (r : ENNReal),
  ⇑Metric.Snowflaking.toSnowflaking '' Metric.eball x r = Metric.eball (Metric.Snowflaking.toSnowflaking x) (r ^ α)
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.and'.sizeOf_spec : ∀ (a : Mathlib.Tactic.ITauto.AndKind) (a_1 a_2 : Mathlib.Tactic.ITauto.IProp),
  sizeOf (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2) = 1 + sizeOf a + sizeOf a_1 + sizeOf a_2
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.Partial.exists_isMax : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : IsOrderedRing K] [inst_3 : Archimedean K]
  {M : Type u_2} [inst_4 : AddCommGroup M] [inst_5 : LinearOrder M] [inst_6 : IsOrderedAddMonoid M]
  [inst_7 : Module K M] [inst_8 : IsOrderedModule K M] {R : Type u_3} [inst_9 : AddCommGroup R]
  [inst_10 : LinearOrder R] [inst_11 : Module K R] (seed : HahnEmbedding.Seed K M R) [IsOrderedAddMonoid R],
  ∃ f, IsMax f
-- Mathlib.Algebra.Group.TransferInstance
/-- For many type classes, we have a definition that lets us transfer instances from one type to another
using an equivalence, such as `Equiv.mul` for `Mul`.
Constructing data instances in this way is discouraged because the resulting data is inefficient
to unfold. To somewhat mitigate this problem, in these definitions we don't write the
projections on `Equiv` in the usual way using `Equiv.symm` and `DFunLike.coe`, and instead use
`Equiv.toFun` and `Equiv.invFun` directly. As a result, unification has to do less unfolding.

Note also that when constructing data instances in this way, it usually helps to use
`fast_instance%` to get a faster instance.
 -/
LibraryNote.instance_transfer_via_equivalence : Batteries.Util.LibraryNote
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc_castSucc : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (i : Fin n),
  Fin.snoc p x i.castSucc = p i
-- Init.Data.List.Int.Sum
List.sum_replicate_int : ∀ {n : ℕ} {a : ℤ}, (List.replicate n a).sum = ↑n * a
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.symm_smul : ∀ {S : Type u_1} {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : Module S V]
  [inst_6 : ContinuousConstSMul S V] [inst_7 : AddCommMonoid W] [inst_8 : Module R W] [inst_9 : TopologicalSpace W]
  [inst_10 : Module S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : SMulCommClass R S W] [inst_13 : SMul S R]
  [inst_14 : IsScalarTower S R V] [inst_15 : IsScalarTower S R W] [inst_16 : SMulCommClass R S V] (e : V ≃L[R] W)
  (α : Sˣ), (α • e).symm = α⁻¹ • e.symm
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isEmpty_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {l : List (α × β)}, (Std.ExtDTreeMap.Const.insertMany t l).isEmpty = (t.isEmpty && l.isEmpty)
-- Mathlib.Topology.Algebra.AsymptoticCone
asymptoticCone_eq_closure_of_forall_smul_mem : ∀ {k : Type u_1} {V : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : TopologicalSpace V] [inst_5 : TopologicalSpace k] [OrderTopology k]
  [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V] {s : Set V},
  (∀ (c : k), 0 < c → ∀ x ∈ s, c • x ∈ s) → asymptoticCone k s = closure s
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.rank_le_iff_subset : ∀ {x y : ZFSet.{u_1}}, x.IsOrdinal → y.IsOrdinal → (x.rank ≤ y.rank ↔ x ⊆ y)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_union' : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} {G : Type u_2} [inst : AddCommMonoid G]
  {m : MeasureTheory.AddContent G C}, s ∈ C → t ∈ C → s ∪ t ∈ C → Disjoint s t → m (s ∪ t) = m s + m t
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_eq_one : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {x : Monoid.Coprod M N},
  (Monoid.Coprod.swap M N) x = 1 ↔ x = 1
-- Mathlib.Order.WellFoundedSet
Set.IsWF.union : ∀ {α : Type u_2} [inst : Preorder α] {s t : Set α}, s.IsWF → t.IsWF → (s ∪ t).IsWF
-- Init.Control.Lawful.Basic
Id.pure_run : ∀ {α : Type u_1} (a : Id α), pure a.run = a
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- The weighted degree of a weighted homogeneous polynomial controls its support.  -/
MvPolynomial.IsWeightedHomogeneous.coeff_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] {φ : MvPolynomial σ R}
  {n : M} {w : σ → M},
  MvPolynomial.IsWeightedHomogeneous w φ n → ∀ (d : σ →₀ ℕ), (Finsupp.weight w) d ≠ n → MvPolynomial.coeff d φ = 0
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.anchor : Lean.Meta.Grind.SplitCandidateWithAnchor → UInt64
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKeyD_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).getKeyD k fallback =
      if (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true then k else fallback
-- Mathlib.Data.Sign.Defs
sign_nonpos_iff : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : LinearOrder α] {a : α}, SignType.sign a ≤ 0 ↔ a ≤ 0
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.sup_eq_closure_mul : ∀ {M : Type u_3} [inst : Monoid M] (H K : Submonoid M), H ⊔ K = Submonoid.closure (↑H * ↑K)
-- Mathlib.CategoryTheory.Presentable.LocallyPresentable
CategoryTheory.IsAccessibleCategory.mk : ∀ {C : Type u} [hC : CategoryTheory.Category.{v, u} C],
  (∃ κ, ∃ (x : Fact κ.IsRegular), CategoryTheory.IsCardinalAccessibleCategory C κ) →
    CategoryTheory.IsAccessibleCategory.{w, v, u} C
-- Mathlib.Logic.Equiv.Functor
Bifunctor.mapEquiv_symm_apply : ∀ {α β : Type u} {α' β' : Type v} (F : Type u → Type v → Type w) [inst : Bifunctor F] [inst_1 : LawfulBifunctor F]
  (h : α ≃ β) (h' : α' ≃ β') (y : F β β'), (Bifunctor.mapEquiv F h h').symm y = bimap (⇑h.symm) (⇑h'.symm) y
-- Mathlib.Order.WithBot
WithBot.ofDual_bot : ∀ {α : Type u_1}, WithBot.ofDual ⊥ = ⊤
-- Mathlib.Analysis.Normed.Operator.Completeness
/-- Let `s` be a bounded set in the space of continuous (semi)linear maps `E →SL[σ] F` taking values
in a proper space. If `s` interpreted as a set in the space of maps `E → F` with topology of
pointwise convergence is closed, then it is compact.

TODO: reformulate this in terms of a type synonym with the right topology.  -/
ContinuousLinearMap.isCompact_image_coe_of_bounded_of_closed_image : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {F : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NontriviallyNormedField 𝕜]
  [inst_2 : NontriviallyNormedField 𝕜₂] [inst_3 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {E' : Type u_6}
  [inst_4 : SeminormedAddCommGroup E'] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : RingHomIsometric σ₁₂] [ProperSpace F]
  {s : Set (E' →SL[σ₁₂] F)}, Bornology.IsBounded s → IsClosed (DFunLike.coe '' s) → IsCompact (DFunLike.coe '' s)
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.Reflective.toFaithful : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {R : CategoryTheory.Functor D C} [self : CategoryTheory.Reflective R], R.Faithful
-- Mathlib.Algebra.Star.NonUnitalSubsemiring
SubStarSemigroup.mk.sizeOf_spec : ∀ {M : Type v} [inst : Mul M] [inst_1 : Star M] [inst_2 : SizeOf M] (toSubsemigroup : Subsemigroup M)
  (star_mem' : ∀ {a : M}, a ∈ toSubsemigroup.carrier → star a ∈ toSubsemigroup.carrier),
  sizeOf { toSubsemigroup := toSubsemigroup, star_mem' := star_mem' } = 1 + sizeOf toSubsemigroup
-- Mathlib.SetTheory.Lists
Lists.Equiv.brecOn : ∀ {α : Type u_1} {motive_1 : (a a_1 : Lists α) → a.Equiv a_1 → Prop}
  {motive_2 : (a a_1 : Lists' α true) → a.Subset a_1 → Prop} {a a_1 : Lists α} (t : a.Equiv a_1),
  (∀ (a a_2 : Lists α) (t : a.Equiv a_2), t.below → motive_1 a a_2 t) →
    (∀ (a a_2 : Lists' α true) (t : a.Subset a_2), t.below → motive_2 a a_2 t) → motive_1 a a_1 t
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.Q_map_comp_Qinv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y Y' : C} (f : X ⟶ Y') (s : Y ⟶ Y') (hs : W s),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MorphismProperty.LeftFraction.Localization.Q W).map f)
      (CategoryTheory.MorphismProperty.LeftFraction.Localization.Qinv s hs) =
    CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk { Y' := Y', f := f, s := s, hs := hs }
-- Mathlib.Topology.Order.LocalExtr
IsLocalExtr.on : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {a : α},
  IsLocalExtr f a → ∀ (s : Set α), IsLocalExtrOn f s a
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.locallyIntegrable_zero : ∀ {X : Type u_1} {ε'' : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace ε''] [inst_3 : ESeminormedAddMonoid ε''] {μ : MeasureTheory.Measure X},
  MeasureTheory.LocallyIntegrable (fun x => 0) μ
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.pair : {ι : Type v} → ι → ι → CategoryTheory.Pairwise ι
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.instSemilatticeSupFiniteIndexNormalAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → SemilatticeSup (FiniteIndexNormalAddSubgroup G)
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- The forgetful functor from group objects to the ambient category.  -/
CategoryTheory.Grp.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.Functor (CategoryTheory.Grp C) C
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instFunLikeSet : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] → [inst_1 : TopologicalSpace M] → FunLike (MeasureTheory.VectorMeasure α M) (Set α) M
-- Mathlib.Algebra.Order.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.embedding_strictMono : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : LinearOrderedCommGroupWithZero B] {f : A →*₀ B},
  StrictMono ⇑MonoidWithZeroHom.ValueGroup₀.embedding
-- Mathlib.Tactic.ModCases
/-- Nat case of `mod_cases h : e % n`.
 -/
Mathlib.Tactic.ModCases.NatMod.modCases : Lean.TSyntax `Lean.binderIdent → Q(ℕ) → ℕ → Lean.Elab.Tactic.TacticM Unit
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.toEmoji : Aesop.SafeRuleResult → String
-- Mathlib.GroupTheory.IsSubnormal
Subgroup.IsSubnormal.below : {G : Type u_1} →
  [inst : Group G] → {motive : (a : Subgroup G) → a.IsSubnormal → Prop} → {a : Subgroup G} → a.IsSubnormal → Prop
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.ext_iff : ∀ {R : Type u_1} [inst : Semiring R] {p q : LaurentPolynomial R}, p = q ↔ ∀ (a : ℤ), p.coeff a = q.coeff a
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring of a `Semiring` is a `Semiring`.  -/
Subsemiring.toSemiring : {R : Type u_1} → [inst : Semiring R] → (s : Subsemiring R) → Semiring ↥s
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_map_iff : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {hr₁ : S₁.RightHomologyData}
  {hr₂ : S₂.RightHomologyData} (ψr : CategoryTheory.ShortComplex.RightHomologyMapData φ hr₁ hr₂)
  [inst_5 : (F.mapShortComplex.obj S₁).HasHomology] [inst_6 : (F.mapShortComplex.obj S₂).HasHomology]
  [hr₁.IsPreservedBy F] [hr₂.IsPreservedBy F],
  CategoryTheory.ShortComplex.QuasiIso (F.mapShortComplex.map φ) ↔ CategoryTheory.IsIso (F.map ψr.φH)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyLED_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLED k fallback = t₂.getKeyLED k fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {he : t.isEmpty = false} {km : α}, t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare k km).isLE = true
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.instCoeMonCat : Coe CommMonCat MonCat
-- Mathlib.Data.Set.Function
Function.Bijective.bijOn_preimage : ∀ {α : Type u_1} {β : Type u_2} {t : Set β} {f : α → β}, Function.Bijective f → Set.BijOn f (f ⁻¹' t) t
-- Mathlib.Algebra.Algebra.Unitization
Unitization.fst_star : ∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [inst_1 : Star A] (x : Unitization R A),
  (star x).toProd.1 = star x.toProd.1
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.instT1Space : ∀ {X : Type u_1} {R : Type u_3} [inst : Zero X] [inst_1 : Zero R] [inst_2 : TopologicalSpace X]
  [inst_3 : TopologicalSpace R] [T1Space R], T1Space (ContinuousMapZero X R)
-- Batteries.Lean.EStateM
EStateM.run_orElse : ∀ {σ ε α δ : Type u_1} [h : EStateM.Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (s : σ),
  (x₁ <|> x₂).run s =
    match x₁.run s with
    | EStateM.Result.ok x s => EStateM.Result.ok x s
    | EStateM.Result.error a s' => x₂.run (EStateM.Backtrackable.restore s' (EStateM.Backtrackable.save s))