mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Side
AffineSubspace.SSameSide.wSameSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SSameSide x y → s.WSameSide x y
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.numeratorHom_apply : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {r : R},
  OreLocalization.numeratorHom r = r /ₒ 1
-- Mathlib.MeasureTheory.Measure.Prod
/-- Two finite measures on a product `α × β × γ` are equal iff they are equal on products of sets.
See `ext_prod₃_iff'` for the same statement for `(α × β) × γ`.  -/
MeasureTheory.Measure.ext_prod₃_iff : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {μ ν : MeasureTheory.Measure (α × β × γ)} [MeasureTheory.IsFiniteMeasure μ],
  μ = ν ↔
    ∀ {s : Set α} {t : Set β} {u : Set γ},
      MeasurableSet s → MeasurableSet t → MeasurableSet u → μ (s ×ˢ t ×ˢ u) = ν (s ×ˢ t ×ˢ u)
-- Mathlib.CategoryTheory.Subfunctor.Finite
CategoryTheory.Subfunctor.IsFinite.instFiniteIndex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type w)}
  (G : CategoryTheory.Subfunctor F) [hG : G.IsFinite], Finite (CategoryTheory.Subfunctor.IsFinite.Index G)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiffAt.fderiv_succ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {x₀ : E} {m : WithTop ℕ∞} {f : E → F → G} {g : E → F},
  ContDiffAt 𝕜 (m + 1) (Function.uncurry f) (x₀, g x₀) →
    ContDiffAt 𝕜 m g x₀ → ContDiffAt 𝕜 m (fun x => fderiv 𝕜 (f x) (g x)) x₀
-- Mathlib.Analysis.Fourier.Convolution
/-- The bilinear convolution of Schwartz functions.

The continuity in the left argument is provided in `SchwartzMap.convolution_continuous_left`.  -/
SchwartzMap.convolution : {𝕜 : Type u_1} →
  {E : Type u_3} →
    {F₁ : Type u_5} →
      {F₂ : Type u_6} →
        {F₃ : Type u_7} →
          [inst : RCLike 𝕜] →
            [inst_1 : NormedAddCommGroup E] →
              [inst_2 : InnerProductSpace ℝ E] →
                [FiniteDimensional ℝ E] →
                  [inst_4 : MeasurableSpace E] →
                    [BorelSpace E] →
                      [inst_6 : NormedAddCommGroup F₁] →
                        [inst_7 : NormedSpace ℂ F₁] →
                          [inst_8 : NormedSpace 𝕜 F₁] →
                            [inst_9 : SMulCommClass ℂ 𝕜 F₁] →
                              [inst_10 : NormedAddCommGroup F₂] →
                                [inst_11 : NormedSpace ℂ F₂] →
                                  [inst_12 : NormedSpace 𝕜 F₂] →
                                    [inst_13 : SMulCommClass ℂ 𝕜 F₂] →
                                      [inst_14 : NormedAddCommGroup F₃] →
                                        [inst_15 : NormedSpace ℂ F₃] →
                                          [inst_16 : NormedSpace 𝕜 F₃] →
                                            [inst_17 : SMulCommClass ℂ 𝕜 F₃] →
                                              (F₁ →L[𝕜] F₂ →L[𝕜] F₃) →
                                                SchwartzMap E F₁ →ₗ[𝕜] SchwartzMap E F₂ →L[𝕜] SchwartzMap E F₃
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.mul_slash : ∀ (k1 k2 : ℤ) (A : GL (Fin 2) ℝ) (f g : UpperHalfPlane → ℂ),
  SlashAction.map (k1 + k2) A (f * g) =
    |↑(Matrix.GeneralLinearGroup.det A)| • (SlashAction.map k1 A f * SlashAction.map k2 A g)
-- Mathlib.RingTheory.Trace.Basic
trace_eq_sum_automorphisms : ∀ {K : Type u_4} {L : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x : L)
  [inst_3 : FiniteDimensional K L] [IsGalois K L], (algebraMap K L) ((Algebra.trace K L) x) = ∑ σ, σ x
