mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Set.ProjIcc
StrictMono.strictMonoOn_IciExtend : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {a : α} {f : ↑(Set.Ici a) → β},
  StrictMono f → StrictMonoOn (Set.IciExtend f) (Set.Ici a)
-- Mathlib.Order.JordanHolder
CompositionSeries.length_pos_of_head_eq_head_of_last_eq_last_of_length_pos : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
  RelSeries.head s₁ = RelSeries.head s₂ → RelSeries.last s₁ = RelSeries.last s₂ → 0 < s₁.length → 0 < s₂.length
-- Mathlib.Algebra.MvPolynomial.Funext
/-- Two multivariate polynomials over an integral domain are equal
if they are equal when evaluated anywhere in a box with infinite sides.  -/
MvPolynomial.funext_set : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] {σ : Type u_2} {p q : MvPolynomial σ R} (s : σ → Set R),
  (∀ (i : σ), (s i).Infinite) → (∀ x ∈ Set.univ.pi s, (MvPolynomial.eval x) p = (MvPolynomial.eval x) q) → p = q
-- Mathlib.GroupTheory.Coxeter.Length
_private.Mathlib.GroupTheory.Coxeter.Length.0.CoxeterSystem.termℓ_ : Lean.ParserDescr
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : (a : α) → β a → Bool} {k : α}, k ∈ Std.ExtDHashMap.filter f m → k ∈ m
-- Mathlib.Order.Hom.Lattice
SupHom.instInhabited.eq_1 : ∀ (α : Type u_2) [inst : Max α], SupHom.instInhabited α = { default := SupHom.id α }
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiagonal_two : Int.divisorsAntidiag 2 = {(1, 2), (2, 1), (-1, -2), (-2, -1)}
-- Mathlib.Geometry.Convex.Cone.Face.Basic
PointedCone.IsFaceOf.mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] {F C : PointedCone R M},
  F ≤ C → (∀ {x y : M} {a : R}, x ∈ C → y ∈ C → 0 < a → a • x + y ∈ F → x ∈ F) → F.IsFaceOf C
-- Mathlib.Topology.Instances.Real.Lemmas
/-- **Alias** of `IsOrderBornology.cobounded_eq`. -/
Real.cobounded_eq : ∀ {α : Type u_1} [inst : Bornology α] [inst_1 : LinearOrder α] [IsOrderBornology α] [NoMaxOrder α] [NoMinOrder α],
  Bornology.cobounded α = Filter.atBot ⊔ Filter.atTop
-- Mathlib.Algebra.Polynomial.Lifts
Polynomial.lifts_and_natDegree_eq_and_monic : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S},
  p ∈ Polynomial.lifts f → p.Monic → ∃ q, Polynomial.map f q = p ∧ q.natDegree = p.natDegree ∧ q.Monic
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.transPartialEquiv_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f' : PartialEquiv β γ) (a : α),
  ↑(e.transPartialEquiv f') a = ↑f' (e a)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
ContDiff.smulRight : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {f : E → StrongDual 𝕜 F} {g : E → G},
  ContDiff 𝕜 n f → ContDiff 𝕜 n g → ContDiff 𝕜 n fun x => ContinuousLinearMap.smulRight (f x) (g x)
-- Std.Time.Time.PlainTime
/-- Converts a `PlainTime` value to the total number of milliseconds.
 -/
Std.Time.PlainTime.toMilliseconds : Std.Time.PlainTime → Std.Time.Millisecond.Offset
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.le_topologicalClosure : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [inst_5 : ContinuousStar A] [inst_6 : ContinuousConstSMul R A]
  [inst_7 : IsSemitopologicalSemiring A] (s : NonUnitalStarSubalgebra R A), s ≤ s.topologicalClosure
-- Mathlib.Algebra.Ring.Commute
sq_eq_one_iff : ∀ {R : Type u} [inst : Ring R] {a : R} [NoZeroDivisors R], a ^ 2 = 1 ↔ a = 1 ∨ a = -1
-- Mathlib.GroupTheory.Solvable
Group.isSolvable_of_isSolvable_injective : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G →* G'},
  Function.Injective ⇑f → ∀ [Group.IsSolvable G'], Group.IsSolvable G
-- Lean.Expr
Lean.Nat.mkInstMul : Lean.Expr
-- Mathlib.Topology.Baire.Lemmas
/-- The intersection of finitely many open dense sets is dense.  -/
Set.Finite.dense_sInter : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (Set X)},
  s.Finite → (∀ t ∈ s, IsOpen t) → (∀ t ∈ s, Dense t) → Dense (⋂₀ s)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.lie_mem : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  {x y : L}, x ∈ L' → y ∈ L' → ⁅x, y⁆ ∈ L'
-- Mathlib.FieldTheory.Perfect
iterateFrobeniusEquiv_one_apply : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p] (x : R),
  (iterateFrobeniusEquiv R p 1) x = x ^ p
