mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.setIntegral_condKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {E : Type u_4} {f : β × Ω → E} [inst_5 : NormedAddCommGroup E]
  [inst_6 : NormedSpace ℝ E] (a : α) {s : Set β},
  MeasurableSet s →
    ∀ {t : Set Ω},
      MeasurableSet t →
        MeasureTheory.IntegrableOn f (s ×ˢ t) (κ a) →
          ∫ (b : β) in s, ∫ (ω : Ω) in t, f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫ (x : β × Ω) in s ×ˢ t, f x ∂κ a
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.Dep.dep_isRestriction : ∀ {α : Type u_1} {M : Matroid α} {X : Set α} {N : Matroid α},
  M.Dep X → N.IsRestriction M → autoParam (X ⊆ N.E) Matroid.Dep.dep_isRestriction._auto_1 → N.Dep X
-- Mathlib.Logic.Function.Basic
Function.instIsTransOnFun : ∀ {α : Sort u_1} {β : Sort u_2} (r : β → β → Prop) (f : α → β) [IsTrans β r], IsTrans α (Function.onFun r f)
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- Type synonym, introduced to put a different `SMul` action on `C^n⟮I, M; 𝕜⟯`
which is defined as `f • r = f(x) * r`.
Denoted as `C^n⟮I, M; 𝕜⟯⟨x⟩` within the `Derivation` namespace.  -/
Derivation.«termC^_⟮_,_;_⟯⟨_⟩» : Lean.ParserDescr
-- Init.Data.List.Basic
List.Sublist.below.cons_cons : ∀ {α : Type u_1} {motive : (a a_1 : List α) → a.Sublist a_1 → Prop} {l₁ l₂ : List α} (a : α) (a_1 : l₁.Sublist l₂),
  List.Sublist.below a_1 → motive l₁ l₂ a_1 → List.Sublist.below ⋯
-- Mathlib.Algebra.Star.CentroidHom
CentroidHom.star_apply : ∀ {α : Type u_1} [inst : NonUnitalNonAssocSemiring α] [inst_1 : StarRing α] (f : CentroidHom α) (a : α),
  (star f) a = star (f (star a))
-- Batteries.Data.List.Lemmas
List.disjoint_iff_ne : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Disjoint l₂ ↔ ∀ a ∈ l₁, ∀ b ∈ l₂, a ≠ b
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.command.sizeOf_spec : sizeOf Lean.Elab.DocElabKind.command = 1
-- Mathlib.Algebra.Order.Group.Cone
/-- Construct a partial order by designating a cone in an abelian group.  -/
PartialOrder.mkOfGroupCone : {S : Type u_1} →
  {G : Type u_2} → [inst : CommGroup G] → [inst_1 : SetLike S G] → S → [GroupConeClass S G] → PartialOrder G
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.Rel : (α₁ α₂ : Type w) →
  (m : Type w → Type w') →
    (β : Type w) →
      [Monad m] →
        [inst : Std.Iterator α₁ m β] →
          [inst_1 : Std.Iterator α₂ m β] →
            [Std.Iterators.Finite α₁ m] → [Std.Iterators.Finite α₂ m] → Std.IterM m β → Std.IterM m β → Prop
-- Mathlib.GroupTheory.Index
Subgroup.instFiniteIndexProdProd : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [H.FiniteIndex] [K.FiniteIndex], (H.prod K).FiniteIndex
-- Mathlib.Probability.Kernel.Disintegration.Integral
ProbabilityTheory.lintegral_condKernel : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω]
  [inst_3 : MeasurableSpace.CountableOrCountablyGenerated α β] {κ : ProbabilityTheory.Kernel α (β × Ω)}
  [inst_4 : ProbabilityTheory.IsFiniteKernel κ] {f : β × Ω → ENNReal},
  Measurable f → ∀ (a : α), ∫⁻ (b : β), ∫⁻ (ω : Ω), f (b, ω) ∂κ.condKernel (a, b) ∂κ.fst a = ∫⁻ (x : β × Ω), f x ∂κ a
