mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.inv_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : Group γ] [inst_3 : IsTopologicalGroup γ] (f : α →ₘ[μ] γ), f⁻¹.toGerm = f.toGerm⁻¹
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.deterministic_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {f : α → β} (hf : Measurable f) {g : β → γ} (hg : Measurable g),
  (ProbabilityTheory.Kernel.deterministic f hf).map g = ProbabilityTheory.Kernel.deterministic (g ∘ f) ⋯
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRk_loopyOn : ∀ {α : Type u_1} (X Y : Set α), (Matroid.loopyOn Y).eRk X = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.comp_preservesColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {E : Type u₃}
  [ℰ : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E)
  [CategoryTheory.Limits.PreservesColimit K F] [CategoryTheory.Limits.PreservesColimit (K.comp F) G],
  CategoryTheory.Limits.PreservesColimit K (F.comp G)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelOrderHom_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] (X : C) (a : CategoryTheory.Subobject (Opposite.op X)),
  (CategoryTheory.Limits.kernelOrderHom X) a =
    CategoryTheory.Subobject.lift (fun x f x_1 => CategoryTheory.Subobject.mk (CategoryTheory.Limits.kernel.ι f.unop)) ⋯
      a
-- Mathlib.Dynamics.PeriodicPts.Defs
MulAction.zpow_period_add_smul : ∀ {α : Type v} {G : Type u} [inst : Group G] [inst_1 : MulAction G α] (i : ℤ) (g : G) (a : α),
  g ^ (↑(MulAction.period g a) + i) • a = g ^ i • a
-- Lean.Data.Lsp.Client
Lean.Lsp.RegistrationParams.mk : Array Lean.Lsp.Registration → Lean.Lsp.RegistrationParams
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.map : ∀ {V : Type u} {V' : Type v} {u v : V} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G →g G'),
  G.Reachable u v → G'.Reachable (f u) (f v)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- A function valued in a metric space has bounded variation on any `Finset` (the finiteness of
the space's distances makes the total variation finite).  -/
BoundedVariationOn.of_finite : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_3} [inst_1 : PseudoMetricSpace E] (f : α → E) (s : Set α)
  [Finite ↑s], BoundedVariationOn f s
-- Lean.Elab.Do.InferControlInfo
/-- The `do` block syntactically contains a `break`.  -/
Lean.Elab.Do.ControlInfo.breaks : Lean.Elab.Do.ControlInfo → Bool
-- Mathlib.Condensed.Discrete.Colimit
Condensed.lanPresheafIso.eq_1 : ∀ {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))}
  (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)),
  Condensed.lanPresheafIso hF =
    (CategoryTheory.Functor.Final.colimitIso (Profinite.Extend.functorOp S.asLimitCone)
          ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op S)).comp
            (FintypeCat.toProfinite.op.comp F))).symm ≪≫
      (CategoryTheory.Limits.colimit.isColimit (S.diagram.op.comp F)).coconePointUniqueUpToIso hF
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.homogeneousComponent_of_lt_order_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R} {p : ℕ},
  ↑p < f.order → (MvPowerSeries.homogeneousComponent p) f = 0
-- Mathlib.Data.FP.Basic
FP.Float.finite.inj : ∀ {C : FP.FloatCfg} {a : Bool} {e : ℤ} {m : ℕ} {a_1 : FP.ValidFinite e m} {a_2 : Bool} {e_1 : ℤ} {m_1 : ℕ}
  {a_3 : FP.ValidFinite e_1 m_1},
  FP.Float.finite a e m a_1 = FP.Float.finite a_2 e_1 m_1 a_3 → a = a_2 ∧ e = e_1 ∧ m = m_1
-- Std.Http.Protocol.H1.Error
/-- Invalid chunk encoding.
 -/
