mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.CompCLM
DifferentiableAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {G : Type u_4} [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {x : E}
  {H : Type u_5} [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {c : E → G →L[𝕜] H} {u : E → G},
  DifferentiableAt 𝕜 c x → DifferentiableAt 𝕜 u x → DifferentiableAt 𝕜 (fun y => (c y) (u y)) x
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_ssubset : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α}, t ⊆ s → t.Nonempty → s \ t ⊂ s
-- Mathlib.CategoryTheory.Category.Basic
/-- A tactic for discharging easy category theory goals, widely used as an autoparameter.
Currently this defaults to the `aesop_cat` wrapper around `aesop`, but by setting
the option `mathlib.tactic.category.grind` to `true`, it will use the `grind` tactic instead.
 -/
CategoryTheory.cat_disch : Lean.ParserDescr
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instRing : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [Ring R] → Ring (l.Germ R)
-- Mathlib.Algebra.Group.Hom.Instances
ZeroHom.instNSMul.eq_1 : ∀ {M : Type uM} {N : Type uN} [inst : Zero M] [inst_1 : AddMonoid N],
  ZeroHom.instNSMul = { smul := fun n f => { toFun := n • ⇑f, map_zero' := ⋯ } }
-- Mathlib.Analysis.Convex.Extrema
/-- A local minimum of a convex function is a global minimum, restricted to a set `s`.
 -/
IsMinOn.of_isLocalMinOn_of_convexOn : ∀ {E : Type u_1} {β : Type u_2} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : Module ℝ E]
  [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] [inst_5 : AddCommGroup β] [inst_6 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_8 : Module ℝ β] [IsOrderedModule ℝ β] [PosSMulReflectLE ℝ β] {s : Set E} {f : E → β}
  {a : E}, a ∈ s → IsLocalMinOn f s a → ConvexOn ℝ s f → IsMinOn f s a
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.mem_asSubmodule'_iff : ∀ {A : Type u_1} {G : Type u_2} {M : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid M]
  [inst_3 : Module (MonoidAlgebra A G) M] {σ : Subrepresentation (Representation.ofModule M)} {m : M},
  m ∈ σ.asSubmodule' ↔ m ∈ σ
-- Mathlib.RingTheory.SimpleModule.Basic
/-- In general, the annihilator of a simple module is called a primitive ideal, and it is
always a two-sided prime ideal, but mathlib's `Ideal.IsPrime` is not the correct definition
for noncommutative rings.  -/
IsSimpleModule.annihilator_isMaximal : ∀ {M : Type u_4} [inst : AddCommGroup M] {R : Type u_6} [inst_1 : CommRing R] [inst_2 : Module R M]
  [simple : IsSimpleModule R M], (Module.annihilator R M).IsMaximal
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.self_mem_adjoin_singleton : ∀ (R : Type uR) {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : A), x ∈ R[x]
-- Mathlib.RingTheory.Morita.Matrix
/-- The natural isomorphism showing that `toModuleCat` is the left inverse of `toMatrixModCat`.  -/
MatrixModCat.unitIso : (R : Type u) →
  {ι : Type v} →
    [inst : Ring R] →
      [inst_1 : Fintype ι] →
        [inst_2 : DecidableEq ι] →
          (i : ι) →
            (ModuleCat.toMatrixModCat R ι).comp (MatrixModCat.toModuleCat R i) ≅ CategoryTheory.Functor.id (ModuleCat R)
-- Mathlib.Order.Quotient
Quotient.instPreorder : {α : Type u_1} → {s : Setoid α} → [LE α] → Preorder (Quotient s)
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.mem_im_iff : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (hφ : Function.Injective φ.obj) {c d : D} (f : c ⟶ d),
  f ∈ (CategoryTheory.Subgroupoid.im φ hφ).arrows c d ↔
    ∃ a b g,
      ∃ (ha : φ.obj a = c) (hb : φ.obj b = d),
        f =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp (φ.map g) (CategoryTheory.eqToHom hb))
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.liftOfSurjective.eq_1 : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : AddGroup G₃]
  (f : G₁ →+ G₂) (hf : Function.Surjective ⇑f), f.liftOfSurjective hf = f.liftOfRightInverse (Function.surjInv hf) ⋯
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.to_middle_condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  {S : J.Cover X} {T : (I : S.Arrow) → J.Cover I.Y} (I : (S.bind T).Arrow), (↑(T I.fromMiddle)).arrows I.toMiddleHom
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instUnique : {α : Type u_1} → [inst : TopologicalSpace α] → [Unique α] → Unique (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- A finite module admits a surjective linear map from a finite free module.  -/
Module.Finite.exists_fin' : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M], ∃ n f, Function.Surjective ⇑f
-- Mathlib.LinearAlgebra.Dimension.Finrank
Module.finrank_le_finrank_of_rank_le_rank : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  Cardinal.lift.{w, v} (Module.rank R M) ≤ Cardinal.lift.{v, w} (Module.rank R N) →
    Module.rank R N < Cardinal.aleph0 → Module.finrank R M ≤ Module.finrank R N
-- Mathlib.Analysis.Convex.ContinuousLinearEquiv
ContinuousLinearEquiv.strictConvex_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F]
  [inst_7 : TopologicalSpace F] {s : Set E} (e : E ≃L[𝕜] F), StrictConvex 𝕜 (⇑e '' s) ↔ StrictConvex 𝕜 s