-- Mathlib.LinearAlgebra.Matrix.Diagonal
Matrix.diagonal_comp_single : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type v} [inst_2 : CommSemiring R] (w : n → R) (i : n),
  Matrix.toLin' (Matrix.diagonal w) ∘ₗ LinearMap.single R (fun x => R) i = w i • LinearMap.single R (fun x => R) i
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- **Alias** of `FunLike.coe_sub`. -/
SlashInvariantForm.coe_sub : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Order.Lattice
inf_eq_sup : ∀ {α : Type u} [inst : Lattice α] {a b : α}, a ⊓ b = a ⊔ b ↔ a = b
-- Mathlib.Topology.Order.MonotoneConvergence
tendsto_atTop_isLUB : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α] [inst_2 : Preorder α]
  [SupConvergenceClass α] {f : ι → α} {a : α},
  Monotone f → IsLUB (Set.range f) a → Filter.Tendsto f Filter.atTop (nhds a)
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.mapsTo_Ico : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictAntiOn f (Set.Icc a b) → Set.MapsTo f (Set.Ico a b) (Set.Ioc (f b) (f a))
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
Matrix.ProjectiveSpecialLinearGroup.toPGL_surj_iff : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R] [Nonempty n],
  Function.Surjective ⇑Matrix.ProjectiveSpecialLinearGroup.toPGL ↔ ∀ (r : Rˣ), ∃ k, k ^ Fintype.card n = r
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
/-- An alternative description of the slit plane as consisting of nonzero complex numbers
whose argument is not π.  -/
Complex.mem_slitPlane_iff_arg : ∀ {z : ℂ}, z ∈ Complex.slitPlane ↔ z.arg ≠ Real.pi ∧ z ≠ 0
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.stoppedValue_upperCrossingTime : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  MeasureTheory.upperCrossingTime a b f N (n + 1) ω ≠ N →
    b ≤ MeasureTheory.stoppedValue f (fun ω => ↑(MeasureTheory.upperCrossingTime a b f N (n + 1) ω)) ω
