mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lTensor_comp_cancelBaseChange : ∀ (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {N : Type uN} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid N] [inst_13 : Module R N] [inst_14 : AddCommMonoid Q] [inst_15 : Module R Q]
  [inst_16 : Algebra A B] [inst_17 : IsScalarTower A B M] (f : N →ₗ[R] Q),
  (TensorProduct.AlgebraTensorModule.lTensor B M) f ∘ₗ ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M N) =
    ↑(TensorProduct.AlgebraTensorModule.cancelBaseChange R A B M Q) ∘ₗ
      (TensorProduct.AlgebraTensorModule.lTensor B M) ((TensorProduct.AlgebraTensorModule.lTensor A A) f)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
pow_right_strictMono' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : Preorder M] [MulLeftStrictMono M] {a : M},
  1 < a → StrictMono fun x => a ^ x
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.instReprAction : {β : Type u_1} → {α : Type u_2} → [Repr β] → [Repr α] → Repr (Std.Tactic.BVDecide.LRAT.Action β α)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.lintegral_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in g • s, f x ∂μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureInformation.mk.injEq : ∀ (label : String) (documentation? : Option Lean.Lsp.MarkupContent)
  (parameters? : Option (Array Lean.Lsp.ParameterInformation)) (activeParameter? : Option ℕ) (label_1 : String)
  (documentation?_1 : Option Lean.Lsp.MarkupContent) (parameters?_1 : Option (Array Lean.Lsp.ParameterInformation))
  (activeParameter?_1 : Option ℕ),
  ({ label := label, documentation? := documentation?, parameters? := parameters?,
        activeParameter? := activeParameter? } =
      { label := label_1, documentation? := documentation?_1, parameters? := parameters?_1,
        activeParameter? := activeParameter?_1 }) =
    (label = label_1 ∧
      documentation? = documentation?_1 ∧ parameters? = parameters?_1 ∧ activeParameter? = activeParameter?_1)
-- Mathlib.Lean.ContextInfo
/-- Embeds a `CoreM` action in `CommandElabM` by supplying the information stored in `info`.

Copy of `ContextInfo.runCoreM` that makes use of the `CommandElabM` context for:
* logging messages produced by the `CoreM` action,
* metavariable generation,
* auxiliary declaration generation.
 -/
Lean.Elab.ContextInfo.runCoreMWithMessages : {α : Type} → Lean.Elab.ContextInfo → Lean.CoreM α → Lean.Elab.Command.CommandElabM α
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- Reinterpret a `NonUnitalSubsemiring` as a `Subsemigroup`.  -/
NonUnitalSubsemiring.toSubsemigroup : {R : Type u} → [inst : NonUnitalNonAssocSemiring R] → NonUnitalSubsemiring R → Subsemigroup R
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_mul : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : StrongNormalizationMonoid α] (x y : α),
  normalize (x * y) = normalize x * normalize y
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.hc₁₃ : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (self : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) (r : ℤ) (pq pq' : κ),
  (c r).Rel pq pq' →
    ∀ (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_20),
      self.i₁ pq = self.i₃ r pq' ⋯
-- Mathlib.MeasureTheory.Group.Arithmetic
measurableDiv₂_of_mul_inv : ∀ (G : Type u_2) [inst : MeasurableSpace G] [inst_1 : DivInvMonoid G] [MeasurableMul₂ G] [MeasurableInv G],
  MeasurableDiv₂ G
-- Mathlib.Order.Ideal
Order.Ideal.coe_top : ∀ {P : Type u_1} [inst : LE P] [inst_1 : IsDirectedOrder P] [inst_2 : Nonempty P], ↑⊤ = Set.univ
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- Let `r` be an element of the base ring. If `y` is a conjugate root of `x`, then `y - r` is a
conjugate root of `x - r`.
 -/
IsConjRoot.sub_algebraMap : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] {x y : S} (r : K),
  IsConjRoot K x y → IsConjRoot K (x - (algebraMap K S) r) (y - (algebraMap K S) r)
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Basic
rieszContent_ne_top : ∀ {X : Type u_1} [inst : TopologicalSpace X] (Λ : CompactlySupportedContinuousMap X NNReal →ₗ[NNReal] NNReal)
  [inst_1 : T2Space X] [inst_2 : LocallyCompactSpace X] {K : TopologicalSpace.Compacts X}, (rieszContent Λ) K ≠ ⊤