-- Mathlib.Analysis.Analytic.IsolatedZeros
HasSum.exists_hasSum_smul_of_apply_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : E} {n : ℕ} {z : 𝕜} {a : ℕ → E},
  HasSum (fun m => z ^ m • a m) s → (∀ k < n, a k = 0) → ∃ t, z ^ n • t = s ∧ HasSum (fun m => z ^ m • a (m + n)) t
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_scomp_eq_sum_orderedFinpartition : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {f : 𝕜 → 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {i : ℕ},
  ContDiffAt 𝕜 n g (f x) →
    ContDiffAt 𝕜 n f x →
      ↑i ≤ n → iteratedDeriv i (g ∘ f) x = ∑ c, (∏ j, iteratedDeriv (c.partSize j) f x) • iteratedDeriv c.length g (f x)
-- Mathlib.Analysis.Convex.Between
Wbtw.trans_left_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {w x y z : P},
  Wbtw R w y z → Wbtw R w x y → Wbtw R x y z
-- Init.Core
/-- If casting a term with `Eq.rec` to another type makes it equal to some other term, then the two
terms are heterogeneously equal.
 -/
heq_of_eqRec_eq : ∀ {α β : Sort u} {a : α} {b : β} (h₁ : α = β), h₁ ▸ a = b → a ≍ b
-- Mathlib.Order.RelClasses
Order.Preimage.instIsSymm : ∀ {α : Type u} {β : Type v} {r : α → α → Prop} [Std.Symm r] {f : β → α}, Std.Symm (f ⁻¹'o r)
-- Lean.Environment
Lean.Kernel.Diagnostics.mk.sizeOf_spec : ∀ (unfoldCounter : Lean.PHashMap Lean.Name ℕ) (enabled : Bool),
  sizeOf { unfoldCounter := unfoldCounter, enabled := enabled } = 1 + sizeOf unfoldCounter + sizeOf enabled
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mem_support_coeff_optionEquivLeft : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] {f : MvPolynomial (Option σ) R} {i : ℕ} {m : σ →₀ ℕ},
  m ∈ (((MvPolynomial.optionEquivLeft R σ) f).coeff i).support ↔ Finsupp.optionElim i m ∈ f.support
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.mem_of_insert_indep : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α}, M.IsBasis I X → e ∈ X → M.Indep (insert e I) → e ∈ I
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- Projective general linear group $PGL(n, R)$
defined as the quotient of the general linear group by its center.  -/
MatrixGroups.«termPGL(_,_)» : Lean.ParserDescr
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isPath_reverse_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.reverse.IsPath ↔ p.IsPath
-- Mathlib.Data.Tree.Traversable
BinaryTree.naturality : ∀ {α : Type u_1} {F : Type u → Type u_3} {G : Type u → Type u_4} [inst : Applicative F] [inst_1 : Applicative G]
  [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {β : Type u} (f : α → F β)
  (t : BinaryTree α), (fun {α} => η.app α) (BinaryTree.traverse f t) = BinaryTree.traverse (η.app β ∘ f) t
-- Mathlib.CategoryTheory.Category.Bipointed
pointedToBipointedSnd_comp_swap : pointedToBipointedSnd.comp Bipointed.swap = pointedToBipointedFst
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableAt.const_cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {x : E} {c : ℂ},
  DifferentiableAt ℂ f x → c ≠ 0 ∨ f x ≠ 0 → DifferentiableAt ℂ (fun x => c ^ f x) x
-- Init.Data.Option.Lemmas
Option.get_filter : ∀ {α : Type u_1} {x : Option α} {f : α → Bool} (h : (Option.filter f x).isSome = true),
  (Option.filter f x).get h = x.get ⋯
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂_map : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] (f : R →+* S₁) (g : σ → S₂) (φ : S₁ →+* S₂) (p : MvPolynomial σ R),
  MvPolynomial.eval₂ φ g ((MvPolynomial.map f) p) = MvPolynomial.eval₂ (φ.comp f) g p