-- Mathlib.RingTheory.Etale.Basic
Algebra.FormallyEtale.of_restrictScalars : ∀ {R : Type u} {A : Type v} {B : Type u_1} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B]
  [Algebra.FormallyUnramified R A] [Algebra.FormallyEtale R B], Algebra.FormallyEtale A B
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.GetLsbDTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → Type
-- Init.Data.String.Basic
String.Slice.Pos.offset_slice : ∀ {s : String.Slice} {p₀ p₁ pos : s.Pos} {h₁ : p₀ ≤ pos} {h₂ : pos ≤ p₁},
  (pos.slice p₀ p₁ h₁ h₂).offset = pos.offset.unoffsetBy p₀.offset
-- Mathlib.Algebra.Homology.DerivedCategory.TStructure
/-- The bounded derived category of an abelian category.  -/
DerivedCategory.Bounded : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [HasDerivedCategory C] → Type (max u v)
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.UInt8.toBitVec_cond : ∀ {c : Bool} {t e : UInt8}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Mathlib.GroupTheory.GroupAction.Ring
/-- Note that `AddCommGroup.int_isScalarTower` requires stronger assumptions on `R`.  -/
NonUnitalNonAssocRing.int_isScalarTower : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R], IsScalarTower ℤ R R
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.monoidalFunctor_obj : ∀ {M : Type u} [inst : Monoid M] {N : Type u'} [inst_1 : Monoid N] (F : M →* N) (m : M),
  (CategoryTheory.Discrete.monoidalFunctor F).obj { as := m } = { as := F m }
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.trans_inv : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D E : HomologicalComplex V c} (f : HomotopyEquiv C D) (g : HomotopyEquiv D E),
  (f.trans g).inv = CategoryTheory.CategoryStruct.comp g.inv f.inv
