mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.isIso_Qh_map_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {X Y : HomotopyCategory C (ComplexShape.up ℤ)} (f : X ⟶ Y),
  CategoryTheory.IsIso (DerivedCategory.Qh.map f) ↔ HomotopyCategory.quasiIso C (ComplexShape.up ℤ) f
-- Init.System.IO
instOrElseEIO : {ε α : Type} → OrElse (EIO ε α)
-- Mathlib.Analysis.SpecialFunctions.Exp
ContinuousWithinAt.rexp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ} {s : Set α} {x : α},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun y => Real.exp (f y)) s x
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.imageMapComp.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  [inst_3 : CategoryTheory.Limits.HasImageMap sq] {h : CategoryTheory.Arrow C}
  [inst_4 : CategoryTheory.Limits.HasImage h.hom] (sq' : g ⟶ h) [inst_5 : CategoryTheory.Limits.HasImageMap sq'],
  CategoryTheory.Limits.imageMapComp sq sq' = CategoryTheory.Limits.imageMapComp sq sq'
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.any_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {p : (a : α) → β a → Bool}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.any p = t₂.any p
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_factors : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} (h : W ⟶ X),
  CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g →
    (CategoryTheory.Limits.equalizerSubobject f g).Factors h
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.mulArchimedean_mrange_of_isCompact_integer : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀],
  IsCompact ↑(Valued.integer K) → MulArchimedean ↥(MonoidHom.mrange Valued.v)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
/-- The linear map `Cochain K L n ≃+ Cochain (K⟦a⟧) (L⟦a⟧) n` when the category is `R`-linear.  -/
CochainComplex.HomComplex.Cochain.shiftLinearMap : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      (R : Type u_1) →
        [inst_2 : Ring R] →
          [inst_3 : CategoryTheory.Linear R C] →
            (K L : CochainComplex C ℤ) →
              (n a : ℤ) →
                CochainComplex.HomComplex.Cochain K L n →ₗ[R]
                  CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K)
                    ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n
