mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpL2_indicator_nonneg : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} (hm : m ≤ m0)
  (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) [MeasureTheory.SigmaFinite (μ.trim hm)],
  0 ≤ᵐ[μ] ↑↑↑((MeasureTheory.condExpL2 ℝ ℝ hm) (MeasureTheory.indicatorConstLp 2 hs hμs 1))
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.forget_obj : ∀ {R : Type u} [inst : CommRing R] (A : CommBialgCat R), (CategoryTheory.forget (CommBialgCat R)).obj A = ↑A
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If a group acts properly then in particular it acts continuously.  -/
ProperSMul.toContinuousSMul : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] [ProperSMul G X], ContinuousSMul G X
-- Mathlib.Data.List.OfFn
/-- This breaks a list of `m*n` items into `n` groups each containing `m` elements.  -/
List.ofFn_mul' : ∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α),
  List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨m * ↑i + ↑j, ⋯⟩).flatten
-- Init.Data.Char.Basic
Char.isValidChar_of_isValidCharNat : ∀ (n : ℕ) (h : Char.isValidCharNat n), isValidChar (UInt32.ofNatLT n ⋯)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {c : ℝ} {g : α → F} {l : Filter α} {u : α → ℝ},
  Asymptotics.IsBigOWith c l (fun x => |u x|) g ↔ Asymptotics.IsBigOWith c l u g
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.p_descOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
  [inst_2 : S.HasRightHomology] {Z : C} (h : A ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.pOpcycles (CategoryTheory.CategoryStruct.comp (S.descOpcycles k hk) h) =
    CategoryTheory.CategoryStruct.comp k h
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.mul_adjugate : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  A * A.adjugate = A.det • 1
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.whiskerLeft : ∀ {C : Type u} (X : CategoryTheory.FreeMonoidalCategory C) {Y Z : CategoryTheory.FreeMonoidalCategory C}
  (f f' : Y.Hom Z),
  CategoryTheory.FreeMonoidalCategory.HomEquiv f f' →
    CategoryTheory.FreeMonoidalCategory.HomEquiv (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f)
      (CategoryTheory.FreeMonoidalCategory.Hom.whiskerLeft X f')
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.wrap : Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Data.Json.FromToJson.Basic
/-- Types that can be encoded as JSON.

Use `deriving ToJson`
to [automatically generate](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=deriving-instances) an instance.
The following encoding strategy is employed by auto-generated instances:

* Basic types corresponding to JSON values are encoded as these values.

  * `Bool` is encoded as `true`/`false`.

  * `String`s are encoded as JSON strings.

  * Numeric types are encoded as JSON numbers, with the exception of:

    * `UInt64` and `USize`
            which are encoded as JSON strings.
            This is because, although JSON numbers proper have unbounded range,
            in JavaScript they are parsed as [Number](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Global_Objects/Number)s
            and these can only represent integers up to $2^{53} - 1$ safely;
            so a roundtrip through JavaScript would result in truncation on these types.
            \(We use these types in the JavaScript-based Lean infoview.\)

    * Special `Float`s which are encoded as JSON strings:
            `"NaN"`/`"Infinity"`/`"-Infinity"`.

* `Unit` is encoded as `{}` \(empty JSON object\).

* `Array`s and `List`s are encoded as JSON arrays.

* `Option.none` is encoded as `null`,
    whereas  `some a` has the same encoding as `a`.
    Note that this implies `Option (Option α)` does not roundtrip,
    since `none` and `some none` both become `null`.

* General `structure`s are encoded as JSON objects in the obvious way.

  * `Option` fields whose names end with `?` have special support:
        the question mark is omitted from the JSON field name,
        and such a field is omitted from the JSON object when its value is `none`
        \(as opposed to being encoded as `{ "someField": null }`\).

* General `inductive` types are encoded on a per-constructor basis.

  * An argument-free constructor is encoded as its name \(a JSON string\).

  * A constructor with named arguments only is encoded as the JSON object
        `{ "ctorName": { "arg1": argVal1, ..., "argN": argValN } }`.

  * A constructor with one unnamed argument is encoded as the JSON object
        `{ "ctorName": argVal }`.

  * A constructor with more than one unnamed argument is encoded as the JSON object
        `{ "ctorName": [argVal1, ..., argValN] }`.

* Certain other types have special handling: see the instances below.  -/
Lean.ToJson : Type u → Type u
-- Mathlib.Logic.Encodable.Pi
/-- If `α` is encodable, then so is `Vector α n`.  -/
Encodable.List.Vector.encodable : {α : Type u_1} → [Encodable α] → {n : ℕ} → Encodable (List.Vector α n)
-- Init.Data.UInt.Bitwise
USize.toUInt64_not : ∀ (a : USize), (~~~a).toUInt64 = ~~~a.toUInt64 % UInt64.ofNat USize.size
-- Mathlib.MeasureTheory.Group.Arithmetic
Units.measurableSMul : ∀ {M : Type u_4} {β : Type u_5} [inst : MeasurableSpace β] [inst_1 : Monoid M] [inst_2 : MulAction M β]
  [inst_3 : MeasurableSpace M] [MeasurableSMul M β], MeasurableSMul Mˣ β
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
/-- An element is in the valuation ring if the norm is bounded by 1. This is a variant of
`Valuation.mem_integer_iff`, phrased using norms instead of the valuation.  -/
Valued.integer.mem_iff : ∀ {K : Type u_1} [inst : NontriviallyNormedField K] [inst_1 : IsUltrametricDist K] {x : K},
  x ∈ Valued.integer K ↔ ‖x‖ ≤ 1
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
/-- Eta-expanded form of `MeasureTheory.hasFiniteIntegral_zero` -/
MeasureTheory.hasFiniteIntegral_fun_zero : ∀ (α : Type u_1) {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε], MeasureTheory.HasFiniteIntegral (fun x => 0) μ
-- Mathlib.Data.Fin.SuccPred
Fin.castPred_mk : ∀ {n : ℕ} (i : ℕ) (h₁ : i < n) (h₂ : optParam (i < n.succ) ⋯) (h₃ : optParam (⟨i, h₂⟩ ≠ Fin.last n) ⋯),
  ⟨i, h₂⟩.castPred h₃ = ⟨i, h₁⟩
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The domain of a 2-morphism.  -/
Mathlib.Tactic.BicategoryLike.Atom.src : Mathlib.Tactic.BicategoryLike.Atom → Mathlib.Tactic.BicategoryLike.Mor₁
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.below.iUnion : ∀ {α : Type u_3} {s : Set (Set α)} {motive : (a : Set α) → MeasurableSpace.DynkinSystem.GenerateHas s a → Prop}
  {f : ℕ → Set α} (a : Pairwise (Function.onFun Disjoint f))
  (a_1 : ∀ (i : ℕ), MeasurableSpace.DynkinSystem.GenerateHas s (f i)),
  (∀ (i : ℕ), MeasurableSpace.DynkinSystem.GenerateHas.below ⋯) →
    (∀ (i : ℕ), motive (f i) ⋯) → MeasurableSpace.DynkinSystem.GenerateHas.below ⋯
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_C : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] {r : R}, (Polynomial.C r).content = normalize r
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.δ_μ_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) (i j : M)
  (X : C) [inst_3 : F.Monoidal] {Z : C} (h : (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj i j)).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F i j).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.LaxMonoidal.μ F i j).app X) h) =
    h