-- Init.Core
/-- Notation type class for the set difference `\`.  -/
SDiff : Type u → Type u
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.span_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.span f g).obj CategoryTheory.Limits.WalkingSpan.right = Z
-- Mathlib.Algebra.Quaternion
Quaternion.imI_natCast : ∀ {R : Type u_3} [inst : CommRing R] (n : ℕ), (↑n).imI = 0
-- Mathlib.Algebra.Order.Ring.Basic
pow_add_pow_le : ∀ {R : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {x y : R} {n : ℕ},
  0 ≤ x → 0 ≤ y → n ≠ 0 → x ^ n + y ^ n ≤ (x + y) ^ n
-- Mathlib.Topology.EMetricSpace.Lipschitz
/-- A locally Lipschitz function is continuous. (The converse is false: for example,
$x ↦ \sqrt{x}$ is continuous, but not locally Lipschitz at 0.)  -/
LocallyLipschitz.continuous : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  LocallyLipschitz f → Continuous f
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocSemiring.toMulZeroClass : {α : Type u} → [self : NonUnitalNonAssocSemiring α] → MulZeroClass α
-- Std.Http.Transport
/-- Mock client endpoint for testing.
 -/
Std.Http.Internal.Mock.Client : Type
-- Init.System.ST
instMonadAttachEST : {ε σ : Type} → MonadAttach (EST ε σ)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.map_top : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f],
  (CategoryTheory.Subobject.map f).obj ⊤ = CategoryTheory.Subobject.mk f
-- Init.Meta.Defs
Lean.isIdFirst : Char → Bool
-- Init.Data.UInt.Lemmas
UInt64.toUSize_add : ∀ (a b : UInt64), (a + b).toUSize = a.toUSize + b.toUSize
-- Std.Time.Duration
Std.Time.Duration.instHAddOffset_5 : HAdd Std.Time.Duration Std.Time.Nanosecond.Offset Std.Time.Duration
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
_private.Mathlib.Analysis.CStarAlgebra.Module.Constructions.0.WithCStarModule.uniformity_pi_eq_aux : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {ι : Type u_2} {E : ι → Type u_3}
  [inst_2 : Fintype ι] [inst_3 : (i : ι) → NormedAddCommGroup (E i)] [inst_4 : (i : ι) → Module ℂ (E i)]
  [inst_5 : (i : ι) → SMul A (E i)] [inst_6 : (i : ι) → CStarModule A (E i)] [inst_7 : StarOrderedRing A],
  uniformity (WithCStarModule A ((i : ι) → E i)) = uniformity (WithCStarModule A ((i : ι) → E i))
-- Mathlib.Util.Export
Lean.Export.State.mk : Lean.Export.Alloc Lean.Name →
  Lean.Export.Alloc Lean.Level →
    Lean.Export.Alloc Lean.Expr → Std.HashSet Lean.Name → Array (Bool × Lean.Export.Entry) → Lean.Export.State
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
/-- the `n`-dimensional simplex can be denoted `⦋n⦌`  -/
Simplicial.«term⦋_⦌» : Lean.ParserDescr
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.startsWith_char_eq_false_iff_forall_append : ∀ {c : Char} {s : String.Slice}, s.startsWith c = false ↔ ∀ (t : String), s.copy ≠ String.singleton c ++ t
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- **Alias** of `Matrix.symm_reindexLinearEquiv`. -/
Matrix.reindexLinearEquiv_symm : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n'),
  (Matrix.reindexLinearEquiv R A eₘ eₙ).symm = Matrix.reindexLinearEquiv R A eₘ.symm eₙ.symm
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R] [Finite σ] (N : ℕ),
  Module.Finite R ↥(MvPolynomial.restrictDegree σ R N)
-- Lean.Structure
Lean.instInhabitedStructureResolutionOrderConflict.default : Lean.StructureResolutionOrderConflict
-- Mathlib.Algebra.WithConv
WithConv.instModule : {R : Type u_1} →
  {A : Type u_2} → [inst : Semiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Module R (WithConv A)
-- Mathlib.Data.Finset.Interval
Finset.Ico_eq_image_ssubsets : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α},
  s ⊆ t → Finset.Ico s t = Finset.image (fun x => s ∪ x) (t \ s).ssubsets
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.Option.get_eq_iff_eq_some : ∀ {α : Type u} {o : Option α} {h : o.isSome = true} {k : α}, o.get h = k ↔ o = some k
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInvEquiv_symm_fromLeftInv : ∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M) (hS : S ≤ IsUnit.submonoid M) (x : ↥S.leftInv),
  (S.leftInvEquiv hS).symm (S.fromLeftInv x) = x
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- A non-quantitative version of Markov inequality for integrable functions: the measure of points
where `‖f x‖ₑ > ε` is finite for all positive `ε`.  -/
MeasureTheory.Integrable.measure_norm_gt_lt_top_enorm : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} [inst : TopologicalSpace E]
  [inst_1 : ContinuousENorm E] {f : α → E},
  MeasureTheory.Integrable f μ → ∀ {ε : ENNReal}, 0 < ε → μ {x | ε < ‖f x‖ₑ} < ⊤
-- Init.Data.Vector.Lemmas
Vector.back?_empty : ∀ {α : Type u_1}, #v[].back? = none
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.comapQuotientEquivOfSurj.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (c : AddCon M) (f : N →+ M)
  (hf : Function.Surjective ⇑f),
  c.comapQuotientEquivOfSurj f hf =
    (AddCon.congr (AddEquiv.refl N) ⋯).trans (AddCon.quotientKerEquivOfSurjective (c.mk'.comp f) ⋯)
-- Mathlib.Algebra.Star.StarAlgHom
/-- Reintrepret a star algebra equivalence as a non-unital star algebra homomorphism.  -/
StarAlgEquiv.toNonUnitalStarAlgHom : {R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_3} →
      [inst : Monoid R] →
        [inst_1 : NonUnitalNonAssocSemiring A₁] →
          [inst_2 : DistribMulAction R A₁] →
            [inst_3 : Star A₁] →
              [inst_4 : NonUnitalNonAssocSemiring A₂] →
                [inst_5 : DistribMulAction R A₂] → [inst_6 : Star A₂] → (A₁ ≃⋆ₐ[R] A₂) → A₁ →⋆ₙₐ[R] A₂
-- Mathlib.Order.Interval.Finset.Nat
Nat.Ico_succ_singleton : ∀ (a : ℕ), Finset.Ico a (a + 1) = {a}
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {J : Type u} [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (iter : (i : J) → i < j → Φ.Iteration i)
  {i₁ i₂ : ↑(Set.Iio j)} (f : i₁ ⟶ i₂),
  (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem iter).map f =
    (iter ↑i₁ ⋯).mapObj (iter ↑i₂ ⋯) ⋯ ⋯ ⋯ ⋯
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkPatternCore : Lean.Expr → List Lean.Name → Array Lean.Expr → Lean.Expr → Lean.MetaM Lean.Meta.Sym.Pattern
-- Mathlib.Data.Set.Image
Set.preimage_union : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s t : Set β}, f ⁻¹' (s ∪ t) = f ⁻¹' s ∪ f ⁻¹' t
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_iff_mul_rearrangement`.