Std.Http.Protocol.H1.Error.invalidChunk : Std.Http.Protocol.H1.Error
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldl.eq_2 : ∀ {σ : Sort u_1} {α : Type u_2} (f : σ → α → σ) (x : σ) (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α)
  (r : RBTree.RBNode α),
  RBTree.RBNode.foldl f x (RBTree.RBNode.node c l v r) = RBTree.RBNode.foldl f (f (RBTree.RBNode.foldl f x l) v) r
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.mem_range_lift_of_le : ∀ {a : Cardinal.{u}} {b : Cardinal.{max u v}}, b ≤ Cardinal.lift.{v, u} a → b ∈ Set.range Cardinal.lift.{v, u}
-- Mathlib.Topology.EMetricSpace.Defs
/-- An extended metric space is a type endowed with a `ℝ≥0∞`-valued distance `edist` satisfying
`edist x y = 0 ↔ x = y`, commutativity `edist x y = edist y x`, and the triangle inequality
`edist x z ≤ edist x y + edist y z`.

See pseudo extended metric spaces (`PseudoEMetricSpace`) for the similar class with the
`edist x y = 0 ↔ x = y` assumption weakened to `edist x x = 0`.

Any extended metric space is a T1 topological space and a uniform space (see `TopologicalSpace`,
`T1Space`, `UniformSpace`), where the topology and uniformity come from the metric.

We make the uniformity/topology part of the data instead of deriving it from the metric.
This e.g. ensures that we do not get a diamond when doing
`[EMetricSpace α] [EMetricSpace β] : TopologicalSpace (α × β)`:
The product metric and product topology agree, but not definitionally so.
See Note [forgetful inheritance].  -/
EMetricSpace : Type u → Type u
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (t.insertMany l).getKey! k' = k
-- Lean.Parser.Do
Lean.Parser.Term.doReturn.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
/-- A presheaf of modules over `R : Cᵒᵖ ⥤ RingCat` consists of family of
objects `obj X : ModuleCat (R.obj X)` for all `X : Cᵒᵖ` together with
functorial maps `obj X ⟶ (ModuleCat.restrictScalars (R.map f)).obj (obj Y)`
for all `f : X ⟶ Y` in `Cᵒᵖ`.  -/
PresheafOfModules : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    CategoryTheory.Functor Cᵒᵖ RingCat → Type (max (max (max u u₁) (v + 1)) v₁)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationDesc.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {T : AlgebraicGeometry.Scheme} (f₁ f₁_1 : X ⟶ T) (e_f₁ : f₁ = f₁_1)
  (f₂ f₂_1 : T ⟶ Y) (e_f₂ : f₂ = f₂_1) [inst_2 : AlgebraicGeometry.IsIntegralHom f₂]
  (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂),
  AlgebraicGeometry.Scheme.Hom.normalizationDesc f f₁ f₂ H =
    AlgebraicGeometry.Scheme.Hom.normalizationDesc f f₁_1 f₂_1 ⋯
-- Mathlib.Algebra.GroupWithZero.Associated
associated_isUnit_mul_left_iff : ∀ {N : Type u_2} [inst : CommMonoid N] {u a b : N}, IsUnit u → (Associated (u * a) b ↔ Associated a b)
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.instToStringDefaultClause : {n : ℕ} → ToString (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
-- Std.Do.Triple.SpecLemmas
Std.Do.StringInvariant.eq_1 : ∀ (s : String) (β : Type u) (ps : Std.Do.PostShape), Std.Do.StringInvariant s β ps = Std.Do.PostCond (s.Pos × β) ps
-- Mathlib.Topology.NhdsKer
nhdsKer_def : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set X), nhdsKer s = ⋂₀ {t | IsOpen t ∧ s ⊆ t}
-- Init.Data.String.Lemmas.Pattern.Find.Basic
_private.Init.Data.String.Lemmas.Pattern.Find.Basic.0.List.findSome?.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match none with
    | some b => h_1 b
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_5 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (x : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (CategoryTheory.FreeMonoidalCategory.Hom.l_inv x) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.FreeMonoidalCategory.projectObj f x)).inv
-- Init.Data.Iterators.Combinators.Monadic.Attach
/-- Internal state of the `attachWith` combinator. Do not depend on its internals.
 -/