-- Mathlib.Data.ENNReal.Basic
ENNReal.instZero : Zero ENNReal
-- Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
ZerothHomotopy.lift.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] {T : Type u_4} (f f_1 : X → T) (e_f : f = f_1)
  (hf : ∀ ⦃x y : X⦄ (x_1 : Path x y), f x = f y) (a a_1 : ZerothHomotopy X),
  a = a_1 → ZerothHomotopy.lift f hf a = ZerothHomotopy.lift f_1 ⋯ a_1
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
EuclideanGeometry.oangle_self_orthogonalProjection : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)] (p : P)
  {p' : P} {s : AffineSubspace ℝ P} [inst_5 : s.direction.HasOrthogonalProjection],
  p ∉ s →
    ∀ (h : p' ∈ s),
      p' ≠ ↑((EuclideanGeometry.orthogonalProjection s) p) →
        EuclideanGeometry.oangle p (↑((EuclideanGeometry.orthogonalProjection s) p)) p' = ↑(Real.pi / 2) ∨
          EuclideanGeometry.oangle p (↑((EuclideanGeometry.orthogonalProjection s) p)) p' = ↑(-Real.pi / 2)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Given an equivalence `e : R ≃+* S` of semirings and a subsemiring `s` of `R`,
`subsemiringMap e s` is the induced equivalence between `s` and `s.map e`  -/
RingEquiv.subsemiringMap : {R : Type u} →
  {S : Type v} →
    [inst : NonAssocSemiring R] →
      [inst_1 : NonAssocSemiring S] → (e : R ≃+* S) → (s : Subsemiring R) → ↥s ≃+* ↥(Subsemiring.map (↑e) s)
-- Mathlib.Order.LatticeIntervals
Set.Iic.coe_top : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑⊤ = a
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.rightOp : C ⥤ Dᵒᵖ` creates finite colimits, then `F : Cᵒᵖ ⥤ D` creates finite
limits.  -/
CategoryTheory.Limits.createsFiniteLimitsOfRightOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor Cᵒᵖ D) →
          [CategoryTheory.Limits.CreatesFiniteColimits F.rightOp] → CategoryTheory.Limits.CreatesFiniteLimits F
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Finset.stronglyMeasurable_fun_sum : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousAdd M]
  {m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable fun a => ∑ i ∈ s, f i a
-- Mathlib.Algebra.RingQuot
RingQuot.ringQuotToIdealQuotient_apply : ∀ {B : Type uR} [inst : CommRing B] (r : B → B → Prop) (x : B),
  (RingQuot.ringQuotToIdealQuotient r) ((RingQuot.mkRingHom r) x) = (Ideal.Quotient.mk (Ideal.ofRel r)) x
-- Mathlib.Analysis.Convex.Function
/-- A convex function on a segment is upper-bounded by the max of its endpoints.  -/
ConvexOn.le_on_segment' : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {s : Set E} {f : E → β},
  ConvexOn 𝕜 s f →
    ∀ {x y : E}, x ∈ s → y ∈ s → ∀ {a b : 𝕜}, 0 ≤ a → 0 ≤ b → a + b = 1 → f (a • x + b • y) ≤ max (f x) (f y)
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `add_tsub_add_eq_tsub_right` for the equality.  -/
add_tsub_add_le_tsub_right : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], a + c - (b + c) ≤ a - b
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_f : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (i : ℕ),
  (groupCohomology.cochainsMap f φ).f i =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (LinearMap.funLeft k ↑A fun x => ⇑f ∘ x))
      (ModuleCat.ofHom ((Rep.Hom.hom φ).compLeft (Fin i → G)))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.mk'_spec : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), f.mk' x y + f ↑y = f x
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.Functor.mapSkeleton_obj_toSkeleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : C),
  F.mapSkeleton.obj (CategoryTheory.toSkeleton X) = CategoryTheory.toSkeleton (F.obj X)
-- Mathlib.Data.Finset.Insert
Finset.insertPiProd_fst : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α} (f : α → Type u_3) (x : (i : α) → i ∈ insert a s → f i),
  (Finset.insertPiProd f x).1 = x a ⋯
-- Lean.Elab.MutualDef
Lean.Elab.instInhabitedDefViewElabHeader.default : Lean.Elab.DefViewElabHeader
-- Mathlib.Logic.Equiv.Set
Equiv.Set.insert_apply_right : ∀ {α : Type u} {s : Set α} [inst : DecidablePred fun x => x ∈ s] {a : α} (H : a ∉ s) (b : ↑s),
  (Equiv.Set.insert H) ⟨↑b, ⋯⟩ = Sum.inl b
-- Mathlib.Data.List.Sublists
List.sublists'_eq_sublists'Aux : ∀ {α : Type u} (l : List α), l.sublists' = List.foldr (fun a r => List.sublists'Aux a r r) [[]] l
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The functor `Arrow C ⥤ Arrow C` that is constructed in order to apply the small
object argument to a family of morphisms `f i : A i ⟶ B i`, see the introduction
of the file `Mathlib/CategoryTheory/SmallObject/Construction.lean`  -/
CategoryTheory.SmallObject.functor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          [CategoryTheory.Limits.HasPushouts C] →
            [∀ {X S : C} (πX : X ⟶ S),
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
              CategoryTheory.Functor (CategoryTheory.Arrow C) (CategoryTheory.Arrow C)
-- ProofWidgets.Component.HtmlDisplay
ProofWidgets.HtmlDisplayProps : Type
-- Mathlib.RepresentationTheory.Coinduced
/-- Given a monoid homomorphism `φ : G →* H` and an intertwining map `f : σ ⟶ ρ`, there is a
natural intertwining map `coind φ σ ⟶ coind φ ρ` given by postcomposition by `f`.  -/
Representation.coindMap : {k : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : Semiring k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) →
              {A : Type u_4} →
                {B : Type u_5} →
                  [inst_3 : AddCommMonoid A] →
                    [inst_4 : Module k A] →
                      [inst_5 : AddCommMonoid B] →
                        [inst_6 : Module k B] →
                          {σ : Representation k G A} →
                            {ρ : Representation k G B} →
                              σ.IntertwiningMap ρ →
                                (Representation.coind φ σ).IntertwiningMap (Representation.coind φ ρ)
-- Mathlib.LinearAlgebra.Basis.VectorSpace
/-- The atoms of the lattice of submodules of a module over a division ring are the
submodules equal to the span of a nonzero element of the module.  -/
atom_iff_nonzero_span : ∀ {K : Type u_3} {V : Type u_4} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  (W : Submodule K V), IsAtom W ↔ ∃ v, v ≠ 0 ∧ W = K ∙ v
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.instIsUnifLocDoublingMeasureRealVolume : ∀ (T : ℝ) [hT : Fact (0 < T)], IsUnifLocDoublingMeasure MeasureTheory.volume
-- Mathlib.Data.Set.Functor
Set.image_image_val_eq_domRestrict_image : ∀ {α : Type u} {β : Set α} {γ : Set ↑β} {δ : Type u_1} {f : α → δ}, f '' Subtype.val '' γ = β.domRestrict f '' γ
-- Mathlib.Probability.Distributions.Uniform
PMF.uniformOfFintype.eq_1 : ∀ (α : Type u_2) [inst : Fintype α] [inst_1 : Nonempty α], PMF.uniformOfFintype α = PMF.uniformOfFinset Finset.univ ⋯
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.ker_ofAlgEquiv : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {T : Type u_8} [inst_3 : CommRing T] [inst_4 : Algebra R T] (e : S ≃ₐ[R] T),
  (P.ofAlgEquiv e).ker = P.ker
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.mk.inj : ∀ {G : Type u_1} {inst : AddGroup G} {toAddSubgroup : AddSubgroup G}
  {isNormal' : autoParam toAddSubgroup.Normal FiniteIndexNormalAddSubgroup.isNormal'._autoParam}
  {isFiniteIndex' : autoParam toAddSubgroup.FiniteIndex FiniteIndexNormalAddSubgroup.isFiniteIndex'._autoParam}
  {toAddSubgroup_1 : AddSubgroup G}
  {isNormal'_1 : autoParam toAddSubgroup_1.Normal FiniteIndexNormalAddSubgroup.isNormal'._autoParam}
  {isFiniteIndex'_1 : autoParam toAddSubgroup_1.FiniteIndex FiniteIndexNormalAddSubgroup.isFiniteIndex'._autoParam},
  { toAddSubgroup := toAddSubgroup, isNormal' := isNormal', isFiniteIndex' := isFiniteIndex' } =
      { toAddSubgroup := toAddSubgroup_1, isNormal' := isNormal'_1, isFiniteIndex' := isFiniteIndex'_1 } →
    toAddSubgroup = toAddSubgroup_1
-- Mathlib.Topology.VectorBundle.Basic
/-- When `ϕ` is a continuous (semi)linear map between the fibers `E x` and `E' y` of two vector
bundles `E` and `E'`, `ContinuousLinearMap.inCoordinates F E F' E' x₀ x y₀ y ϕ` is a coordinate
change of this continuous linear map w.r.t. the chart around `x₀` and the chart around `y₀`.

It is defined by composing `ϕ` with appropriate coordinate changes given by the vector bundles
`E` and `E'`.
We use the operations `Bundle.Trivialization.continuousLinearMapAt` and
`Bundle.Trivialization.symmL` in the definition, instead of
`Bundle.Trivialization.continuousLinearEquivAt`, so that
`ContinuousLinearMap.inCoordinates` is defined everywhere (but see
`ContinuousLinearMap.inCoordinates_eq`).

This is the (second component of the) underlying function of a trivialization of the hom-bundle
(see `hom_trivializationAt_apply`). However, note that `ContinuousLinearMap.inCoordinates` is
defined even when `x` and `y` live in different base sets.
Therefore, it is also convenient when working with the hom-bundle between pulled back bundles.
 -/
ContinuousLinearMap.inCoordinates : {B : Type u_2} →
  (F : Type u_3) →
    (E : B → Type u_4) →
      [inst : (x : B) → AddCommMonoid (E x)] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : TopologicalSpace B] →
            [inst_3 : (x : B) → TopologicalSpace (E x)] →
              {𝕜₁ : Type u_5} →
                {𝕜₂ : Type u_6} →
                  [inst_4 : NontriviallyNormedField 𝕜₁] →
                    [inst_5 : NontriviallyNormedField 𝕜₂] →
                      {σ : 𝕜₁ →+* 𝕜₂} →
                        {B' : Type u_7} →
                          [inst_6 : TopologicalSpace B'] →
                            [inst_7 : NormedSpace 𝕜₁ F] →
                              [inst_8 : (x : B) → Module 𝕜₁ (E x)] →
                                [inst_9 : TopologicalSpace (Bundle.TotalSpace F E)] →
                                  (F' : Type u_8) →
                                    [inst_10 : NormedAddCommGroup F'] →
                                      [inst_11 : NormedSpace 𝕜₂ F'] →
                                        (E' : B' → Type u_9) →
                                          [inst_12 : (x : B') → AddCommMonoid (E' x)] →
                                            [inst_13 : (x : B') → Module 𝕜₂ (E' x)] →
                                              [inst_14 : TopologicalSpace (Bundle.TotalSpace F' E')] →
                                                [inst_15 : FiberBundle F E] →
                                                  [VectorBundle 𝕜₁ F E] →
                                                    [inst_17 : (x : B') → TopologicalSpace (E' x)] →
                                                      [inst_18 : FiberBundle F' E'] →
                                                        [VectorBundle 𝕜₂ F' E'] →
                                                          B → (x : B) → B' → (y : B') → (E x →SL[σ] E' y) → F →SL[σ] F'
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
CategoryTheory.preservesLimits_preadditiveCoyoneda_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (X : Cᵒᵖ),
  CategoryTheory.Limits.PreservesLimits (CategoryTheory.preadditiveCoyoneda.obj X)
-- Mathlib.NumberTheory.Modular
ModularGroup.lcRow0_apply : ∀ (p : Fin 2 → ℤ) (g : Matrix (Fin 2) (Fin 2) ℝ), (ModularGroup.lcRow0 p) g = ↑(p 0) * g 0 0 + ↑(p 1) * g 0 1
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
FixedDetMatrices.smul_def : ∀ (n : Type u_1) [inst : DecidableEq n] [inst_1 : Fintype n] (R : Type u_2) [inst_2 : CommRing R] (m : R)
  (g : Matrix.SpecialLinearGroup n R) (A : FixedDetMatrix n R m), g • A = ⟨↑g * ↑A, ⋯⟩
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonMulHom.eq_1 : ∀ {α : Type u_2} [inst : Mul α], Set.singletonMulHom = { toFun := singleton, map_mul' := ⋯ }
-- Mathlib.LinearAlgebra.RootSystem.Chain
OrderIso.addRight.congr_simp : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddRightMono α] (a a_1 : α),
  a = a_1 → OrderIso.addRight a = OrderIso.addRight a_1
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_diff : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.single_pos_int_one : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : DecidableEq X] {x : X},
  0 < Function.locallyFinsuppWithin.single x 1
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} [inst : Inhabited β], k ∉ m₂ → (m₁ ∪ m₂)[k]! = m₁[k]!
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instSMulCommClass : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {R : Type u_5}
  [inst_2 : Semiring R] [inst_3 : NonUnitalNonAssocSemiring β] [inst_4 : IsTopologicalSemiring β] [inst_5 : Module R β]
  [inst_6 : ContinuousConstSMul R β] [SMulCommClass R β β],
  SMulCommClass R (CompactlySupportedContinuousMap α β) (CompactlySupportedContinuousMap α β)
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.symm_eq' : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (hf : f v = 0) (hf' : autoParam ((-f) v = 0) LinearEquiv.transvection.symm_eq'._auto_1),
  (LinearEquiv.transvection hf).symm = LinearEquiv.transvection hf'
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
IsTranscendenceBasis.algebraMap_comp : ∀ {ι : Type u} {R : Type u_1} {S : Type v} {A : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [Nontrivial R]
  [NoZeroDivisors S] [Algebra.IsAlgebraic S A] [FaithfulSMul S A] {x : ι → S},
  IsTranscendenceBasis R x → IsTranscendenceBasis R (⇑(algebraMap S A) ∘ x)
-- Mathlib.Data.Finsupp.ToDFinsupp
/-- The additive version of `finsupp.toFinsupp`. Note that this is `noncomputable` because
`Finsupp.add` is noncomputable.  -/
finsuppAddEquivDFinsupp : {ι : Type u_1} →
  {M : Type u_3} → [DecidableEq ι] → [inst : AddZeroClass M] → [(m : M) → Decidable (m ≠ 0)] → (ι →₀ M) ≃+ Π₀ (x : ι), M
-- Mathlib.Algebra.Group.TypeTags.Basic
instUniqueAdditive : {α : Type u} → [Unique α] → Unique (Additive α)
-- Std.Net.Addr
Std.Net.instDecidableEqSocketAddressV4 : DecidableEq Std.Net.SocketAddressV4
-- Mathlib.Data.EReal.Inv
EReal.div_le_iff_le_mul : ∀ {a b c : EReal}, 0 < b → b ≠ ⊤ → (a / b ≤ c ↔ a ≤ b * c)
-- Lean.CoreM
/-- Wraps the given action for use in `EIO.asTask` etc., discarding its final monadic state.  -/
Lean.Core.wrapAsync : {β α : Type} → (α → Lean.CoreM β) → Option IO.CancelToken → Lean.CoreM (α → EIO Lean.Exception β)
-- Mathlib.Util.Superscript
/-- Successfully delaborates only if the resulting expression can be subscripted.

See `Mapping.subscript` in this file for legal subscript characters.  -/
Mathlib.Tactic.delabSubscript : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- If `cons (exp, coef) tl` approximates `f`, then `f` can be Majorized with exponent `exp`, and
there exists function `fC` such that `coef` approximates `fC` and `tl` approximates
`f - fC * basis_hd ^ exp`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Approximates.elim_cons : ∀ {f basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {exp : ℝ}
  {coef : Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl}
  {tl : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.cons exp coef tl) f).Approximates →
    coef.Approximates ∧
      Tactic.ComputeAsymptotics.Majorized f basis_hd exp ∧
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.instCompleteSpaceSubtypeAEEqFunMemAddSubgroupLpLpMeasSubgroupOfFactLeMeasurableSpace : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [hm : Fact (m ≤ m0)] [CompleteSpace F] [hp : Fact (1 ≤ p)],
  CompleteSpace ↥(MeasureTheory.lpMeasSubgroup F m p μ)
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
Finset.hasProd_support : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (s : Finset β) (f : β → α)
  (L : optParam (SummationFilter ↑↑s) (SummationFilter.unconditional ↑↑s)) [L.HasSupport]
  [inst_3 : DecidablePred fun x => x ∈ L.support],
  HasProd (f ∘ Subtype.val) (∏ b ∈ Finset.map (Function.Embedding.subtype fun x => x ∈ ↑s) L.support.toFinset, f b) L
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualAnnihilator_dualCoannihilator_eq : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {W : Subspace K V},
  (Submodule.dualAnnihilator W).dualCoannihilator = W
-- Mathlib.CategoryTheory.Idempotents.FunctorCategories
CategoryTheory.Idempotents.functor_category_isIdempotentComplete : ∀ (J : Type u_1) (C : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.IsIdempotentComplete C],
  CategoryTheory.IsIdempotentComplete (CategoryTheory.Functor J C)
-- Mathlib.Algebra.Group.Conj
addConj_injective : ∀ {α : Type u} [inst : AddGroup α] {x : α}, Function.Injective fun g => x + g + -x
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.mul_generator_self_inv : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_6} [inst_1 : CommRing R₁] [inst_2 : Algebra R₁ K]
  [inst_3 : IsLocalization (nonZeroDivisors R₁) K] (I : FractionalIdeal (nonZeroDivisors R₁) K)
  [inst_4 : (↑I).IsPrincipal],
  I ≠ 0 → I * FractionalIdeal.spanSingleton (nonZeroDivisors R₁) (Submodule.IsPrincipal.generator ↑I)⁻¹ = 1
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.Core.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] (P : Algebra.Presentation R S ι σ), P.Core = ↥P.core
-- Std.Async.Process
Std.IO.Process.instDecidableEqPId : DecidableEq Std.IO.Process.PId
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey!_eq_minKeyD_default : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t.minKey! = t.minKeyD default
-- Mathlib.Algebra.Category.Ring.Basic
SemiRingCat.instCoeSortType : CoeSort SemiRingCat (Type u)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The equivariant map on `SubAddAction.ofFixingAddSubgroup` given a set inclusion.  -/
SubAddAction.ofFixingAddSubgroup_of_inclusion : (M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {s t : Set α} →
          (hst : t ⊆ s) →
            ↥(SubAddAction.ofFixingAddSubgroup M s) →ₑ[⇑(AddSubgroup.inclusion ⋯)]
              ↥(SubAddAction.ofFixingAddSubgroup M t)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassPExceptSeries.eq_1 : ∀ (L : PeriodPair) (l₀ x : ℂ),
  L.derivWeierstrassPExceptSeries l₀ x =
    FormalMultilinearSeries.ofScalars ℂ fun i =>
      (↑i + 1) * (↑i + 2) * (L.sumInvPow x (i + 3) - if l₀ ∈ L.lattice then ((l₀ - x) ^ (i + 3))⁻¹ else 0)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.map_surjective : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁),
  Function.Surjective ⇑f → Function.Surjective ⇑(MvPolynomial.map f)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.smul_set_subset_mul : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a : α}, a ∈ s → a • t ⊆ s * t