---

Two functions antivary iff the rearrangement inequality holds.  -/
Antivary.mul_add_mul_le_mul_add_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α},
  Antivary f g → ∀ (i j : ι), f i * g i + f j * g j ≤ f i * g j + f j * g i
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Alternative constructor for `isLimit`,
providing a morphism of cones rather than a morphism between the cone points
and separately the factorisation condition.
 -/
CategoryTheory.Limits.IsLimit.mkConeMorphism : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            (lift : (s : CategoryTheory.Limits.Cone F) → s ⟶ t) →
              (∀ (s : CategoryTheory.Limits.Cone F) (m : s ⟶ t), m = lift s) → CategoryTheory.Limits.IsLimit t
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Composing each term `pₙ` in a formal multilinear series with a continuous linear map `f` on the
left gives a new formal multilinear series `f.compFormalMultilinearSeries p` whose general term
is `f ∘ pₙ`.  -/
ContinuousLinearMap.compFormalMultilinearSeries : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      {G : Type x} →
        [inst : Semiring 𝕜] →
          [inst_1 : AddCommMonoid E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : ContinuousAdd E] →
                  [inst_5 : ContinuousConstSMul 𝕜 E] →
                    [inst_6 : AddCommMonoid F] →
                      [inst_7 : Module 𝕜 F] →
                        [inst_8 : TopologicalSpace F] →
                          [inst_9 : ContinuousAdd F] →
                            [inst_10 : ContinuousConstSMul 𝕜 F] →
                              [inst_11 : AddCommMonoid G] →
                                [inst_12 : Module 𝕜 G] →
                                  [inst_13 : TopologicalSpace G] →
                                    [inst_14 : ContinuousAdd G] →
                                      [inst_15 : ContinuousConstSMul 𝕜 G] →
                                        (F →L[𝕜] G) → FormalMultilinearSeries 𝕜 E F → FormalMultilinearSeries 𝕜 E G