-- Mathlib.Algebra.Lie.TensorProduct
/-- The tensor product of two Lie modules is a Lie ring module.  -/
TensorProduct.LieModule.lieRingModule : {R : Type u} →
  [inst : CommRing R] →
    {L : Type v} →
      {M : Type w} →
        {N : Type w₁} →
          [inst_1 : LieRing L] →
            [inst_2 : LieAlgebra R L] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R M] →
                  [inst_5 : LieRingModule L M] →
                    [LieModule R L M] →
                      [inst_7 : AddCommGroup N] →
                        [inst_8 : Module R N] →
                          [inst_9 : LieRingModule L N] → [LieModule R L N] → LieRingModule L (TensorProduct R M N)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- The category over any object `X` factors through the category over the terminal object `T`.  -/
CategoryTheory.Over.forgetMapTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      {T : C} →
        (hT : CategoryTheory.Limits.IsTerminal T) →
          CategoryTheory.Over.forget X ≅
            (CategoryTheory.Over.map (hT.from X)).comp (CategoryTheory.Over.equivalenceOfIsTerminal hT).functor
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.isLimitConeOfAdj_lift : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {L : CategoryTheory.Functor (CategoryTheory.Functor J C) C} (adj : CategoryTheory.Functor.const J ⊣ L)
  (F : CategoryTheory.Functor J C) (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.isLimitConeOfAdj adj F).lift s = (adj.homEquiv s.pt F) s.π
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.filter_key_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → Bool},
  Std.ExtDHashMap.filter (fun a x => f a) m = ∅ ↔ ∀ (k : α) (h : k ∈ m), f (m.getKey k h) = false
