mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.Convolution
SchwartzMap.fourier_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] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : MeasurableSpace E] [inst_5 : 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₃] [CompleteSpace F₃] (B : F₁ →L[𝕜] F₂ →L[𝕜] F₃) (f : SchwartzMap E F₁)
  (g : SchwartzMap E F₂),
  FourierTransform.fourier (((SchwartzMap.convolution B) f) g) =
    ((SchwartzMap.pairing B) (FourierTransform.fourier f)) (FourierTransform.fourier g)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_filterMap : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → Option (γ a)} {k : α}
  {h' : k ∈ Std.ExtDHashMap.filterMap f m}, (Std.ExtDHashMap.filterMap f m).getKey k h' = m.getKey k ⋯
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.eq_top_of_isIso_arrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} (P : CategoryTheory.Subobject Y)
  [CategoryTheory.IsIso P.arrow], P = ⊤
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.instFullLocallyRingedSpaceForgetToLocallyRingedSpace : AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.Full
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_le_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp (t.minKeyD fallback) k).isLE = true
-- Mathlib.Topology.Sheaves.EtaleSpace
TopCat.Presheaf.EtaleSpace.instTopologicalSpace : {X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {CC : C → Type v} →
        {FC : C → C → Type w} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory C FC] →
              [inst_3 : CategoryTheory.Limits.HasColimits C] → (F : TopCat.Presheaf C X) → TopologicalSpace F.EtaleSpace
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- The measure of an a.e. disjoint union (even uncountable) of null-measurable sets is at least
the sum of the measures of the sets.  -/
MeasureTheory.tsum_meas_le_meas_iUnion_of_disjoint₀ : ∀ {α : Type u_1} {ι : Type u_8} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (As i) μ) →
    Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) As) → ∑' (i : ι), μ (As i) ≤ μ (⋃ i, As i)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsAddFreimanHom.superset : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] {A : Set α} {B₁ B₂ : Set β}
  {f : α → β} {n : ℕ}, B₁ ⊆ B₂ → IsAddFreimanHom n A B₁ f → IsAddFreimanHom n A B₂ f
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.HasInvolutiveReverse.toHasReverse : {V : Type u_2} → {inst : Quiver V} → [self : Quiver.HasInvolutiveReverse V] → Quiver.HasReverse V
-- Aesop.Forward.SlotIndex
Aesop.instLTSlotIndex : LT Aesop.SlotIndex
-- Mathlib.Tactic.FunProp.FunctionData
/-- applied function arguments  -/
Mathlib.Meta.FunProp.FunctionData.args : Mathlib.Meta.FunProp.FunctionData → Array Mathlib.Meta.FunProp.Mor.Arg
-- Mathlib.GroupTheory.Coxeter.Matrix
CoxeterMatrix.symmetric : ∀ {B : Type u_1} (M : CoxeterMatrix B) (i i' : B), M.M i i' = M.M i' i
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.zero_mem_sub : ∀ {α : Type u_2} [inst : AddGroup α] {s : Set α}, s.Nonempty → 0 ∈ s - s
-- Init.Data.Nat.Basic
Nat.le_of_add_le_add_left : ∀ {a b c : ℕ}, a + b ≤ a + c → b ≤ c
-- Mathlib.Algebra.Group.Hom.Defs
/-- Copy of a `MonoidHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
MonoidHom.copy : {M : Type u_4} →
  {N : Type u_5} → [inst : MulOne M] → [inst_1 : MulOne N] → (f : M →* N) → (f' : M → N) → f' = ⇑f → M →* N
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableAdd₂ : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Add (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableAdd₂ (α i)], MeasurableAdd₂ ((i : ι) → α i)
-- Mathlib.Order.Types.Defs
OrderType.instInhabited : Inhabited OrderType.{u_1}
-- Mathlib.Algebra.Category.MonCat.Limits
AddMonCat.forget_createsLimitsOfShape : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget AddMonCat)
-- Init.Data.UInt.Bitwise
UInt64.not_xor : ∀ {a b : UInt64}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule : {R : Type u_1} →
  {A : Type u_2} →
    [inst : Star R] →
      [TrivialStar R] →
        [inst_2 : AddCommGroup A] →
          [inst_3 : StarAddMonoid A] →
            [inst_4 : Semiring R] → [inst_5 : Module R A] → [StarModule R A] → Module R ↥(selfAdjoint A)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- Given `S`-schemes `X` and `Y` such that `Y` is locally of finite type and `X` is integral,
`S`-morphisms `Spec K(X) ⟶ Y` correspond bijectively to `S`-rational maps from `X` to `Y`.
 -/
AlgebraicGeometry.Scheme.RationalMap.equivFunctionFieldOver : {X Y S : AlgebraicGeometry.Scheme} →
  [inst : X.Over S] →
    [inst_1 : Y.Over S] →
      [inst_2 : AlgebraicGeometry.IsIntegral X] →
        [AlgebraicGeometry.LocallyOfFiniteType (Y ↘ S)] →
          { f // AlgebraicGeometry.Scheme.Hom.IsOver f S } ≃ { f // AlgebraicGeometry.Scheme.RationalMap.IsOver S f }
-- Mathlib.Algebra.BigOperators.Pi
MonoidHom.functions_ext : ∀ {I : Type u_7} [inst : DecidableEq I] {M : I → Type u_8} [inst_1 : (i : I) → CommMonoid (M i)] [Finite I]
  (N : Type u_9) [inst_3 : CommMonoid N] (g h : ((i : I) → M i) →* N),
  (∀ (i : I) (x : M i), g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) → g = h
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.Normal.addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.Normal → ∀ (K : AddSubgroup G), (H.addSubgroupOf K).Normal
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
cbiInf_eq_of_forall : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] {p : ι → Prop} {f : Subtype p → α},
  (∀ (i : ι), p i) → ⨅ i, ⨅ (h : p i), f ⟨i, h⟩ = iInf f
-- Mathlib.Data.Sym.Sym2
Equiv.sigmaQuotFromRel_symm_apply_coe : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} (sym : Std.Symm r) {r' : β → β → Prop} (f : r →r r')
  (z : (b : Quot r') × ↑(Sym2.fromRel ⋯)), ↑((Equiv.sigmaQuotFromRel sym f).symm z) = Sym2.map Subtype.val ↑z.snd
-- Mathlib.FieldTheory.Perfect
powMulEquiv_mul' : ∀ (M : Type u_1) (p q : ℕ) [inst : CommMonoid M] [inst_1 : PerfectRing M p] [inst_2 : PerfectRing M q],
  powMulEquiv M (p * q) = (powMulEquiv M q).trans (powMulEquiv M p)
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
/-- A natural criterion for `HasFiniteIntegral` of a `C(Y, E)₀`-valued function is the existence
of some positive function with finite integral such that `∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x`.
Note that there is no dominated convergence here (hence no first-countability assumption
on `Y`). We are just using the properties of Banach-space-valued integration.  -/
ContinuousMapZero.hasFiniteIntegral_of_bound : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : CompactSpace Y] [inst_4 : Zero Y]
  (f : X → ContinuousMapZero Y E) (bound : X → ℝ),
  MeasureTheory.HasFiniteIntegral bound μ →
    (∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x) → MeasureTheory.HasFiniteIntegral f μ
-- Lean.Util.NumObjs
Lean.Expr.NumObjs.State.counter : Lean.Expr.NumObjs.State → ℕ
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.instRxcLawfulHasSize : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  [inst_8 : Std.Rxc.HasSize β] [Std.Rxc.LawfulHasSize β], Std.Rxc.LawfulHasSize α
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyEntourage_le_coverEntropy : ∀ {X : Type u_1} {U : SetRel X X} [inst : UniformSpace X] (T : X → X) (F : Set X),
  U ∈ uniformity X → Dynamics.coverEntropyEntourage T F U ≤ Dynamics.coverEntropy T F
-- Mathlib.Combinatorics.SetFamily.Shatter
/-- The Vapnik-Chervonenkis dimension of a set family is the maximal size of a set it shatters.  -/
Finset.vcDim : {α : Type u_1} → [DecidableEq α] → Finset (Finset α) → ℕ
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.integral_singleton : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  [MeasurableSingletonClass X] {a : X} [CompleteSpace G], ∫ᵛ (a : X) in {a}, f a ∂[B; μ] = (B (f a)) (μ {a})
-- Init.Data.Array.Monadic
Array.anyM_pure : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] [LawfulMonad m] {p : α → Bool} {xs : Array α},
  Array.anyM (fun x => pure (p x)) xs = pure (xs.any p)
-- Mathlib.Order.Basic
Prod.swap_lt_swap : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {x y : α × β}, x.swap < y.swap ↔ x < y
-- Mathlib.Topology.UniformSpace.Defs
/-- Construct a `UniformSpace.Core` from a `UniformSpace`.  -/
UniformSpace.toCore : {α : Type ua} → UniformSpace α → UniformSpace.Core α
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var
Std.Tactic.BVDecide.BVExpr.bitblast.blastVar : {w : ℕ} →
  Std.Sat.AIG Std.Tactic.BVDecide.BVBit →
    Std.Tactic.BVDecide.BVExpr.bitblast.BVVar w → Std.Sat.AIG.RefVecEntry Std.Tactic.BVDecide.BVBit w
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.NatTrans.toCatHom₂_toNatTrans : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  {F G : CategoryTheory.Functor C D} (η : F ⟶ G), (CategoryTheory.NatTrans.toCatHom₂ η).toNatTrans = η
-- Std.Internal.UV.Loop
Std.Internal.UV.Loop.Options.mk.inj : ∀ {accumulateIdleTime blockSigProfSignal accumulateIdleTime_1 blockSigProfSignal_1 : Bool},
  { accumulateIdleTime := accumulateIdleTime, blockSigProfSignal := blockSigProfSignal } =
      { accumulateIdleTime := accumulateIdleTime_1, blockSigProfSignal := blockSigProfSignal_1 } →
    accumulateIdleTime = accumulateIdleTime_1 ∧ blockSigProfSignal = blockSigProfSignal_1
-- Lean.Parser.Types
Lean.Parser.instInhabitedError.default : Lean.Parser.Error
-- Mathlib.Topology.Constructions
IsOpenMap.piMap : ∀ {ι : Type u_5} {A : ι → Type u_6} {B : ι → Type u_7} [T : (i : ι) → TopologicalSpace (A i)]
  [inst : (i : ι) → TopologicalSpace (B i)] {f : (i : ι) → A i → B i},
  (∀ (i : ι), IsOpenMap (f i)) → (∀ᶠ (i : ι) in Filter.cofinite, Function.Surjective (f i)) → IsOpenMap (Pi.map f)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.enorm_assoc : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (x : TensorProduct 𝕜 (TensorProduct 𝕜 E F) G),
  ‖(TensorProduct.assoc 𝕜 E F G) x‖ₑ = ‖x‖ₑ
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_option : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (v : Option α → M) (f : Option α →₀ R),
  (Finsupp.linearCombination R v) f = f none • v none + (Finsupp.linearCombination R (v ∘ some)) f.some
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The right adjoint of the adjunction which induces the monad `(T, η_ T, μ_ T)`.  -/
CategoryTheory.Kleisli.Adjunction.fromKleisli : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (T : CategoryTheory.Monad C) → CategoryTheory.Functor (CategoryTheory.Kleisli T) C
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_C_left : ∀ {R : Type u_1} [inst : CommRing R] (g : Polynomial R) (m n : ℕ) (r : R),
  (Polynomial.C r).resultant g m n = (-1) ^ (m * n) * g.coeff n ^ m * r ^ n
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- Distance between the images of any two points is at most twice the norm of the function.  -/
BoundedContinuousFunction.dist_le_two_norm : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) (x y : α), dist (f x) (f y) ≤ 2 * ‖f‖
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.positional.inj : ∀ {name : Lean.Name} {type : Lean.Expr} {name_1 : Lean.Name} {type_1 : Lean.Expr},
  Lean.Doc.ArgSpec.positional✝ name type = Lean.Doc.ArgSpec.positional✝ name_1 type_1 → name = name_1 ∧ type = type_1
-- Mathlib.Data.Set.Lattice.Image
Set.biUnion_range_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), ⋃ y ∈ Set.range f, f ⁻¹' {y} = Set.univ
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- `AddMonoidAlgebra.mapAlgEquiv` as an `AddMonoidHom` from `R ≃ₐ[k] R`.  -/
AddMonoidAlgebra.mapAlgAut : (R : Type u_1) →
  {A : Type u_4} →
    (M : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : AddMonoid M] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R A] → (A ≃ₐ[R] A) →* AddMonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra A M
-- Mathlib.Analysis.Calculus.FDeriv.Basic
differentiableOn_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {s : Set E}, DifferentiableOn 𝕜 id s
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.instMax : Max YoungDiagram
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxiHasSize : Std.Rxi.HasSize Int8
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.mk.inj : ∀ {A : Type u_1} {C : Type u_2} {inst : CategoryTheory.Category.{v_1, u_2} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_1} A} {ι : CategoryTheory.Functor C A} {F : CategoryTheory.Functor A C}
  {π : F.comp ι ⟶ CategoryTheory.Functor.id A}
  {epi_π_app :
    autoParam (∀ (X : A), CategoryTheory.Epi (π.app X)) CategoryTheory.Abelian.LeftResolution.epi_π_app._autoParam}
  {F_1 : CategoryTheory.Functor A C} {π_1 : F_1.comp ι ⟶ CategoryTheory.Functor.id A}
  {epi_π_app_1 :
    autoParam (∀ (X : A), CategoryTheory.Epi (π_1.app X)) CategoryTheory.Abelian.LeftResolution.epi_π_app._autoParam},
  { F := F, π := π, epi_π_app := epi_π_app } = { F := F_1, π := π_1, epi_π_app := epi_π_app_1 } → F = F_1 ∧ π ≍ π_1
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
/-- **Alias** of `IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_sdiff`.

---

If `s` is a transcendence basis and `j` is algebraic over `s ∪ {i} \ {j}`,
then `s ∪ {i} \ {j}` is also a transcendence basis.  -/
IsTranscendenceBasis.of_isAlgebraic_adjoin_insert_diff : ∀ {ι : Type u} {R : Type u_1} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [FaithfulSMul R S] [NoZeroDivisors S] (s : Set ι) (i j : ι) (v : ι → S),
  j ∈ insert i s →
    (IsTranscendenceBasis R fun x => v ↑x) →
      IsAlgebraic (↥(Algebra.adjoin R (v '' (insert i s \ {j})))) (v j) → IsTranscendenceBasis R fun x => v ↑x
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Any type satisfying `DistribMulActionSemiHomClass` can be cast into `DistribMulActionHom`
via `DistribMulActionSemiHomClass.toDistribMulActionHom`.  -/
DistribMulActionHom.instCoeTCOfAddDistribAddActionSemiHomClassCoeAddMonoidHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_4} →
            [inst_2 : AddMonoid A] →
              [inst_3 : DistribMulAction M A] →
                {B : Type u_5} →
                  [inst_4 : AddMonoid B] →
                    [inst_5 : DistribMulAction N B] →
                      {F : Type u_10} →
                        [inst_6 : FunLike F A B] → [DistribMulActionSemiHomClass F (⇑φ) A B] → CoeTC F (A →ₑ+[φ] B)
-- Mathlib.Algebra.WithConv
WithConv.instUnique : {A : Type u_2} → [Unique A] → Unique (WithConv A)
-- Mathlib.Algebra.Group.Prod
MulHom.prodMap.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {M' : Type u_6} {N' : Type u_7} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul M']
  [inst_3 : Mul N'] (f : M →ₙ* M') (g : N →ₙ* N'),
  f.prodMap g = (f.comp (MulHom.fst M N)).prod (g.comp (MulHom.snd M N))
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.digits_length_le_iff : ∀ {b k : ℕ}, 1 < b → ∀ (n : ℕ), (b.digits n).length ≤ k ↔ n < b ^ k
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.pointReflection_toAffineEquiv : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (x : P),
  (AffineIsometryEquiv.pointReflection 𝕜 x).toAffineEquiv = AffineEquiv.pointReflection 𝕜 x
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_surjective : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {v : α → M}, Function.Surjective v → Function.Surjective ⇑(Finsupp.linearCombination R v)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  CategoryTheory.Limits.imageSubobject f = CategoryTheory.Subobject.mk f
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.lift_mapRingHom_algebraMap : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : AddMonoid M]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : CommSemiring S] [inst_5 : Algebra S A] [inst_6 : Algebra R S]
  [IsScalarTower R S A] (f : Multiplicative M →* A) (x : AddMonoidAlgebra R M),
  ((AddMonoidAlgebra.lift S A M) f) ((AddMonoidAlgebra.mapRingHom M (algebraMap R S)) x) =
    ((AddMonoidAlgebra.lift R A M) f) x
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.coe_aeval : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] {a : S} [inst_2 : UniformSpace R]
  [inst_3 : UniformSpace S] [inst_4 : IsUniformAddGroup R] [inst_5 : IsTopologicalSemiring R]
  [inst_6 : IsUniformAddGroup S] [inst_7 : T2Space S] [inst_8 : CompleteSpace S] [inst_9 : IsTopologicalRing S]
  [inst_10 : IsLinearTopology S S] [inst_11 : Algebra R S] [inst_12 : ContinuousSMul R S] (ha : PowerSeries.HasEval a),
  ⇑(PowerSeries.aeval ha) = PowerSeries.eval₂ (algebraMap R S) a
-- Mathlib.Algebra.Ring.Basic
/-- Multiplication of an element of a (semi)ring is an `AddMonoidHom` in both arguments.

This is a more-strongly bundled version of `AddMonoidHom.mulLeft` and `AddMonoidHom.mulRight`.

Stronger versions of this exists for algebras as `LinearMap.mul`, `NonUnitalAlgHom.mul`
and `Algebra.lmul`.
 -/
AddMonoidHom.mul : {R : Type u_1} → [inst : NonUnitalNonAssocSemiring R] → R →+ R →+ R
-- Init.Data.Float.Float32
/-- Converts a floating-point number to a 16-bit unsigned integer.

If the given `Float32` is non-negative, truncates the value to a positive integer, rounding down and
clamping to the range of `UInt16`. Returns `0` if the `Float32` is negative or `NaN`, and returns
the largest `UInt16` value (i.e. `UInt16.size - 1`) if the float is larger than it.

This function has a logical model in terms of `Float32.Model`.
 -/
Float32.toUInt16 : Float32 → UInt16
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.toSeminormFamily_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {x : E} {y : F},
  (B.toSeminormFamily y) x = ‖(B x) y‖
-- Std.Http.Data.URI
/-- Attempts to parse a `URI` from the given string.
 -/
Std.Http.URI.parse? : String → Option Std.Http.URI
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Mem.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x : α) (t : RBTree.RBNode α),
  RBTree.RBNode.Mem cmp x t = RBTree.RBNode.MemP (cmp x) t
-- Init.Data.Nat.Coprime
Nat.coprime_div_gcd_div_gcd : ∀ {m n : ℕ}, 0 < m.gcd n → (m / m.gcd n).Coprime (n / m.gcd n)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_comp : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι} {γ : Type u_4}
  (f : β → γ), MeasureTheory.stoppedValue (fun t ω => f (u t ω)) τ = fun ω => f (MeasureTheory.stoppedValue u τ ω)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.ker_quotientMap_mk : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : I.IsTwoSided] [inst_2 : J.IsTwoSided],
  RingHom.ker (Ideal.quotientMap (Ideal.map (Ideal.Quotient.mk I) J) (Ideal.Quotient.mk I) ⋯) =
    Ideal.map (Ideal.Quotient.mk J) I
-- Lean.Parser.Basic
Lean.Parser.orelseFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Aesop.Index.RulePattern
/-- Get all substitutions of the rule patterns that match a subexpression of
the given local declaration. Subexpressions containing bound variables are not
considered.  -/
Aesop.RulePatternIndex.getInLocalDecl : Lean.LocalDecl → Aesop.RulePatternIndex → Aesop.BaseM Aesop.RulePatternSubstMap
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.mk_sub_lt_mk_right_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M},
  ArchimedeanClass.mk (a - b) < ArchimedeanClass.mk b ↔ ArchimedeanClass.mk a < ArchimedeanClass.mk b
-- Lean.DocString.Types
Lean.Doc.Block.para.sizeOf_spec : ∀ {i : Type u} {b : Type v} [inst : SizeOf i] [inst_1 : SizeOf b] (contents : Array (Lean.Doc.Inline i)),
  sizeOf (Lean.Doc.Block.para contents) = 1 + sizeOf contents
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Submartingale.stronglyMeasurable : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [inst_3 : LE E],
  MeasureTheory.Submartingale f ℱ μ → ∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)
-- Mathlib.Analysis.Convex.StrictConvexBetween
/-- An isometry of `NormedAddTorsor`s for real normed spaces, strictly convex in the case of the
codomain, is an affine isometry.  Unlike Mazur-Ulam, this does not require the isometry to be
surjective.  -/
Isometry.affineIsometryOfStrictConvexSpace : {E : Type u_3} →
  {F : Type u_4} →
    {PE : Type u_5} →
      {PF : Type u_6} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedAddCommGroup F] →
            [inst_2 : NormedSpace ℝ E] →
              [inst_3 : NormedSpace ℝ F] →
                [StrictConvexSpace ℝ E] →
                  [inst_5 : MetricSpace PE] →
                    [inst_6 : MetricSpace PF] →
                      [inst_7 : NormedAddTorsor E PE] →
                        [inst_8 : NormedAddTorsor F PF] → {f : PF → PE} → Isometry f → PF →ᵃⁱ[ℝ] PE
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instSMulCarrierMkOfSMul' : {R : Type u} →
  [inst : Ring R] → {A : AddCommGrpCat} → (φ : R →+* CategoryTheory.End A) → SMul R ↑(ModuleCat.mkOfSMul' φ)
-- Mathlib.Algebra.Opposites
AddOpposite.instAdd : {α : Type u_1} → [Add α] → Add αᵃᵒᵖ
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {A B : CommHopfAlgCat R} {f g : A ⟶ B},
  f = g ↔ CommHopfAlgCat.Hom.hom f = CommHopfAlgCat.Hom.hom g