-- Mathlib.MeasureTheory.Measure.Haar.Disintegration
/-- Given a linear map `L : E → F`, a property holds almost everywhere in `F` if and only if,
almost everywhere in `F`, it holds almost everywhere along the subspace spanned by the
image of `L`. This is an instance of a disintegration argument for additive Haar measures.  -/
MeasureTheory.ae_ae_add_linearMap_mem_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : MeasurableSpace E] [BorelSpace E] [inst_5 : NormedSpace 𝕜 E]
  [inst_6 : NormedAddCommGroup F] [inst_7 : MeasurableSpace F] [BorelSpace F] [inst_9 : NormedSpace 𝕜 F] (L : E →ₗ[𝕜] F)
  (μ : MeasureTheory.Measure E) (ν : MeasureTheory.Measure F) [μ.IsAddHaarMeasure] [ν.IsAddHaarMeasure]
  [LocallyCompactSpace E] [LocallyCompactSpace F] {s : Set F},
  MeasurableSet s → ((∀ᵐ (y : F) ∂ν, ∀ᵐ (x : E) ∂μ, y + L x ∈ s) ↔ ∀ᵐ (y : F) ∂ν, y ∈ s)
-- Mathlib.Algebra.Homology.Embedding.Basic
ComplexShape.Embedding.instIsRelIffMk' : ∀ {ι : Type u_1} {ι' : Type u_2} (c : ComplexShape ι) (c' : ComplexShape ι') (f : ι → ι') (hf : Function.Injective f)
  (iff : ∀ (i₁ i₂ : ι), c.Rel i₁ i₂ ↔ c'.Rel (f i₁) (f i₂)), (ComplexShape.Embedding.mk' c c' f hf iff).IsRelIff
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.colimitFlipIsoCompColim_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasColimitsOfShape J C]
  (F : CategoryTheory.Functor K (CategoryTheory.Functor J C)) (X : K),
  (CategoryTheory.Limits.colimitFlipIsoCompColim F).inv.app X =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.flipCompEvaluation F X)).inv
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation F.flip X).inv
-- Lean.Elab.Tactic.SimpTrace
Lean.Elab.Tactic.evalDSimpTrace : Lean.Elab.Tactic.Tactic
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- `β` is equivalent to its image in `α ⊕ β` as measurable spaces.  -/
MeasurableEquiv.Set.rangeInr : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : MeasurableSpace β] → ↑(Set.range Sum.inr) ≃ᵐ β
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.ext : ∀ {R : Type u_1} {inst : CommRing R} {K : Type u_2} {inst_1 : LieRing K} {inst_2 : LieAlgebra R K} {L : Type u_3}
  {inst_3 : LieRing L} {inst_4 : LieAlgebra R L} {x : L →ₗ⁅R⁆ LieDerivation R K K} {x_1 y : K ⋊⁅x⁆ L},
  x_1.left = y.left → x_1.right = y.right → x_1 = y