-- Init.Data.List.Basic
/-- Returns the last non-`none` result of applying `f` to each element of the list in order. Returns
`none` if `f` returns `none` for all elements of the list.

`O(|l|)`.

Examples:
 * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 5 then some (10 * x) else none) = some 20`
 * `[7, 6, 5, 8, 1, 2, 6].findSomeRev? (fun x => if x < 1 then some (10 * x) else none) = none`
 -/
List.findSomeRev? : {α : Type u} → {β : Type v} → (α → Option β) → List α → Option β
-- Init.Data.Vector.Lemmas
Vector.any_eq : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {p : α → Bool}, xs.any p = decide (∃ i, ∃ (h : i < n), p xs[i] = true)
-- Lean.Exception
Lean.MonadRecDepth.mk : {m : Type → Type} → ({α : Type} → ℕ → m α → m α) → m ℕ → m ℕ → Lean.MonadRecDepth m
-- Mathlib.Probability.Independence.Process.Basic
/-- If `X` and `Y` are two independent processes and for all `i`, `X' i` is almost everywhere equal
to `X i`, and for all `j`, `Y' j` is almost everywhere equal to `Y j`,
then `X'` is independent from `Y'`. This implies that independence results about
measurable processes should generally also hold
for processes whose marginals are only a.e.-measurable.  -/
ProbabilityTheory.Kernel.IndepFun.process_congr : ∀ {S : Type u_1} {T : Type u_2} {Ω : Type u_3} {mΩ : MeasurableSpace Ω} {α : Type u_4} {mα : MeasurableSpace α}
  {κ : ProbabilityTheory.Kernel α Ω} {P : MeasureTheory.Measure α} {𝓧 : S → Type u_5} {𝓨 : T → Type u_6}
  [inst : (i : S) → MeasurableSpace (𝓧 i)] [inst_1 : (j : T) → MeasurableSpace (𝓨 j)] {X X' : (i : S) → Ω → 𝓧 i}
  {Y Y' : (j : T) → Ω → 𝓨 j},
  ProbabilityTheory.Kernel.IndepFun (fun ω i => X i ω) (fun ω j => Y j ω) κ P →
    (∀ (i : S), ∀ᵐ (a : α) ∂P, X i =ᵐ[κ a] X' i) →
      (∀ (j : T), ∀ᵐ (a : α) ∂P, Y j =ᵐ[κ a] Y' j) →
        ProbabilityTheory.Kernel.IndepFun (fun ω i => X' i ω) (fun ω j => Y' j ω) κ P
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_tensorUnit_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.power_le_power_left : ∀ {a b c : Cardinal.{u_1}}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.conesEquiv_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.Initial.conesEquiv F G).inverse = CategoryTheory.Limits.Cone.whiskering F
-- Mathlib.Order.Closure
ClosureOperator.idempotent : ∀ {α : Type u_1} [inst : Preorder α] (c : ClosureOperator α) (x : α), c (c x) = c x
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
_private.Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart.0.LindemannWeierstrass.P_eq_integral_exp_mul_eval : ∀ (f : Polynomial ℂ) (s : ℂ),
  LindemannWeierstrass.P✝ f s =
    Complex.exp s * (s * ∫ (x : ℝ) in 0..1, Complex.exp (-(x • s)) * Polynomial.eval (x • s) f)
-- Mathlib.Analysis.Normed.Group.Basic
inseparable_one_iff_norm : ∀ {E : Type u_5} [inst : SeminormedGroup E] {a : E}, Inseparable a 1 ↔ ‖a‖ = 0
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
cauchySeq_of_edist_le_of_tsum_ne_top : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → ENNReal),
  (∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n) → tsum d ≠ ⊤ → CauchySeq f
-- Mathlib.RingTheory.Finiteness.Nilpotent
Module.End.isNilpotent_iff_of_finite : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M] {f : Module.End R M}, IsNilpotent f ↔ ∀ (m : M), ∃ n, (f ^ n) m = 0
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.WidePushoutShape.fintypeObj : {J : Type v} → [Fintype J] → Fintype (CategoryTheory.Limits.WidePushoutShape J)
-- Mathlib.Order.Hom.Set
OrderIso.image_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set β), ⇑e '' ⇑e ⁻¹' s = s
-- Mathlib.Order.Cover
CovBy.ne : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ⋖ b → a ≠ b
-- Mathlib.Data.Vector.Defs
/-- `drop` of vectors corresponds under `toList` to `drop` of lists.  -/
List.Vector.toList_drop : ∀ {α : Type u_1} {n m : ℕ} (v : List.Vector α m), (List.Vector.drop n v).toList = List.drop n v.toList
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.one_eq_id : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], 1 = LinearMap.id
-- Std.Time.Zoned
/-- Gets the current `DateTime`.
 -/