-- Mathlib.Algebra.Group.Equiv.Opposite
MulOpposite.opAddEquiv_apply : ∀ {α : Type u_2} [inst : Add α], ⇑MulOpposite.opAddEquiv = MulOpposite.op
-- Mathlib.Order.Interval.Finset.Defs
/-- Transfer `LocallyFiniteOrderTop` across an `OrderIso`.  -/
OrderIso.locallyFiniteOrderTop : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Preorder α] → [inst_1 : Preorder β] → [LocallyFiniteOrderTop β] → α ≃o β → LocallyFiniteOrderTop α
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inl_desc_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c}
  (α : K ⟶ M) (β : L ⟶ M) (i : ι),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i)
      ((CategoryTheory.Limits.biprod.desc α β).f i) =
    α.f i
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_min?_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∈ t → t.min?.isSome = true
-- Init.Control.Except
/-- Runs a computation from an underlying monad in the transformed monad with exceptions.
 -/
ExceptT.lift : {ε : Type u} → {m : Type u → Type v} → [Monad m] → {α : Type u} → m α → ExceptT ε m α
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.instFunLike : {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] → FunLike (R →ₑ+*[φ] S) R S
-- Mathlib.RingTheory.Coalgebra.TensorProduct
/-- The base ring is a right identity for the tensor product of coalgebras, up to
coalgebra equivalence.  -/
Coalgebra.TensorProduct.rid : (R : Type u_5) →
  (S : Type u_6) →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] →
                  [inst_6 : IsScalarTower R S M] → [inst_7 : Coalgebra S M] → TensorProduct R M R ≃ₗc[S] M
-- Mathlib.RingTheory.Bialgebra.Hom
/-- Identity map as a `BialgHom`.  -/
BialgHom.id : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [inst_3 : CoalgebraStruct R A] → A →ₐc[R] A
-- Mathlib.RingTheory.WittVector.MulP
/-- Multiplication by `n` is a polynomial function.  -/
WittVector.mulN_isPoly : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), WittVector.IsPoly p fun x _Rcr x_1 => x_1 * ↑n
-- Init.Data.String.Defs
String.byteIdx_rawEndPos : ∀ {s : String}, s.rawEndPos.byteIdx = s.utf8ByteSize
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.of_measure_le_smul : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {μ' : MeasureTheory.Measure α} {c : ENNReal},
  c ≠ ⊤ → μ' ≤ c • μ → ∀ {f : α → ε}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp f p μ'
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F) (S : AddSubmonoid M),
  AddSubmonoid.map f S = { carrier := ⇑f '' ↑S, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.WellOrderContinuous
CategoryTheory.Functor.instIsWellOrderContinuousCompFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : PartialOrder J]
  (F : CategoryTheory.Functor J C) {J' : Type w'} [inst_2 : PartialOrder J'] (f : J' ≤i J) [F.IsWellOrderContinuous],
  (⋯.functor.comp F).IsWellOrderContinuous
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.instFunLikeBasisSubtypeMemFinsetCycleFactorsFinset : {α : Type u_1} →
  [inst : DecidableEq α] → [inst_1 : Fintype α] → (g : Equiv.Perm α) → FunLike g.Basis (↥g.cycleFactorsFinset) α
-- Mathlib.Data.Nat.Factorization.Induction
/-- For any multiplicative function `f` with `f 1 = 1` and any `n ≠ 0`,
we can evaluate `f n` by evaluating `f` at `p ^ k` over the factorization of `n`  -/
Nat.multiplicative_factorization : ∀ {β : Type u_1} [inst : CommMonoid β] (f : ℕ → β),
  (∀ (x y : ℕ), x.Coprime y → f (x * y) = f x * f y) →
    f 1 = 1 → ∀ {n : ℕ}, n ≠ 0 → f n = n.factorization.prod fun p k => f (p ^ k)