Std.Iterators.Types.Attach : (α : Type w) → (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → (β → Prop) → Type w
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntry.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.isEmpty = false → Sort u_3)
  (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l_1 r : Std.DTreeMap.Internal.Impl α β)
  (h :
    (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
      false)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l l_2 : Std.DTreeMap.Internal.Impl α β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β k_2) →
                  (l_3 r : Std.DTreeMap.Internal.Impl α β) →
                    l_2 = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r →
                      (h :
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                                (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r)).isEmpty =
                            false) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r))
                          h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r), h with
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_1 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l l_2@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_3 r), h_3 =>
      h_2 size k v l l_2 size_2 k_2 v_2 l_3 r h h_3) =
    h_2 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ h
-- Mathlib.Topology.MetricSpace.Thickening
Metric.tendsto_nhdsSet : ∀ {α : Type u_2} {β : Type u_3} [inst : PseudoMetricSpace α] {l : Filter β} {s : Set α} {f : β → α},
  IsCompact s → s.Nonempty → (Filter.Tendsto f l (nhdsSet s) ↔ ∀ ε > 0, ∀ᶠ (x : β) in l, Metric.infDist (f x) s < ε)
-- Batteries.Data.List.Interleave
List.interleave.eq_def : ∀ {α : Type u_1} (x x_1 : List α),
  x.interleave x_1 =
    match x, x_1 with
    | [], l₂ => l₂
    | a :: l₁, l₂ => a :: l₂.interleave l₁
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.linearIndependentSingleton : ∀ {I : Type u_1} [inst : LinearOrder I],
  LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval {fun x => false})
-- Mathlib.Algebra.Homology.QuasiIso
HomologicalComplex.instIsStableUnderRetractsQuasiIso : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.CategoryWithHomology C], (HomologicalComplex.quasiIso C c).IsStableUnderRetracts
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.isoShortComplexH1_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.isoShortComplexH1 A).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ShortComplex.homMk (groupHomology.chainsIso₂ A).inv (groupHomology.chainsIso₁ A).inv
        (groupHomology.chainsIso₀ A).inv ⋯ ⋯)
      ((HomologicalComplex.natIsoSc' (ModuleCat k) (ComplexShape.down ℕ) 2 1 0 groupHomology.isoShortComplexH1._proof_1
              groupHomology.isoShortComplexH1._proof_2).inv.app
        (groupHomology.inhomogeneousChains A))