-- Mathlib.FieldTheory.AbelRuffini
solvableByRad.rad_mem : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E} {n : ℕ},
  n ≠ 0 → x ^ n ∈ solvableByRad F E → x ∈ solvableByRad F E
-- Mathlib.Algebra.Group.Action.End
AddAut.applyAddDistribAddAction.eq_1 : ∀ {M : Type u_2} [inst : AddMonoid M],
  AddAut.applyAddDistribAddAction = { toAddAction := AddAut.applyAddAction, vadd_zero := ⋯, vadd_add := ⋯ }
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        {f : (i : I) → A i ⟶ B i} →
          {S X : C} →
            {πX : X ⟶ S} →
              (i : I) →
                (t : A i ⟶ X) →
                  (b : B i ⟶ S) →
                    CategoryTheory.CategoryStruct.comp t πX = CategoryTheory.CategoryStruct.comp (f i) b →
                      CategoryTheory.SmallObject.FunctorObjIndex f πX
-- Mathlib.Algebra.Polynomial.UnitTrinomial
/-- A unit trinomial is a trinomial with unit coefficients.  -/
Polynomial.IsUnitTrinomial : Polynomial ℤ → Prop
-- Mathlib.CategoryTheory.Presentable.Type
/-- The functor `HasCardinalLT.Set X κ ⥤ Type u` which sends a subset of `X`
of cardinality `κ` to the corresponding subtype.  -/
HasCardinalLT.Set.functor : (X : Type u) → (κ : Cardinal.{u}) → CategoryTheory.Functor (HasCardinalLT.Set X κ) (Type u)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.S_add_one : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ),
  Polynomial.Chebyshev.S R (n + 1) = Polynomial.X * Polynomial.Chebyshev.S R n - Polynomial.Chebyshev.S R (n - 1)
-- Mathlib.Algebra.DirectSum.Basic
/-- The natural map between `⨁ (i : Σ i, α i), δ i.1 i.2` and `⨁ i (j : α i), δ i j`.  -/
DirectSum.sigmaCurry : {ι : Type v} →
  [DecidableEq ι] →
    {α : ι → Type u} →
      {δ : (i : ι) → α i → Type w} →
        [inst : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
          (DirectSum ((_i : ι) × α _i) fun i => δ i.fst i.snd) →+ DirectSum ι fun i => DirectSum (α i) fun j => δ i j
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.degree_C_mul : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {a : R} [NoZeroDivisors R],
  a ≠ 0 → (Polynomial.C a * p).degree = p.degree
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cokernelSequenceE_X₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (f₁₂ : i ⟶ k)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cokernelSequenceE._auto_3),
  (X.cokernelSequenceE f₁ f₂ f₃ f₁₂ h₁₂ n₀ n₁ n₂ hn₁ hn₂).X₂ = (X.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ f₁₂)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).isEmpty = false →
        ∀ {fallback : α},
          (t.alter k f).minKeyD fallback = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_mem_sub : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α} {a b : α}, a ∈ s → b ∈ t → a - b ∈ s - t
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.ext : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  {D : Type u₂} [inst_2 : CategoryTheory.EnrichedCategory V C] [inst_3 : CategoryTheory.EnrichedCategory V D]
  {F G : CategoryTheory.EnrichedFunctor V C D} (h_obj : ∀ (X : C), F.obj X = G.obj X),
  (∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.map X Y) (CategoryTheory.eqToHom ⋯) = G.map X Y) → F = G
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.smul_eq_comap : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] (σ : Gal(K/k))
  (w : NumberField.InfinitePlace K), σ • w = w.comap ↑σ.symm