-- Mathlib.CategoryTheory.Category.TwoP
/-- Turns a two-pointed type into a bipointed type, by forgetting that the pointed elements are
distinct.  -/
TwoP.toBipointed : TwoP → Bipointed
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.d₁_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁ : I₁) (i₂ : I₂) (i₁₂ : I₁₂), ¬c₁.Rel i₁ (c₁.next i₁) → K.d₁ c₁₂ i₁ i₂ i₁₂ = 0
-- Mathlib.Data.Set.Image
Set.preimage_inl_range_inr : ∀ {α : Type u_1} {β : Type u_2}, Sum.inl ⁻¹' Set.range Sum.inr = ∅
-- Mathlib.Algebra.Polynomial.Degree.Support
Polynomial.as_sum_support : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), p = ∑ i ∈ p.support, (Polynomial.monomial i) (p.coeff i)
-- Mathlib.Control.Bifunctor
Bifunctor.functor : {F : Type u₀ → Type u₁ → Type u₂} → [Bifunctor F] → {α : Type u₀} → Functor (F α)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
iteratedFDeriv_one_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} (m : Fin 1 → E), (iteratedFDeriv 𝕜 1 f x) m = (fderiv 𝕜 f x) (m 0)
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.go : Lean.Meta.Match.SimpH.M✝ Bool
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- The cycles of a short complex, given by the `K` field of a chosen left homology data.  -/
CategoryTheory.ShortComplex.cycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (S : CategoryTheory.ShortComplex C) → [S.HasLeftHomology] → C
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.map_rel : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N] (φ : L.Equiv M N)
  {n : ℕ} (r : L.Relations n) (x : Fin n → M),
  FirstOrder.Language.Structure.RelMap r (⇑φ ∘ x) ↔ FirstOrder.Language.Structure.RelMap r x
-- Mathlib.Data.Nat.Choose.Cast
Nat.cast_add_choose : ∀ (K : Type u_1) [inst : DivisionSemiring K] [CharZero K] {a b : ℕ},
  ↑((a + b).choose a) = ↑(a + b).factorial / (↑a.factorial * ↑b.factorial)
-- Mathlib.Topology.Order.Basic
nhds_basis_Ioo : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMaxOrder α] [NoMinOrder α]
  (a : α), (nhds a).HasBasis (fun b => b.1 < a ∧ a < b.2) fun b => Set.Ioo b.1 b.2