Std.Time.DateTime.now : IO Std.Time.DateTime
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.instSMulQuotient : {S : Type u_2} → (M : Type u_3) → [inst : SMul S M] → (c : SMulCon S M) → SMul S (SMulCon.Quotient M c)
-- Init.Data.UInt.Bitwise
Bool.toBitVec_toUInt32 : ∀ {b : Bool}, b.toUInt32.toBitVec = BitVec.setWidth 32 (BitVec.ofBool b)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand the square  -/
norm_add_sq : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖x + y‖ ^ 2 = ‖x‖ ^ 2 + 2 * RCLike.re (inner 𝕜 x y) + ‖y‖ ^ 2
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.inner : {α : Type u} →
  {m : Type u → Type u'} →
    {n : Type (max u v) → Type v'} →
      {β : Type u} →
        {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} →
          Std.Iterators.Types.ULiftIterator α m n β lift → Std.IterM m β
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
/-- The right localizer morphism in the Guitart exact square `iso`.  -/
_private.Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives.0.HomotopyCategory.Plus.isRightDerivabilityStructure.R : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      CategoryTheory.LocalizerMorphism (CochainComplex.Plus.quasiIso C) (HomotopyCategory.Plus.quasiIso C)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.le_preBeth_ord : ∀ (c : Cardinal.{u_1}), c ≤ Cardinal.preBeth c.ord
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsReal.comap : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (f : k →+* K) {w : NumberField.InfinitePlace K},
  w.IsReal → (w.comap f).IsReal
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
CategoryTheory.Functor.EffectivePresentation.mk.sizeOf_spec : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {X : D} [inst_2 : SizeOf C]
  [inst_3 : SizeOf D] (p : C) (f : F.obj p ⟶ X) (effectiveEpi : CategoryTheory.EffectiveEpi f),
  sizeOf { p := p, f := f, effectiveEpi := effectiveEpi } = 1 + sizeOf p + sizeOf f + sizeOf effectiveEpi
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `le_sub_iff_add_le'`. -/
add_le_of_le_sub_left : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, b ≤ c - a → a + b ≤ c
-- Init.Prelude
/-- Addition of natural numbers, typically used via the `+` operator.

This function is overridden in both the kernel and the compiler to efficiently evaluate using the
arbitrary-precision arithmetic library. The definition provided here is the logical model.
 -/
Nat.add : ℕ → ℕ → ℕ
-- Mathlib.Algebra.Order.SuccPred
Order.sub_one_lt_iff_of_not_isMin : ∀ {α : Type u_1} {x y : α} [inst : LinearOrder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α],
  ¬IsMin x → (x - 1 < y ↔ x ≤ y)
-- Mathlib.Order.Hom.Lattice
SupHom.instBot.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : Bot β],
  SupHom.instBot = { bot := SupHom.const α ⊥ }
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.sup_eq_range : ∀ {N : Type u_4} [inst : CommMonoid N] (s t : Submonoid N), s ⊔ t = MonoidHom.mrange (s.subtype.coprod t.subtype)
-- Batteries.Lean.HashMap
/-- `O(|other|)` amortized. Merge two `HashMap`s.
The values of keys which appear in both maps are combined using the monadic function `f`.
 -/
Std.HashMap.mergeWithM : {m : Type (max u_1 u_2) → Type u_3} →
  {α : Type u_2} →
    {β : Type (max u_1 u_2)} →
      [inst : BEq α] →
        [inst_1 : Hashable α] → [Monad m] → (α → β → β → m β) → Std.HashMap α β → Std.HashMap α β → m (Std.HashMap α β)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J ProfiniteAddGrp.{max v u}),
  CompactSpace ↥(ProfiniteAddGrp.limitConePtAux F)