-- Mathlib.Order.MinMax
max_eq_right_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, max a b = b ↔ a ≤ b
-- Mathlib.Topology.Instances.Irrational
Irrational.instDenselyOrderedSubtypeReal : DenselyOrdered { x // Irrational x }
-- Mathlib.Order.Filter.Map
Function.LeftInverse.filter_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α},
  Function.LeftInverse g f → Function.RightInverse (Filter.comap g) (Filter.comap f)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.quotient_smul_eq : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g : G} {a : α}, ⟦g • a⟧ = ⟦a⟧
-- Mathlib.ModelTheory.Complexity
FirstOrder.Language.BoundedFormula.IsQF.below.falsum : ∀ {L : FirstOrder.Language} {α : Type u'} {n : ℕ} {motive : (a : L.BoundedFormula α n) → a.IsQF → Prop},
  FirstOrder.Language.BoundedFormula.IsQF.below ⋯
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- If `α` is an isomorphism between right adjoints, then its conjugate 2-morphism is an
isomorphism. The converse is given in `conjugateEquiv_symm_of_iso`.
 -/
CategoryTheory.Bicategory.conjugateEquiv_symm_iso : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {c d : B} {l₁ l₂ : c ⟶ d} {r₁ r₂ : d ⟶ c}
  (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁) (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (α : r₁ ⟶ r₂)
  [CategoryTheory.IsIso α], CategoryTheory.IsIso ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂).symm α)
-- Mathlib.Topology.Algebra.ConstMulAction
Filter.Tendsto.const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  {f : β → α} {l : Filter β} {a : α},
  Filter.Tendsto f l (nhds a) → ∀ (c : M), Filter.Tendsto (fun x => c • f x) l (nhds (c • a))
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.Q₂_map : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)} (h : E ≠ ⊥),
  Polynomial.map Polynomial.C (RatFunc.Luroth.Q₂✝ h) = RatFunc.Luroth.Q₁✝ h
-- Mathlib.Algebra.Group.Prod
MonoidHom.coprod_inl_inr : ∀ {M : Type u_6} {N : Type u_7} [inst : CommMonoid M] [inst_1 : CommMonoid N],
  (MonoidHom.inl M N).coprod (MonoidHom.inr M N) = MonoidHom.id (M × N)
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.lineDerivOpCLM_eq : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : AddCommGroup F]
  [inst_3 : Module ℂ F] [inst_4 : TopologicalSpace F] [inst_5 : IsTopologicalAddGroup F]
  [inst_6 : ContinuousConstSMul ℂ F] (m : E),
  LineDeriv.lineDerivOpCLM ℂ (TemperedDistribution E F) m =
    PointwiseConvergenceCLM.precomp F (-LineDeriv.lineDerivOpCLM ℂ (SchwartzMap E ℂ) m)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The **Borel Isomorphism Theorem**: If two standard Borel spaces have the same cardinality,
they are Borel isomorphic.  -/
PolishSpace.Equiv.measurableEquiv : {α : Type u_4} →
  {β : Type u_6} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → [StandardBorelSpace α] → [StandardBorelSpace β] → α ≃ β → α ≃ᵐ β
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.withBRecOnArgs.go : (Array Lean.Expr → Array Lean.Expr → Lean.MetaM Unit) →
  Lean.Meta.IndPredBelow.Context✝ → ℕ → Array Lean.Expr → Lean.MetaM Unit
-- Mathlib.Topology.Defs.Induced
Topology.isEmbedding_iff : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] (f : X → Y),
  Topology.IsEmbedding f ↔ Topology.IsInducing f ∧ Function.Injective f
-- Mathlib.Topology.MetricSpace.Dilation
/-- Alternative `Dilation` constructor when the distance hypothesis is over `nndist`  -/
Dilation.mkOfNNDistEq : {α : Type u_5} →
  {β : Type u_6} →
    [inst : PseudoMetricSpace α] →
      [inst_1 : PseudoMetricSpace β] →
        (f : α → β) → (∃ r, r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) → α →ᵈ β