-- Mathlib.Analysis.SpecialFunctions.Bernstein
bernstein.z_zero : ∀ {n : ℕ}, bernstein.z 0 = 0
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.glue.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (sz : ℕ) (k : α) (v : β k) (l' r' : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced →
        Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size r.size →
          Sort u_3)
  (sz' : ℕ) (k' : α) (v' : β k') (l'' r'' : Std.DTreeMap.Internal.Impl α β)
  (hr : (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
      (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
            Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hr hlr)
  (h_2 :
    (sz' : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner sz k v l' r').size
                    (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'').size) →
                motive (Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'') hr hlr),
  (match Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'', hr, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hr, hlr => h_1 hr hlr
    | Std.DTreeMap.Internal.Impl.inner sz' k' v' l'' r'', hr, hlr => h_2 sz' k' v' l'' r'' hr hlr) =
    h_2 sz' k' v' l'' r'' hr hlr
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.idCompletionCore.searchAlias : (Lean.Name → Lean.Name → Bool) →
  (Lean.Name → List Lean.Name → Lean.Server.Completion.M✝ Unit) →
    Lean.Name → List Lean.Name → Lean.Name → Lean.Server.Completion.M✝ Unit
-- Lean.Meta.Basic
/-- Return the parameter names for the given global declaration.  -/
Lean.Meta.getParamNames : Lean.Name → Lean.MetaM (Array Lean.Name)
-- Mathlib.Analysis.Complex.SqrtDeriv
Complex.hasDerivAt_sqrt : ∀ {z : ℂ}, z ∈ Complex.slitPlane → HasDerivAt Complex.sqrt (z ^ (-1 / 2) / 2) z
-- Init.Meta.Defs
Lean.instQuoteNatNumLitKind : Lean.Quote ℕ Lean.numLitKind
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.split.match_1.splitter : {s : String.Slice} →
  (motive : Option s.Pos → Sort u_1) →
    (x : Option s.Pos) → ((pos : s.Pos) → x = some pos → motive (some pos)) → (x = none → motive none) → motive x
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is negative, the vectors are not equal.  -/
Orientation.ne_of_oangle_sign_eq_neg_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign = -1 → x ≠ y
-- Mathlib.RingTheory.HahnSeries.Addition
/-- Extending the domain of Hahn series is a linear map.  -/
HahnSeries.embDomainLinearMap : {Γ : Type u_1} →
  {Γ' : Type u_2} →
    {R : Type u_3} →
      [inst : PartialOrder Γ] →
        [inst_1 : Semiring R] → [inst_2 : PartialOrder Γ'] → Γ ↪o Γ' → HahnSeries Γ R →ₗ[R] HahnSeries Γ' R
-- Mathlib.RingTheory.Trace.Defs
/-- If `x` is in the base field `K`, then the trace is `[L : K] * x`.  -/
Algebra.trace_algebraMap_of_basis : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  [inst_3 : Fintype ι] (b : Module.Basis ι R S) (x : R), (Algebra.trace R S) ((algebraMap R S) x) = Fintype.card ι • x
-- Lean.Data.Lsp.Basic
Lean.Lsp.Location.range : Lean.Lsp.Location → Lean.Lsp.Range
-- Mathlib.Order.Lattice
right_lt_sup : ∀ {α : Type u} [inst : SemilatticeSup α] {a b : α}, b < a ⊔ b ↔ ¬a ≤ b
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.List.filterMap_replicate.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Init.Data.Array.Lemmas
Array.contains_filter : ∀ {α : Type u_1} [inst : BEq α] {xs : Array α} {x : α} {p : α → Bool},
  (Array.filter p xs).contains x = xs.any fun a => x == a && p a
-- Mathlib.GroupTheory.GroupAction.ConjAct
val_unitsCentralizerEquiv_symm_apply_coe : ∀ (M : Type u_2) [inst : Monoid M] (x : Mˣ) (a : ↥(MulAction.stabilizer (ConjAct Mˣ) x)),
  ↑↑((unitsCentralizerEquiv M x).symm a) = ↑(ConjAct.ofConjAct ↑a)
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.rank_inf_eq_one_of_flat_right_of_inj : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B → ∀ [Module.Flat R ↥B], Function.Injective ⇑(algebraMap R S) → Module.rank R ↥(A ⊓ B) = 1
-- Mathlib.Algebra.GroupWithZero.Action.Opposite
MulOpposite.instMulDistribMulAction : {M : Type u_1} →
  {α : Type u_2} → [inst : Monoid M] → [inst_1 : Monoid α] → [MulDistribMulAction M α] → MulDistribMulAction M αᵐᵒᵖ
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.EnoughInjectives.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∀ (X : C), Nonempty (CategoryTheory.InjectivePresentation X)) → CategoryTheory.EnoughInjectives C
-- Mathlib.Analysis.InnerProductSpace.LinearPMap
/-- The adjoint of a submodule

Note that the adjoint is taken with respect to the L^2 inner product on `E × F`, which is defined
as `WithLp 2 (E × F)`.  -/
Submodule.adjoint : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : InnerProductSpace 𝕜 F] → Submodule 𝕜 (E × F) → Submodule 𝕜 (F × E)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.forIn'_toList_eq_forIn' : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [inst_4 : Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {γ : Type u} {init : γ} {m : Type u → Type w} [inst_6 : Monad m]
  [LawfulMonad m] {f : (a : α) → a ∈ r.toList → γ → m (ForInStep γ)},
  forIn' r.toList init f = forIn' r init fun a ha acc => f a ⋯ acc
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_zero : UInt16.toBitVec 0 = 0#16
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_getElem?_eq_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  t[a]?.isSome = t.contains a
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.comul_includeRight : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Bialgebra R B] [inst_4 : Algebra R A],
  (↑(Bialgebra.comulAlgHom A (TensorProduct R A B))).comp ↑Algebra.TensorProduct.includeRight =
    (Algebra.TensorProduct.mapRingHom (algebraMap R A) ↑Algebra.TensorProduct.includeRight
          ↑Algebra.TensorProduct.includeRight ⋯ ⋯).comp
      ↑(Bialgebra.comulAlgHom R B)
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.instMonoidalSheafSheafFiber : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [inst_2 : CategoryTheory.MonoidalCategory A] →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                [CategoryTheory.LocallySmall.{w, v, u} C] →
                  [∀ (X : A),
                        CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
                          (CategoryTheory.MonoidalCategory.tensorLeft X)] →
                    [∀ (X : A),
                          CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v', u', u'}
                            (CategoryTheory.MonoidalCategory.tensorRight X)] →
                      [inst_7 : J.W.IsMonoidal] →
                        [inst_8 : CategoryTheory.HasWeakSheafify J A] →
                          [CategoryTheory.Limits.HasProducts A] → Φ.sheafFiber.Monoidal
-- Mathlib.Probability.Distributions.Poisson.Basic
ProbabilityTheory.map_cast_poissonMeasure_conv : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] {mR : MeasurableSpace R} [MeasurableAdd₂ R] (r₁ r₂ : NNReal),
  (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₁)).conv
      (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure r₂)) =
    MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.poissonMeasure (r₁ + r₂))