-- Init.Data.Iterators.ToIterator
/-- Converts `x` into a pure iterator.  -/
Std.ToIterator.iter : {γ : Type u_1} → {α β : Type u_2} → [Std.ToIterator γ Id α β] → γ → Std.Iter β
-- Lean.Meta.Tactic.Generalize
/-- The `generalize` tactic takes arguments of the form `h : e = x`  -/
Lean.Meta.GeneralizeArg : Type
-- Mathlib.CategoryTheory.Localization.Predicate
/-- The canonical isomorphism `L ⋙ lift F hF L ≅ F` for any functor `F : C ⥤ E`
which inverts `W`, when `L : C ⥤ D` is a localization functor for `W`.  -/
CategoryTheory.Localization.fac : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {W : CategoryTheory.MorphismProperty C} →
          {E : Type u_3} →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
              (F : CategoryTheory.Functor C E) →
                (hF : W.IsInvertedBy F) →
                  (L : CategoryTheory.Functor C D) →
                    [inst_3 : L.IsLocalization W] → L.comp (CategoryTheory.Localization.lift F hF L) ≅ F
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Construct a morphism `Mon.mk G ⟶ Mon.mk H` from a  map `f : G ⟶ H` and a `IsMonHom f`
instance.  -/
CategoryTheory.Mon.ofHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {A B : C} →
        [inst_2 : CategoryTheory.MonObj A] →
          [inst_3 : CategoryTheory.MonObj B] →
            (f : A ⟶ B) → [CategoryTheory.IsMonHom f] → { X := A, mon := inst_2 } ⟶ { X := B, mon := inst_3 }
-- Mathlib.Logic.Equiv.Basic
Equiv.ofFiberEquiv_map : ∀ {α : Type u_13} {β : Type u_14} {γ : Type u_15} {f : α → γ} {g : β → γ}
  (e : (c : γ) → { a // f a = c } ≃ { b // g b = c }) (a : α), g ((Equiv.ofFiberEquiv e) a) = f a
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.ExtensionStateArray.containsWithSamePatterns : Lean.Meta.Grind.ExtensionStateArray →
  Lean.Meta.Grind.Origin → List Lean.Expr → List Lean.Meta.Grind.EMatchTheoremConstraint → Bool
-- Mathlib.Topology.Category.Profinite.Product
Profinite.IndexFunctor.π_app.eq_1 : ∀ {ι : Type u} {X : ι → Type} [inst : (i : ι) → TopologicalSpace (X i)] (C : Set ((i : ι) → X i)) (J : ι → Prop),
  Profinite.IndexFunctor.π_app C J =
    { toFun := Set.MapsTo.restrict (⇑(ContinuousMap.precomp Subtype.val)) C (Profinite.IndexFunctor.obj C J) ⋯,
      continuous_toFun := ⋯ }
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_bijective : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {σ : R →+* S} {σ' : S →+* R} [inst_4 : Module R M]
  [inst_5 : Module S M₂] [inst_6 : RingHomInvPair σ' σ] [inst_7 : RingHomInvPair σ σ'],
  Function.Bijective LinearEquiv.symm
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
lowerHemicontinuousAt_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α},
  LowerHemicontinuousAt (fun x => {f x}) x ↔ ContinuousAt f x
-- Init.Data.Range.Polymorphic.UInt
UInt16.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite UInt16
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierEquiv_apply : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : FourierTransformInv F E] [inst_9 : FourierPair E F]
  [inst_10 : FourierInvPair F E] (f : E), (FourierTransform.fourierEquiv R E) f = FourierTransform.fourier f
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- Given `F : SingleFunctors C D A`, and a functor `G : D ⥤ E` which commutes
with the shift by `A`, this is the "composition" of `F` and `G` in `SingleFunctors C E A`.  -/
CategoryTheory.SingleFunctors.postcomp : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            {A : Type u_5} →
              [inst_3 : AddMonoid A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  [inst_5 : CategoryTheory.HasShift E A] →
                    CategoryTheory.SingleFunctors C D A →
                      (G : CategoryTheory.Functor D E) → [G.CommShift A] → CategoryTheory.SingleFunctors C E A
-- Mathlib.Probability.Moments.Tilted
ProbabilityTheory.setIntegral_tilted_mul_eq_cgf' : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : Ω → E) {s : Set Ω},
  MeasurableSet s →
    MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
      (∫ (x : Ω) in s, g x ∂μ.tilted fun x => t * X x) =
        ∫ (x : Ω) in s, Real.exp (t * X x - ProbabilityTheory.cgf X μ t) • g x ∂μ
-- Mathlib.Data.DFinsupp.Module
DFinsupp.smulCommClass : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} {δ : Type u_1} [inst : (i : ι) → Zero (β i)]
  [inst_1 : (i : ι) → SMulZeroClass γ (β i)] [inst_2 : (i : ι) → SMulZeroClass δ (β i)]
  [∀ (i : ι), SMulCommClass γ δ (β i)], SMulCommClass γ δ (Π₀ (i : ι), β i)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftLeft
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {n w : ℕ} (aig : Std.Sat.AIG α) (distance : aig.RefVec n)
  (curr : ℕ) (acc : aig.RefVec w) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go aig distance curr acc).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftLeft.go aig distance curr acc).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Topology.Order.Basic