-- Mathlib.Data.Tree.Basic
BinaryTree.numLeaves_pos : ∀ {α : Type u} (x : BinaryTree α), 0 < x.numLeaves
-- Init.Data.BitVec.Lemmas
BitVec.sub_ofFin : ∀ {n : ℕ} (x : BitVec n) (y : Fin (2 ^ n)), x - { toFin := y } = { toFin := x.toFin - y }
-- Mathlib.Algebra.Regular.Defs
/-- An add-left-regular element is an element `c` such that addition
on the left by `c` is injective.  -/
IsAddLeftRegular : {R : Type u_1} → [Add R] → R → Prop
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
/-- The universal factorization ring of a monic polynomial `p` of degree `n`.
This is the representing object of the functor
`S ↦ "factorizations of p into (monic deg m) * (monic deg k) in S"`.
See `UniversalFactorizationRing.homEquiv`.  -/
Polynomial.UniversalFactorizationRing : {R : Type u_1} → [inst : CommRing R] → {n : ℕ} → (m k : ℕ) → n = m + k → Polynomial.MonicDegreeEq R n → Type u_1
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toList_roo_eq_singleton_iff : ∀ {k m n : ℕ}, (m<...n).toList = [k] ↔ n = m + 2 ∧ m + 1 = k
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_map_map : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A B : IntermediateField F E) (f : E →ₐ[F] L),
  (IntermediateField.map f A).relfinrank (IntermediateField.map f B) = A.relfinrank B
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- [Stacks Tag 00PY](https://stacks.math.columbia.edu/tag/00PY) -/
exists_leadingCoeff_pow_smul_mem_radical_conductor : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (φ : Polynomial R →ₐ[R] S) (t : S) (p : Polynomial R),
  integralClosure R S = ⊥ →
    φ.Finite →
      φ p * t ∈ (conductor R (φ Polynomial.X)).radical →
        ∀ (i : ℕ), p.coeff i • t ∈ (conductor R (φ Polynomial.X)).radical
-- Mathlib.GroupTheory.Coset.Basic
/-- An equivalence between any non-empty fiber of a `MonoidHom` and its kernel.  -/
MonoidHom.fiberEquivKer : {α : Type u_1} →
  [inst : Group α] → {H : Type u_2} → [inst_1 : Group H] → (f : α →* H) → (a : α) → ↑(⇑f ⁻¹' {f a}) ≃ ↥f.ker
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.smul_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : TopologicalSpace 𝕜] [inst_2 : SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜},
  MeasureTheory.StronglyMeasurable f → ∀ (c : β), MeasureTheory.StronglyMeasurable fun x => f x • c
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.beq.match_1.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive Nat.zero Nat.zero) (h_2 : (n : ℕ) → motive Nat.zero n.succ)
  (h_3 : (n : ℕ) → motive n.succ Nat.zero) (h_4 : (n m : ℕ) → motive n.succ m.succ),
  (match n.succ, Nat.zero with
    | Nat.zero, Nat.zero => h_1 ()
    | Nat.zero, n.succ => h_2 n
    | n.succ, Nat.zero => h_3 n
    | n.succ, m.succ => h_4 n m) =
    h_3 n
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.ofRepresentableBy.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X),
  CategoryTheory.MonObj.ofRepresentableBy X F α =
    { one := α.homEquiv'.symm 1,
      mul :=
        α.homEquiv'.symm
          (α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.fst X X) *
            α.homEquiv' (CategoryTheory.SemiCartesianMonoidalCategory.snd X X)),
      one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Mathlib.Computability.AkraBazzi.AkraBazzi
/-- The main proof of the lower-bound part of the Akra-Bazzi theorem. The factor `1 + ε n` does not
change the asymptotic order, but it is needed for the induction step to go through.  -/
AkraBazziRecurrence.smoothingFn_mul_asympBound_isBigO_T : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  (fun n => (1 + AkraBazziRecurrence.smoothingFn ↑n) * AkraBazziRecurrence.asympBound g a b n) =O[Filter.atTop] T
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.instHasBinaryBiproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  CategoryTheory.Limits.HasBinaryBiproducts C
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- In the specific case of continuous multilinear maps on spaces indexed by `Fin (n+1)`, where one
can build an element of `(i : Fin (n+1)) → M i` using `cons`, one can express directly the
additivity of a multilinear map along the first variable.  -/
ContinuousMultilinearMap.cons_add : ∀ {R : Type u} {n : ℕ} {M : Fin n.succ → Type w} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂]
  [inst_5 : (i : Fin n.succ) → TopologicalSpace (M i)] [inst_6 : TopologicalSpace M₂]
  (f : ContinuousMultilinearMap R M M₂) (m : (i : Fin n) → M i.succ) (x y : M 0),
  f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.isAlgebraic_tower_top : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {S : IntermediateField K L}
  [Algebra.IsAlgebraic K L], Algebra.IsAlgebraic (↥S) L
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_rightUnitor : ∀ {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 C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor c).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c)).hom
-- Mathlib.CategoryTheory.Limits.Shapes.Connected
CategoryTheory.instIsConnectedWidePullbackShape : ∀ {J : Type u_1}, CategoryTheory.IsConnected (CategoryTheory.Limits.WidePullbackShape J)
-- Mathlib.Data.Nat.Bitwise
_private.Mathlib.Data.Nat.Bitwise.0.Nat.xor.eq_1 : Nat.xor = Nat.bitwise bne
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.PullOut
/-- Pull-out property of the conditional expectation.  -/
MeasureTheory.condExp_smul_of_aestronglyMeasurable_left : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_2} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : Ω → ℝ} {g : Ω → E},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.Integrable (f • g) μ → MeasureTheory.Integrable g μ → μ[f • g | m] =ᵐ[μ] f • μ[g | m]
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.subsingleton_iff : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G}, Subsingleton (G ⧸ N) ↔ N = ⊤
-- Mathlib.Data.Real.Basic
Real.ringEquivCauchy_symm_apply_cauchy : ∀ (cauchy : CauSeq.Completion.Cauchy abs), (Real.ringEquivCauchy.symm cauchy).cauchy = cauchy
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithTerminal.widePullbackShapeEquivObj.match_1.eq_2 : ∀ {J : Type u_1} (motive : CategoryTheory.Limits.WidePullbackShape J → Sort u_2) (h_1 : (x : J) → motive (some x))
  (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.forget_reflects_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C), T.forget.ReflectsIsomorphisms
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.isAlphaAscii : UInt8 → Bool
-- Std.Sat.AIG.Lemmas
Std.Sat.AIG.instLawfulOperatorMkAtom : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α], Std.Sat.AIG.LawfulOperator α (fun x => α) Std.Sat.AIG.mkAtom
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.nnnorm_sub_eq_max : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] {R : Type u_4}
  [inst_2 : NonUnitalSeminormedRing R] [IsCancelMulZero R] {f g : C(α, R)}, f * g = 0 → ‖f - g‖₊ = max ‖f‖₊ ‖g‖₊