-- Mathlib.RingTheory.Polynomial.GaussLemma
Polynomial.Monic.dvd_of_fraction_map_dvd_fraction_map : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K]
  [IsIntegrallyClosed R] {p q : Polynomial R},
  p.Monic → q.Monic → Polynomial.map (algebraMap R K) q ∣ Polynomial.map (algebraMap R K) p → q ∣ p
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.map_iInf : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {ι : Sort u_5} [Nonempty ι] (f : M →ₙ* N),
  Function.Injective ⇑f → ∀ (s : ι → Subsemigroup M), Subsemigroup.map f (iInf s) = ⨅ i, Subsemigroup.map f (s i)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionLiteralSupport.fromJson : Lean.Json → Except String Lean.Lsp.CodeActionLiteralSupport
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.Hom.isRingHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R₁ R₂ : CategoryTheory.CommRingObjCat C} (self : R₁.Hom R₂),
  CategoryTheory.IsRingHom self.hom
-- Mathlib.Order.KrullDimension
Order.krullDim_le_one_iff : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim α ≤ 1 ↔ ∀ (x : α), IsMin x ∨ IsMax x
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.gammaSet_one_mem_iff : ∀ (r : ℕ) (v : Fin 2 → ℤ), v ∈ EisensteinSeries.gammaSet 1 r 0 ↔ (v 0).gcd (v 1) = r
-- Mathlib.Algebra.Module.Torsion.Free
Module.isTorsionFree_nat_iff_isAddTorsionFree : ∀ {M : Type u_3} [inst : AddCommMonoid M], Module.IsTorsionFree ℕ M ↔ IsAddTorsionFree M
-- Init.Data.String.Bootstrap
List.utf8Encode.eq_1 : ∀ (l : List Char), l.utf8Encode = (List.flatMap String.utf8EncodeChar l).toByteArray
-- Mathlib.CategoryTheory.Limits.FullSubcategory
/-- If a `J`-shaped diagram in `FullSubcategory P` has a colimit cocone in `C` whose cocone point
lives in the full subcategory, then this defines a colimit in the full subcategory.  -/
CategoryTheory.Limits.createsColimitFullSubcategoryInclusion' : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {P : CategoryTheory.ObjectProperty C} →
          (F : CategoryTheory.Functor J P.FullSubcategory) →
            {c : CategoryTheory.Limits.Cocone (F.comp P.ι)} →
              CategoryTheory.Limits.IsColimit c → P c.pt → CategoryTheory.CreatesColimit F P.ι
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.filterOldMVars : Array Lean.MVarId → ℕ → Lean.MetaM (Array Lean.MVarId)
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.rightUnitor'_inv_comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : (CategoryTheory.MonoidalCategory.curriedTensor C).Additive]
  [inst_5 : ∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] {I : Type u_2}
  [inst_6 : AddMonoid I] {c : ComplexShape I} [inst_7 : c.TensorSigns] (K : HomologicalComplex C c)
  [inst_8 : DecidableEq I]
  [inst_9 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  (i j : I),
  CategoryTheory.CategoryStruct.comp (K.rightUnitor'.inv i) ((K.tensorObj (HomologicalComplex.tensorUnit C c)).d i j) =
    CategoryTheory.CategoryStruct.comp (K.d i j) (K.rightUnitor'.inv j)
-- Mathlib.Algebra.BigOperators.Group.Finset.Lemmas
Finset.even_sum : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] {s : Finset ι} (f : ι → M),
  (∀ c ∈ s, Even (f c)) → Even (∑ i ∈ s, f i)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The 2nd face of a 2-simplex, as a morphism in the 2-truncated simplex category.  -/
SSet.Truncated.δ2₂ : { obj := { len := 1 }, property := SSet.Truncated.ι0₂._proof_5 } ⟶
  { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
/-- The (topological) closure of a non-unital subalgebra of a non-unital topological algebra is
itself a non-unital subalgebra.  -/
NonUnitalSubalgebra.topologicalClosure : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : TopologicalSpace A] →
        [inst_2 : NonUnitalSemiring A] →
          [inst_3 : Module R A] →
            [ContinuousConstSMul R A] →
              [IsSemitopologicalSemiring A] → NonUnitalSubalgebra R A → NonUnitalSubalgebra R A
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- An alternative version of `Subcomplex.mk`: Instead of requiring that `E` is closed it requires
that for every cell of the subcomplex the corresponding closed cell is a subset of `E`.  -/
Topology.CWComplex.Subcomplex.mk' : {X : Type u_1} →
  [t : TopologicalSpace X] →
    [T2Space X] →
      (C : Set X) →
        [inst : Topology.CWComplex C] →
          (E : Set X) →
            (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) →
              (∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E) →
                ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E → Topology.RelCWComplex.Subcomplex C
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The middle vertex of a 2-simplex in a 2-truncated simplicial set.  -/
SSet.Truncated.ev1₂ : {V : SSet.Truncated 2} →
  V.obj (Opposite.op { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }) → SSet.OneTruncation₂ V
-- Aesop.Tree.Traversal
Aesop.postTraverseUp : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT (ST IO.RealWorld) m] →
      (Aesop.GoalRef → m Unit) → (Aesop.RappRef → m Unit) → (Aesop.MVarClusterRef → m Unit) → Aesop.TreeRef → m Unit
-- Std.Http.Protocol.H1.Config
/-- Maximum aggregate byte size of all header field lines in a single message
(name + value bytes plus 4 bytes per line for `: ` and `\r\n`). Default: 64 KiB.
 -/
Std.Http.Protocol.H1.Config.maxHeaderBytes : Std.Http.Protocol.H1.Config → ℕ
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_div_iff_right : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α} (c : α), a / c ≤ b / c ↔ a ≤ b
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_adjoint_comp_self : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (S : E →ₗ[𝕜] F),
  (LinearMap.adjoint S ∘ₗ S).IsPositive
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.one.eq_1 : ∀ {α : Type u_2} [inst : One α], Set.one = { one := {1} }
-- Lean.Elab.Parallel
_private.Lean.Elab.Parallel.0.Std.Iterators.Types.Internal.instIteratorTaskIteratorBaseIO : {α : Type} → Std.Iterator (Std.Iterators.Types.Internal.TaskIterator α) BaseIO α
-- Mathlib.Logic.Basic
forall_or_right : ∀ {α : Sort u_1} {q : Prop} {p : α → Prop}, (∀ (x : α), p x ∨ q) ↔ (∀ (x : α), p x) ∨ q
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolResult.mk.inj : ∀ {syms syms_1 : Array Lean.Lsp.DocumentSymbol}, { syms := syms } = { syms := syms_1 } → syms = syms_1
-- Lean.Parser.Term
Lean.Parser.Term.withDeclName.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.List.Permutation
_private.Mathlib.Data.List.Permutation.0.List.permutationsAux.rec.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (is : List α) (h_1 : (is : List α) → motive [] is)
  (h_2 : (t : α) → (ts is : List α) → motive (t :: ts) is),
  (match [], is with
    | [], is => h_1 is
    | t :: ts, is => h_2 t ts is) =
    h_1 is
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.congr_apply : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} {δ : Sort x} (e₁ : α ≃ β) (e₂ : γ ≃ δ) (f : α ↪ γ),
  ⇑(Function.Embedding.congr e₁ e₂ f) = ⇑(f.trans e₂.toEmbedding) ∘ ⇑e₁.symm
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
MeasureTheory.condLExp_smul : ∀ {Ω : Type u_1} {mΩ₀ mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} (X : Ω → ENNReal),
  AEMeasurable X P → ∀ (c : ENNReal), P⁻[c • X | mΩ] =ᵐ[P] c • P⁻[X | mΩ]
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.OplaxMonoidal.right_unitality_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.OplaxMonoidal.δ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.η F))
        (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom) =
    F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