OrderTopology.to_orderClosedTopology : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α], OrderClosedTopology α
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM : ∀ {n : Type u_2} {A : Type u_5} [inst : NonUnitalCStarAlgebra A] [inst_1 : Fintype n] {M : CStarMatrix n n A},
  CStarMatrix.toCLMNonUnitalAlgHom M = MulOpposite.op (CStarMatrix.toCLM M)
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnModule.of_symm_sub : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_5} [inst : PartialOrder Γ] [inst_1 : SMul R V] [inst_2 : AddCommGroup V]
  (x y : HahnModule Γ R V), (HahnModule.of R).symm (x - y) = (HahnModule.of R).symm x - (HahnModule.of R).symm y
-- Mathlib.Algebra.Group.Torsion
zpow_left_injective : ∀ {G : Type u_2} [inst : Group G] [IsMulTorsionFree G] {n : ℤ}, n ≠ 0 → Function.Injective fun a => a ^ n
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpToOn.cont : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F} {s : Set E},
  HasFTaylorSeriesUpToOn n f p s → ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => p x m) s
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- curly brackets `{}` are used here instead of instance brackets `[]` because
the instance in a goal is often not the same as the one inferred by type class inference.  -/
Submonoid.card_bot : ∀ {M : Type u_1} [inst : Monoid M] {x : Fintype ↥⊥}, Fintype.card ↥⊥ = 1
-- Mathlib.RingTheory.IsTensorProduct
IsTensorProduct.map_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M₁ : Type u_2} {M₂ : Type u_3} {M : Type u_4} [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R M] {f : M₁ →ₗ[R] M₂ →ₗ[R] M} {N₁ : Type u_6} {N₂ : Type u_7} {N : Type u_8}
  [inst_7 : AddCommMonoid N₁] [inst_8 : AddCommMonoid N₂] [inst_9 : AddCommMonoid N] [inst_10 : Module R N₁]
  [inst_11 : Module R N₂] [inst_12 : Module R N] {g : N₁ →ₗ[R] N₂ →ₗ[R] N} (hf : IsTensorProduct f)
  (hg : IsTensorProduct g) (i₁ : M₁ →ₗ[R] N₁) (i₂ : M₂ →ₗ[R] N₂) (x₁ : M₁) (x₂ : M₂),
  (hf.map hg i₁ i₂) ((f x₁) x₂) = (g (i₁ x₁)) (i₂ x₂)
-- Lean.Elab.InfoTree.Basic
/-- Adds the given trailing substring to all adjacent syntax in the info tree.  -/
Lean.Elab.InfoTree.addTrailing : Substring.Raw → Lean.Elab.InfoTree → Lean.Elab.InfoTree
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.mem_of_mem_rco : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {lo hi a : α}, (a ∈ lo...hi) → a ∈ *...hi
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM_toListModel : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {m : Type u_1 → Type u_2} {δ : Type u_1}
  [inst : Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ},
  Std.DTreeMap.Internal.Impl.foldlM f init t = List.foldlM (fun acc p => f acc p.fst p.snd) init t.toListModel
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.instIsIsoFunctorUnitOfIsEquivalence_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.IsEquivalence],
  CategoryTheory.IsIso h.unit
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.toMonoidHom_injective : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], Function.Injective ContinuousMonoidHom.toMonoidHom
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.quasiFinite_algebraMap : ∀ {R : Type u_4} {S : Type u_5} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).QuasiFinite ↔ Algebra.QuasiFinite R S
-- Init.Data.Nat.Basic
Nat.zero_pow_of_pos : ∀ (n : ℕ), 0 < n → 0 ^ n = 0
-- Mathlib.NumberTheory.Modular
/-- If `1 < |z|`, then `|S • z| < 1`.  -/
ModularGroup.normSq_S_smul_lt_one : ∀ {z : UpperHalfPlane}, 1 < Complex.normSq ↑z → Complex.normSq ↑(ModularGroup.S • z) < 1