-- Mathlib.Algebra.Ring.Subring.Basic
AddSubmonoid.mk.congr_simp : ∀ {M : Type u_3} [inst : AddZeroClass M] (toAddSubsemigroup toAddSubsemigroup_1 : AddSubsemigroup M)
  (e_toAddSubsemigroup : toAddSubsemigroup = toAddSubsemigroup_1) (zero_mem' : 0 ∈ toAddSubsemigroup.carrier),
  { toAddSubsemigroup := toAddSubsemigroup, zero_mem' := zero_mem' } =
    { toAddSubsemigroup := toAddSubsemigroup_1, zero_mem' := ⋯ }
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
ofDegLex_toDegLex : ∀ {α : Type u_1} (a : α), ofDegLex (toDegLex a) = a
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.mem_upperCentralSeries_succ_iff`.

---

The `n+1`st term of the upper central series `H i` has underlying set equal to the `x` such
that `⁅x,G⁆ ⊆ H n`.  -/
mem_upperCentralSeries_succ_iff : ∀ {G : Type u_1} [inst : Group G] {n : ℕ} {x : G},
  x ∈ Subgroup.upperCentralSeries G (n + 1) ↔ ∀ (y : G), ⁅x, y⁆ ∈ Subgroup.upperCentralSeries G n
-- Init.Control.Lawful.Instances
OptionT.run_monadMap : ∀ {n : Type u → Type u_1} {m : Type u → Type u_2} {α : Type u} [inst : MonadFunctorT n m] (f : {β : Type u} → n β → n β)
  (x : OptionT m α), (monadMap f x).run = monadMap f x.run
-- Init.Data.SInt.Basic
/-- Adds two 16-bit signed integers, wrapping around on over- or underflow.  Usually accessed via the `+`
operator.

This function is overridden at runtime with an efficient implementation.
 -/
Int16.add : Int16 → Int16 → Int16
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
NumberField.FinitePlace.hasFiniteMulSupport_int : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : NumberField.RingOfIntegers K},
  x ≠ 0 → Function.HasFiniteMulSupport fun w => w ↑x
-- Mathlib.Order.Cover
Pi.wcovBy_iff : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → PartialOrder (α i)] {a b : (i : ι) → α i} [Nonempty ι],
  a ⩿ b ↔ ∃ i, a i ⩿ b i ∧ ∀ (j : ι), j ≠ i → a j = b j
-- Mathlib.RingTheory.KrullDimension.Zero
IsLocalRing.of_isMaximal_nilradical : ∀ (R : Type u_1) [inst : CommSemiring R] [(nilradical R).IsMaximal], IsLocalRing R
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
/-- The retraction of the unit in the proof of `4 → 1` in `isIso_tfae` below.  -/
_private.Mathlib.CategoryTheory.Monoidal.Braided.Reflection.0.CategoryTheory.Monoidal.Reflective.adjRetraction : {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.MonoidalCategory D] →
          [CategoryTheory.SymmetricCategory D] →
            [inst_4 : CategoryTheory.MonoidalClosed D] →
              {R : CategoryTheory.Functor C D} →
                [R.Faithful] →
                  [R.Full] →
                    {L : CategoryTheory.Functor D C} →
                      (adj : L ⊣ R) →
                        (c : C) →
                          (d : D) →
                            [CategoryTheory.IsIso
                                  (L.map
                                    (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app (d ⟹ R.obj c))
                                      (adj.unit.app d)))] →
                              (L.comp R).obj (d ⟹ R.obj c) ⟶ d ⟹ R.obj c
-- Mathlib.Order.UpperLower.Principal
LowerSet.coe_Iic : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑(LowerSet.Iic a) = Set.Iic a
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.prod_top_top : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q], ⊤.prod ⊤ = ⊤
-- Mathlib.GroupTheory.GroupAction.IterateAct
/-- A structure with a single field `val : ℕ`
that additively acts on `α` by `⟨n⟩ +ᵥ x = f^[n] x`.  -/
IterateAddAct : {α : Type u_1} → (α → α) → Type
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_eq_none : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {a : α}, a ∉ t → Std.ExtDTreeMap.Const.get? t a = none
-- Lean.Server.References
Lean.Server.Reference.mk.inj : ∀ {ident : Lean.Lsp.RefIdent} {aliases : Array Lean.Lsp.RefIdent} {range : Lean.Lsp.Range} {stx : Lean.Syntax}
  {ci : Lean.Elab.ContextInfo} {info : Lean.Elab.Info} {isBinder : Bool} {ident_1 : Lean.Lsp.RefIdent}
  {aliases_1 : Array Lean.Lsp.RefIdent} {range_1 : Lean.Lsp.Range} {stx_1 : Lean.Syntax} {ci_1 : Lean.Elab.ContextInfo}
  {info_1 : Lean.Elab.Info} {isBinder_1 : Bool},
  { ident := ident, aliases := aliases, range := range, stx := stx, ci := ci, info := info, isBinder := isBinder } =
      { ident := ident_1, aliases := aliases_1, range := range_1, stx := stx_1, ci := ci_1, info := info_1,
        isBinder := isBinder_1 } →
    ident = ident_1 ∧
      aliases = aliases_1 ∧ range = range_1 ∧ stx = stx_1 ∧ ci = ci_1 ∧ info = info_1 ∧ isBinder = isBinder_1
-- Mathlib.CategoryTheory.Discrete.Basic
/-- A category is discrete when there is at most one morphism between two objects,
in which case they are equal.  -/
CategoryTheory.IsDiscrete : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.CategoryTheory.Limits.Creates
CategoryTheory.LiftableCocone.mk.sizeOf_spec : ∀ {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}
  {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cocone (K.comp F)} [inst_3 : SizeOf C] [inst_4 : SizeOf D]
  [inst_5 : SizeOf J] (liftedCocone : CategoryTheory.Limits.Cocone K) (validLift : F.mapCocone liftedCocone ≅ c),
  sizeOf { liftedCocone := liftedCocone, validLift := validLift } = 1 + sizeOf liftedCocone + sizeOf validLift
-- Std.Time.Format.Modifier
Std.Time.ExtendedDayPeriod.afternoon.sizeOf_spec : sizeOf Std.Time.ExtendedDayPeriod.afternoon = 1
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.instDistribMulAction : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → DistribMulAction R (TensorProduct R M N)
-- Mathlib.MeasureTheory.Measure.FiniteMeasurePi
MeasureTheory.FiniteMeasure.toMeasure_pi : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.FiniteMeasure (α i)),
  ↑(MeasureTheory.FiniteMeasure.pi μ) = MeasureTheory.Measure.pi fun i => ↑(μ i)
-- Mathlib.MeasureTheory.Measure.RegularityCompacts
/-- A finite measure `μ` on a completely pseudo-metrizable space `E` with
`SecondCountableTopology E` is inner regular. In other words, a finite measure
on such a space is a tight measure.
 -/
MeasureTheory.instInnerRegularOfIsCompletelyPseudoMetrizableSpace : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [SecondCountableTopology α]
  [TopologicalSpace.IsCompletelyPseudoMetrizableSpace α] [BorelSpace α] (P : MeasureTheory.Measure α)
  [MeasureTheory.IsFiniteMeasure P], P.InnerRegular
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.conts_stable_of_terminated : ∀ {K : Type u_1} {g : GenContFract K} {n m : ℕ} [inst : DivisionRing K],
  n ≤ m → g.TerminatedAt n → g.conts m = g.conts n
-- Mathlib.Combinatorics.Colex
_private.Mathlib.Combinatorics.Colex.0.Finset.Colex.trans_aux : ∀ {α : Type u_1} [inst : PartialOrder α] {s t u : Finset α} {a : α},
  toColex s ≤ toColex t → toColex t ≤ toColex u → a ∈ s → a ∉ t → ∃ b ∈ u, b ∉ s ∧ a ≤ b
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.densityProcess.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) (a : α) (x : γ) (s : Set β),
  κ.densityProcess ν n a x s =
    ((κ a) (MeasurableSpace.countablePartitionSet n x ×ˢ s) / (ν a) (MeasurableSpace.countablePartitionSet n x)).toReal
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_top_right_eq_bot_iff_le_center : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ⁅H, ⊤⁆ = ⊥ ↔ H ≤ Subgroup.center G
-- Mathlib.Tactic.Lift
/-- Generate instance for the `lift` tactic.  -/
Mathlib.Tactic.Lift.getInst : Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr × Lean.Expr)
-- Init.Data.Vector.Lemmas
Vector.mapIdx_mk : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : ℕ → α → β} {xs : Array α} (h : xs.size = n),
  Vector.mapIdx f (Vector.mk xs h) = Vector.mk (Array.mapIdx f xs) ⋯
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.equivEquivIso_symm_apply_symm_apply : ∀ {A B : FintypeCat} (i : A ≅ B) (a : B.obj),
  (FintypeCat.equivEquivIso.symm i).symm a = (CategoryTheory.ConcreteCategory.hom i.inv) a
-- Mathlib.Algebra.Order.Monoid.Unbundled.MinMax
min_mul_mul_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : Mul α] [MulRightMono α] (a b c : α), min (a * c) (b * c) = min a b * c
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.getKey?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α), Std.Internal.List.getKey? a [] = none
-- Mathlib.Logic.Equiv.List
Equiv.listUniqueEquiv_symm_apply : ∀ (α : Type u_1) [inst : Unique α] (n : ℕ), (Equiv.listUniqueEquiv α).symm n = List.replicate n default
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.map_source : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) {x : α}, x ∈ e.source → ↑e x ∈ e.target
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Sieve.firstMap.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))) {X : C}
  (S : CategoryTheory.Sieve X),
  CategoryTheory.Equalizer.Sieve.firstMap P S =
    CategoryTheory.Limits.Pi.lift fun fg =>
      CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.fst))
        ⟨fg.snd.fst, ⟨CategoryTheory.CategoryStruct.comp fg.snd.snd.fst ↑fg.snd.snd.snd, ⋯⟩⟩
-- Mathlib.Combinatorics.SimpleGraph.Hasse
/-- The subgraph of a walk contains the path graph with the same number of vertices  -/
SimpleGraph.Walk.pathGraphHomToSubgraph : {V : Type u_3} →
  {G : SimpleGraph V} → {u v : V} → (w : G.Walk u v) → SimpleGraph.pathGraph (w.length + 1) →g w.toSubgraph.coe
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withLocalDeclImp : {α : Type} → Lean.Name → Lean.BinderInfo → Lean.Expr → (Lean.Expr → Lean.MetaM α) → Lean.LocalDeclKind → Lean.MetaM α
-- Mathlib.Tactic.DepRewrite
/-- See `Config.castMode`.  -/
Mathlib.Tactic.DepRewrite.CastMode : Type
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.isCompact' : ∀ {α : Type u_4} [inst : TopologicalSpace α] (self : TopologicalSpace.Compacts α), IsCompact self.carrier
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.algebraMap_eq : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R], algebraMap R (MvPolynomial σ R) = MvPolynomial.C
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.leftUnitor_tensor_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv Y)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X Y).hom
        h)
-- Mathlib.Algebra.Order.Group.CompleteLattice
ciInf_mul : ∀ {ι : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [MulRightMono G], BddBelow (Set.range f) → ∀ (a : G), (⨅ i, f i) * a = ⨅ i, f i * a
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.mk.sizeOf_spec : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : SizeOf R] [inst_4 : SizeOf S] [inst_5 : SizeOf ι] [inst_6 : SizeOf σ]
  (toPresentation : Algebra.Presentation R S ι σ) (map : σ → ι) (map_inj : Function.Injective map),
  sizeOf { toPresentation := toPresentation, map := map, map_inj := map_inj } = 1 + sizeOf toPresentation