-- Mathlib.Data.ENNReal.Action
ENNReal.toReal_smul : ∀ (r : NNReal) (s : ENNReal), (r • s).toReal = r • s.toReal
-- Mathlib.Algebra.Group.Pi.Basic
Pi.rightCancelMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → RightCancelMonoid (f i)] → RightCancelMonoid ((i : I) → f i)
-- Mathlib.Data.W.Basic
IsEmpty.elim'.congr_simp : ∀ {α : Sort u} {β : Sort v} (h : IsEmpty α) (a a_1 : α), a = a_1 → h.elim' a = h.elim' a_1
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the forward direction of `Equiv.Perm.sameCycle_zpow_left`. -/
Equiv.Perm.SameCycle.of_zpow_left : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} {n : ℤ}, f.SameCycle ((f ^ n) x) y → f.SameCycle x y
-- Mathlib.Algebra.Category.Grp.Basic
CategoryTheory.Iso.commGroupIsoToMulEquiv_symm_apply : ∀ {X Y : CommGrpCat} (i : X ≅ Y) (a : ↑Y), i.commGroupIsoToMulEquiv.symm a = (CommGrpCat.Hom.hom i.inv) a
-- Mathlib.Algebra.Group.Hom.Defs
/-- Any type satisfying `OneHomClass` can be cast into `OneHom` via `OneHomClass.toOneHom`.  -/
instCoeTCOneHomOfOneHomClass : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : One M] → [inst_1 : One N] → [inst_2 : FunLike F M N] → [OneHomClass F M N] → CoeTC F (OneHom M N)
-- Init.Data.Int.Order
Int.le_sub_right_of_add_le : ∀ {a b c : ℤ}, a + b ≤ c → a ≤ c - b
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.BitVec.zero_lt_iff_zero_neq : ∀ {w : ℕ} (a : BitVec w), 0#w < a ↔ a ≠ 0#w
-- Mathlib.RingTheory.TensorProduct.Basic
/-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`.  -/
Algebra.TensorProduct.includeLeft : {R : Type uR} →
  {S : Type uS} →
    {A : Type uA} →
      {B : Type uB} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : CommSemiring S] →
                    [inst_6 : Algebra S A] → [inst_7 : SMulCommClass R S A] → A →ₐ[S] TensorProduct R A B
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The canonical fan is limiting.  -/
CommRingCat.Under.piFanIsLimit : {R : CommRingCat} →
  {ι : Type u} → (P : ι → CategoryTheory.Under R) → CategoryTheory.Limits.IsLimit (CommRingCat.Under.piFan P)
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
/-- The SL-level equivariance pushed through the quotient: the image in `PSL` of
the conjugate `MulAut.conj g_SL • H` equals `MulAut.conj (mk g_SL) • (image of H)`.  -/
PSL.iwasawaT_map_conj : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  (g : Matrix.SpecialLinearGroup ι F) (H : Subgroup (Matrix.SpecialLinearGroup ι F)),
  Subgroup.map (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι F))) (MulAut.conj g • H) =
    MulAut.conj ↑g • Subgroup.map (QuotientGroup.mk' (Subgroup.center (Matrix.SpecialLinearGroup ι F))) H
-- Mathlib.CategoryTheory.Iso
/-- Notation for composition of isomorphisms.  -/
CategoryTheory.Iso.«term_≪≫_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Basis.Basic
Module.Basis.span_eq : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M), Submodule.span R (Set.range ⇑b) = ⊤
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.ReflectsLimitsOfSize.reflectsLimitsOfShape : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J], CategoryTheory.Limits.ReflectsLimitsOfShape J F
-- Init.Internal.Order.Basic
Lean.Order.PProd.chain.chain_fst : ∀ {α : Sort u} {β : Sort v} [inst : Lean.Order.CCPO α] [inst_1 : Lean.Order.CCPO β] {c : α ×' β → Prop},
  Lean.Order.chain c → Lean.Order.chain (Lean.Order.PProd.chain.fst c)
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.get! : {α : Type u} → {β : Type v} → [BEq α] → [Inhabited β] → α → (Std.DHashMap.Internal.AssocList α fun x => β) → β
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sigmaOfIsColimit_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c) (x : PUnit.{w + 1}),
  (E.sigmaOfIsColimit hc).f x = CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f
-- Mathlib.Algebra.BigOperators.Fin
/-- The product of `g i j` over `i j : Fin (n + 1)`, `i ≠ j`,
is equal to the product of `g i j * g j i` over `i < j`.

The additive version of this lemma is useful for some proofs about differential forms.
In this application, the function has the signature `f : Fin (n + 1) → Fin n → M`,
where `f i j` means `g i (Fin.succAbove i j)` in the informal statements.

Similarly, the product of `g i j * g j i` over `i < j`
is written as `f (Fin.castSucc i) j * f (Fin.succ j) i` over `i j : Fin n`, `j ≥ i`.
 -/
Fin.prod_prod_eq_prod_triangle_mul : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → Fin n → M),
  ∏ i, ∏ j, f i j = ∏ i, ∏ j ≥ i, f i.castSucc j * f j.succ i
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- Sum of a multiset of elements in an `AddSubmonoid` of an `AddCommMonoid` is
in the `AddSubmonoid`.  -/
AddSubmonoid.multiset_sum_mem : ∀ {M : Type u_4} [inst : AddCommMonoid M] (S : AddSubmonoid M) (m : Multiset M), (∀ a ∈ m, a ∈ S) → m.sum ∈ S
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.zero_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : StarAddMonoid A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : StarAddMonoid B] (a : A), 0 a = 0
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.mulRight_apply : ∀ (R : Type u_14) {A : Type u_15} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a b : A), (LinearMap.mulRight R a) b = b * a