-- Std.Data.TreeMap.Raw.Basic
/-- Returns `true` if there is a mapping for the given key `a` or a key that is equal to `a` according
to the comparator `cmp`. There is also a `Prop`-valued version
of this: `a ∈ t` is equivalent to `t.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for equality checks, while for tree maps, both use the given comparator `cmp`.
 -/
Std.TreeMap.Raw.contains : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Bool
-- Init.Prelude
/-- State monads provide a value of a given type (the _state_) that can be retrieved or replaced.
Instances may implement these operations by passing state values around, by using a mutable
reference cell (e.g. `ST.Ref σ`), or in other ways.

In this class, `σ` is a `semiOutParam`, which means that it can influence the choice of instance.
`MonadState σ` provides the same operations, but requires that `σ` be inferable from `m`.

The mutable state of a state monad is visible between multiple `do`-blocks or functions, unlike
[local mutable state](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=do-notation-let-mut) in `do`-notation.
 -/
MonadStateOf : semiOutParam (Type u) → (Type u → Type v) → Type (max (u + 1) v)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If `f` is a morphism `X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂` whose `X₁ ⟶ Y₁` entry is an isomorphism,
then we can construct isomorphisms `L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂` and `R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂`
so that `L.hom ≫ g ≫ R.hom` is diagonal (with `X₁ ⟶ Y₁` component still `f`),
via Gaussian elimination.
 -/
CategoryTheory.Biprod.gaussian : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
        {X₁ X₂ Y₁ Y₂ : C} →
          (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) →
            [CategoryTheory.IsIso
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
                    (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))] →
              (L : X₁ ⊞ X₂ ≅ X₁ ⊞ X₂) ×'
                (R : Y₁ ⊞ Y₂ ≅ Y₁ ⊞ Y₂) ×'
                  (g₂₂ : X₂ ⟶ Y₂) ×'
                    CategoryTheory.CategoryStruct.comp L.hom (CategoryTheory.CategoryStruct.comp f R.hom) =
                      CategoryTheory.Limits.biprod.map
                        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
                          (CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.biprod.fst))
                        g₂₂
-- Mathlib.Analysis.Convex.Basic
Convex.add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s t : Set E}, Convex 𝕜 s → Convex 𝕜 t → Convex 𝕜 (s + t)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sum_f_inl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S) (i : E.I₀), (E.sum F).f (Sum.inl i) = E.f i
-- Mathlib.Algebra.Homology.HomotopyCategory.KProjective
CochainComplex.instIsKProjectiveExtendNatIntEmbeddingDownNatOfProjectiveX : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (K : ChainComplex C ℕ) [∀ (n : ℕ), CategoryTheory.Projective (K.X n)],
  CochainComplex.IsKProjective (HomologicalComplex.extend K ComplexShape.embeddingDownNat)
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.instCompactSpace_coe : ∀ (𝕜 : Type u_1) (ι : Type u_2) [inst : Fintype ι] [inst_1 : TopologicalSpace 𝕜] [inst_2 : Semiring 𝕜]
  [inst_3 : PartialOrder 𝕜] [OrderClosedTopology 𝕜] [ContinuousAdd 𝕜] [CompactIccSpace 𝕜] [IsOrderedAddMonoid 𝕜],
  CompactSpace ↑(stdSimplex 𝕜 ι)
-- Mathlib.Algebra.GroupWithZero.ProdHom
/-- Given groups with zero `G₀`, `H₀`, the natural inclusion ordered homomorphism from
`G₀` to `WithZero (G₀ˣ × H₀ˣ)`, which is the group with zero that can be identified
as their product.  -/
MonoidWithZeroHom.inl : (G₀ : Type u_1) →
  (H₀ : Type u_2) →
    [inst : GroupWithZero G₀] →
      [inst_1 : GroupWithZero H₀] → [DecidablePred fun x => x = 0] → G₀ →*₀ WithZero (G₀ˣ × H₀ˣ)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_eq_bot_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [inst_1 : OrderBot α] (f : β → α) (S : Finset β),
  S.sup f = ⊥ ↔ ∀ s ∈ S, f s = ⊥
-- Std.Time.Format.Modifier
Std.Time.Modifier.m.injEq : ∀ (presentation presentation_1 : Std.Time.Number),
  (Std.Time.Modifier.m presentation = Std.Time.Modifier.m presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.map_map : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : NonUnitalNonAssocSemiring C] [inst_8 : Module R C] [inst_9 : Star C] (S : NonUnitalStarSubalgebra R A)
  (g : B →⋆ₙₐ[R] C) (f : A →⋆ₙₐ[R] B),
  NonUnitalStarSubalgebra.map g (NonUnitalStarSubalgebra.map f S) = NonUnitalStarSubalgebra.map (g.comp f) S
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_inf_partition : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (f : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (π : BoxIntegral.TaggedPrepartition I)
  {π' : BoxIntegral.Prepartition I},
  π'.IsPartition → BoxIntegral.integralSum f vol (π.infPrepartition π') = BoxIntegral.integralSum f vol π
-- Mathlib.GroupTheory.Index
AddSubgroup.add_self_mem_of_index_two : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 2 → ∀ (a : G), a + a ∈ H
-- Lean.Data.Lsp.CodeActions
/-- A data entry field that is preserved on a code action between a `textDocument/codeAction` and a `codeAction/resolve` request.
In particular, for Lean-created commands we expect `data` to have a `uri : DocumentUri` field so that `FileSource` can be implemented.
  -/
Lean.Lsp.CodeAction.data? : Lean.Lsp.CodeAction → Option Lean.Json