-- Lean.Data.Options
Lean.Options.find : Lean.Options → Lean.Name → Option Lean.DataValue
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.toArray_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.toList.toArray = t.toArray
-- Mathlib.Control.Monad.Cont
instLawfulMonadContExceptT : ∀ {m : Type u → Type v} [inst : Monad m] {ε : Type u} [inst_1 : MonadCont m] [LawfulMonadCont m],
  LawfulMonadCont (ExceptT ε m)
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (p : P.LimitOfShape J X) {X_1 Y : J} (f : X_1 ⟶ Y),
  p.toStructuredArrow.map f =
    CategoryTheory.StructuredArrow.homMk (CategoryTheory.ObjectProperty.homMk (p.diag.map f)) ⋯
-- Mathlib.Data.Finset.Lattice.Basic
Finset.mem_inter : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s₁ s₂ : Finset α}, a ∈ s₁ ∩ s₂ ↔ a ∈ s₁ ∧ a ∈ s₂
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.Relations.isUniversal_reflexive : ∀ {L : FirstOrder.Language} (r : L.Relations 2), FirstOrder.Language.BoundedFormula.IsUniversal r.reflexive
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanFileProgressKind : Lean.FromJson Lean.Lsp.LeanFileProgressKind
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.toPreimages_nonempty_of_surjective : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i : J}
  (s : Set (F.obj i)) [CategoryTheory.IsCofilteredOrEmpty J] [hFn : ∀ (j : J), Nonempty (F.obj j)],
  (∀ ⦃i j : J⦄ (f : i ⟶ j), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) →
    s.Nonempty → ∀ (j : J), Nonempty ((F.toPreimages s).obj j)
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.State.cache : Lean.MetavarContext.MkBinding.State → Std.HashMap Lean.ExprStructEq Lean.Expr
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.insertManyIfNew! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {ρ : Type u_1} [inst : ForIn Id ρ ((a : α) × β a)] {l : ρ}
  {t : Std.DTreeMap.Internal.Impl α β}, t.WF → (↑(t.insertManyIfNew! l)).WF
-- Mathlib.Data.List.Triplewise
List.triplewise_iff_getElem : ∀ {α : Type u_1} {l : List α} {p : α → α → α → Prop},
  List.Triplewise p l ↔ ∀ (i j k : ℕ) (hij : i < j) (hjk : j < k) (hk : k < l.length), p l[i] l[j] l[k]
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.Cocone.ofPushoutCocone_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingSpan C}
  (t :
    CategoryTheory.Limits.PushoutCocone (F.map CategoryTheory.Limits.WalkingSpan.Hom.fst)
      (F.map CategoryTheory.Limits.WalkingSpan.Hom.snd)),
  (CategoryTheory.Limits.Cocone.ofPushoutCocone t).pt = t.pt
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v)[a] = if h₂ : (k == a) = true ∧ k ∉ m then v else m[a]
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.keys_filter_key : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {f : α → Bool},
  (Std.DHashMap.filter (fun k x => f k) m).keys.Perm (List.filter f m.keys)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.isGLB_sInf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S : Set (Submodule R M)}, IsGLB S (sInf S)
-- Mathlib.Data.Vector.Basic
List.Vector.mOfFn.eq_2 : ∀ {m : Type u → Type u_6} [inst : Monad m] {α : Type u} (n : ℕ) (f : Fin (n + 1) → m α),
  List.Vector.mOfFn f = do
    let a ← f 0
    let v ← List.Vector.mOfFn fun i => f i.succ
    pure (a ::ᵥ v)