mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖᵒᵖ)
  (n m : ℤ) (hnm : autoParam (n + m = 0) CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso_inv_app._auto_1),
  (CategoryTheory.Pretriangulated.Opposite.UnopUnopCommShift.iso C n).inv.app X =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso C m n ⋯).hom.app (Opposite.unop X)).unop
      ((CategoryTheory.Pretriangulated.shiftFunctorOpIso Cᵒᵖ n m hnm).inv.app X).unop.unop
-- Mathlib.Algebra.Divisibility.Basic
dvd_mul : ∀ {α : Type u_1} [inst : CommSemigroup α] [DecompositionMonoid α] {k m n : α},
  k ∣ m * n ↔ ∃ d₁ d₂, d₁ ∣ m ∧ d₂ ∣ n ∧ k = d₁ * d₂
-- Lean.Data.Name
Lean.Name.isAtomic : Lean.Name → Bool
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Suggestion.name : Lean.LibrarySuggestions.Suggestion → Lean.Name
-- Mathlib.Algebra.Module.Submodule.Equiv
LinearEquiv.ofSubmodules_symm_apply : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {module_M : Module R M} {module_M₂ : Module R₂ M₂}
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} (e : M ≃ₛₗ[σ₁₂] M₂)
  {p : Submodule R M} {q : Submodule R₂ M₂} (h : Submodule.map (↑e) p = q) (x : ↥q),
  ↑((e.ofSubmodules p q h).symm x) = e.symm ↑x
-- Mathlib.Data.Fintype.Card
Fintype.card_coe : ∀ {α : Type u_1} (s : Finset α) [inst : Fintype ↥s], Fintype.card ↥s = s.card
-- Mathlib.Combinatorics.SimpleGraph.Hasse
/-- The Hasse diagram of an order as a simple graph. The graph of the covering relation.  -/
SimpleGraph.hasse : (α : Type u_1) → [Preorder α] → SimpleGraph α
-- Mathlib.Data.Finsupp.Notation
/-- `Finsupp` elaborator for `single₀`.  -/
Finsupp.Internal.elabSingle₀ : Lean.Elab.Term.TermElab
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the integer parts of the stream are at least one.  -/
GenContFract.IntFractPair.one_le_succ_nth_stream_b : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {ifp_succ_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n → 1 ≤ ifp_succ_n.b
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.subset_insert_sdiff_singleton`. -/
Set.subset_insert_diff_singleton : ∀ {α : Type u_1} (x : α) (s : Set α), s ⊆ insert x (s \ {x})
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mul_apply : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Mul (R i)] [inst_2 : ∀ (i : ι), MulMemClass (S i) (R i)]
  (x y : RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕) (i : ι), (x * y) i = x i * y i
-- Mathlib.Order.Hom.Lattice
OrderIsoClass.toSupHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : EquivLike F α β] [inst_1 : SemilatticeSup α]
  [inst_2 : SemilatticeSup β] [OrderIsoClass F α β], SupHomClass F α β
-- Init.MetaTypes
/-- If `failIfUnchanged` is `true` (default: `true`), then calls to `simp`, `dsimp`, or `simp_all`
will fail if they do not make progress.
 -/
Lean.Meta.DSimp.Config.failIfUnchanged : Lean.Meta.DSimp.Config → Bool
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.ext_iff : ∀ {n : ℕ} {x y : Composition n}, x = y ↔ x.blocks = y.blocks
-- Mathlib.Algebra.Module.CharacterModule
/-- `ℤ⋆`, the character module of `ℤ` in the unit rational circle.
 -/
CharacterModule.int : Type
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mker.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] (f : F), AddMonoidHom.mker f = AddSubmonoid.comap f ⊥
-- Mathlib.Analysis.Convex.Star
StarConvex.add_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 x s → ∀ (z : E), StarConvex 𝕜 (z + x) ((fun x => z + x) '' s)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Defs
UniqueFactorizationMonoid.of_subsingleton : ∀ (α : Type u_1) [inst : CommMonoidWithZero α] [Subsingleton α], UniqueFactorizationMonoid α
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.X_dvd_iff : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R}, PowerSeries.X ∣ φ ↔ PowerSeries.constantCoeff φ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
/-- Finite wide pullbacks are finite limits, so if `C` has all finite limits,
it also has finite wide pullbacks
 -/
CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C],
  CategoryTheory.Limits.HasFiniteWidePullbacks C
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.lt_pow_iff_log_lt : ∀ {x y : ℝ} {n : ℕ}, 0 < x → 0 < y → (x < y ^ n ↔ Real.log x < ↑n * Real.log y)
-- Mathlib.Algebra.Category.Grp.Basic
MulEquiv.toGrpIso_hom : ∀ {X Y : GrpCat} (e : ↑X ≃* ↑Y), e.toGrpIso.hom = GrpCat.ofHom e.toMonoidHom
-- Init.Core
/-- The first component of a dependent pair.
 -/
PSigma.fst : {α : Sort u} → {β : α → Sort v} → PSigma β → α
-- Init.Data.Char.Lemmas
Char.leRefl : Std.Refl fun x1 x2 => x1 ≤ x2
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.factorization_succ_le_sub_one : ∀ {p d : ℕ} [Fact (Nat.Prime p)], d ≥ 2 → (d + 1).factorization p ≤ d - 1
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.not_continuousAt_weierstrassP : ∀ (L : PeriodPair), ∀ x ∈ L.lattice, ¬ContinuousAt L.weierstrassP x
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.presentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular],
  P.IsCardinalFilteredGenerator κ →
    ∀ [CategoryTheory.LocallySmall.{w, v, u} C] (X : C), CategoryTheory.IsPresentable.{w, v, u} X
-- Mathlib.Probability.Martingale.Basic
/-- Given a discrete submartingale `f` and a predictable process `ξ` (i.e. `ξ (n + 1)` is strongly
adapted) the process defined by `fun n => ∑ k ∈ Finset.range n, ξ (k + 1) * (f (k + 1) - f k)` is
also a submartingale.  -/
MeasureTheory.Submartingale.sum_mul_sub' : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] {R : ℝ} {ξ f : ℕ → Ω → ℝ},
  MeasureTheory.Submartingale f 𝒢 μ →
    (MeasureTheory.StronglyAdapted 𝒢 fun n => ξ (n + 1)) →
      (∀ (n : ℕ) (ω : Ω), ξ n ω ≤ R) →
        (∀ (n : ℕ) (ω : Ω), 0 ≤ ξ n ω) →
          MeasureTheory.Submartingale (fun n => ∑ k ∈ Finset.range n, ξ (k + 1) * (f (k + 1) - f k)) 𝒢 μ
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.instRingQuotient : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → Ring (R ⧸ I)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.expand.eq_1 : ∀ (R : Type u) [inst : CommSemiring R] (p : ℕ),
  Polynomial.expand R p = { toRingHom := Polynomial.eval₂RingHom Polynomial.C (Polynomial.X ^ p), commutes' := ⋯ }
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.instNonemptyAlgHomOfPerfectField : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (L : Type u_2) [inst_4 : Field L] [PerfectField L] [inst_6 : Algebra F L], Nonempty (E →ₐ[F] L)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerRight_naturality_comp_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (η : F ⟶ G) {a b c : B} {a' : CategoryTheory.Cat} (f : a ⟶ b) (g : b ⟶ c) (h : G.obj c ⟶ a') (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp
      (h.toFunctor.map ((η.naturality (CategoryTheory.CategoryStruct.comp f g)).hom.toNatTrans.app X))
      (h.toFunctor.map ((G.mapComp f g).hom.toNatTrans.app ((η.app a).toFunctor.obj X))) =
    CategoryTheory.CategoryStruct.comp
      (h.toFunctor.map ((η.app c).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)))
      (CategoryTheory.CategoryStruct.comp
        (h.toFunctor.map
          (CategoryTheory.CategoryStruct.id
            ((η.app c).toFunctor.obj ((F.map g).toFunctor.obj ((F.map f).toFunctor.obj X)))))
        (CategoryTheory.CategoryStruct.comp
          (h.toFunctor.map ((η.naturality g).hom.toNatTrans.app ((F.map f).toFunctor.obj X)))
          (CategoryTheory.CategoryStruct.comp
            (h.toFunctor.map
              (CategoryTheory.CategoryStruct.id
                ((G.map g).toFunctor.obj ((η.app b).toFunctor.obj ((F.map f).toFunctor.obj X)))))
            (CategoryTheory.CategoryStruct.comp
              (h.toFunctor.map ((G.map g).toFunctor.map ((η.naturality f).hom.toNatTrans.app X)))
              (h.toFunctor.map
                (CategoryTheory.CategoryStruct.id
                  ((G.map g).toFunctor.obj ((G.map f).toFunctor.obj ((η.app a).toFunctor.obj X)))))))))
-- Mathlib.Combinatorics.Graph.Basic
Graph.bouquet_isLoopAt : ∀ {α : Type u_1} {β : Type u_2} {x : α} {e : β} (v : α) (edgeSet : Set β),
  (Graph.bouquet v edgeSet).IsLoopAt e x ↔ e ∈ edgeSet ∧ x = v
-- Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.elabLinarithConfig : Lean.Syntax → optParam Lean.Grind.LinarithConfig { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Grind.Config
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiFork_functor_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) [inst_1 : CategoryTheory.Limits.HasProduct I.left]
  [inst_2 : CategoryTheory.Limits.HasProduct I.right] {K₁ K₂ : CategoryTheory.Limits.Multifork I} (f : K₁ ⟶ K₂),
  (I.multiforkEquivPiFork.functor.map f).hom = f.hom
-- Mathlib.Topology.Covering.Basic
/-- A covering map is a continuous function `f : E → X` with discrete fibers such that each point
of `X` has an evenly covered neighborhood.  -/
IsCoveringMapOn : {E : Type u_1} → {X : Type u_2} → [TopologicalSpace E] → [TopologicalSpace X] → (E → X) → Set X → Prop
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] (f : β → α) {b : β}, {b}.sup' ⋯ f = f b
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.rnDeriv_smul_same : ∀ {α : Type u_1} {m : MeasurableSpace α} (ν μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure ν]
  [ν.HaveLebesgueDecomposition μ] {r : NNReal}, r ≠ 0 → (r • ν).rnDeriv (r • μ) =ᵐ[μ] ν.rnDeriv μ
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
/-- The q-expansion of the normalised weight-2 Eisenstein series:
`E₂(z) = 1 - 24 ∑_{n≥1} σ₁(n) qⁿ`.  -/
EisensteinSeries.E2_eq_tsum_cexp : ∀ (z : UpperHalfPlane),
  EisensteinSeries.E2 z =
    1 - 24 * ∑' (n : ℕ+), ↑((ArithmeticFunction.sigma 1) ↑n) * Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) ^ ↑n
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.add_cancel : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {r : R} {s t : ↥S},
  ↑s -ₒ t + (r -ₒ s) = r -ₒ t
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.rTensorEquiv_symm_apply_apply : ∀ {R : Type u} {M : Type v} {N : Type u_1} (P : Type u_2) (Q : Type u_3) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  (e : TensorProduct R M N ≃ₗ[R] R) (a : TensorProduct R P M →ₗ[R] TensorProduct R Q M) (x : P),
  ((Module.Invertible.rTensorEquiv P Q e).symm a) x =
    ((Module.Invertible.rightCancelEquiv Q e).congrRight (LinearMap.rTensor N a))
      ((TensorProduct.assoc R P M N).symm (x ⊗ₜ[R] e.symm 1))
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.isEmbedding_postcomp : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂]
  [inst_2 : NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [inst_3 : RingHomCompTriple σ τ ρ]
  {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜₁ E]
  [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : AddCommGroup G] [inst_9 : Module 𝕜₃ G]
  [inst_10 : TopologicalSpace E] [inst_11 : TopologicalSpace F] [inst_12 : TopologicalSpace G]
  [inst_13 : IsTopologicalAddGroup F] [inst_14 : IsTopologicalAddGroup G] (f : F →SL[τ] G),
  Topology.IsEmbedding ⇑f → Topology.IsEmbedding f.comp
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The second triangle identity for the counit and unit of the adjunction.  -/
CategoryTheory.ExponentiableMorphism.coev_ev_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  (Y : CategoryTheory.Over I) {Z : CategoryTheory.Over J}
  (h : (CategoryTheory.ExponentiableMorphism.pushforward f).obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ExponentiableMorphism.coev f).app ((CategoryTheory.ExponentiableMorphism.pushforward f).obj Y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ExponentiableMorphism.pushforward f).map ((CategoryTheory.ExponentiableMorphism.ev f).app Y))
        h) =
    h
-- Mathlib.Algebra.Group.Prod
MonoidHom.coe_prod : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (f : M →* N) (g : M →* P), ⇑(f.prod g) = Function.prod ⇑f ⇑g
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.sup_eq_map₂ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Max β] (f g : MeasureTheory.SimpleFunc α β),
  f ⊔ g = MeasureTheory.SimpleFunc.map (fun p => p.1 ⊔ p.2) (f.pair g)
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionOfMonoidalFunctorToEndofunctorMop_actionUnitIso_hom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)ᴹᵒᵖ) [inst_3 : F.Monoidal] (d : D),
  (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso d).hom =
    (CategoryTheory.Functor.OplaxMonoidal.η F).unmop.app d
-- Mathlib.RingTheory.LaurentSeries
/-- The coefficients of a Laurent series vanish in degree strictly less than its valuation.  -/
LaurentSeries.coeff_zero_of_lt_valuation : ∀ (K : Type u_2) [inst : Field K] {n D : ℤ} {f : LaurentSeries K},
  Valued.v f ≤ WithZero.exp (-D) → n < D → f.coeff n = 0
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- Given commutative rings `R, S` and a ring hom `f : R →+* S`, the extension and restriction of
scalars by `f` are adjoint to each other.
 -/
ModuleCat.extendRestrictScalarsAdj : {R : Type u₁} →
  {S : Type u₂} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] → (f : R →+* S) → ModuleCat.extendScalars f ⊣ ModuleCat.restrictScalars f
-- Mathlib.RingTheory.Smooth.StandardSmoothCotangent
Algebra.SubmersivePresentation.cotangentEquiv_apply : ∀ {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] [inst_3 : Finite σ] (P : Algebra.SubmersivePresentation R S ι σ) (x : P.toExtension.Cotangent)
  (a : σ), P.cotangentEquiv x a = P.cotangentComplexAux x a
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.forIn_iter : ∀ {α : Type v} {γ : Type u} {β : Type v} {m : Type w → Type x} [inst : Monad m] {δ : Type w}
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  {s : Std.Slice γ} {init : δ} {f : β → δ → m (ForInStep δ)}, forIn s.iter init f = forIn s init f
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ReturnCont.resultType : Lean.Elab.Do.ReturnCont → Lean.Expr
-- Std.Data.TreeSet.Raw.Iterator
Std.TreeSet.Raw.toList_iter : ∀ {α : Type u_1} {cmp : α → α → Ordering} (m : Std.TreeSet.Raw α cmp), m.iter.toList = m.toList
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- Eta-expanded form of `MeasureTheory.AEStronglyMeasurable.smul` -/
MeasureTheory.AEStronglyMeasurable.fun_smul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β},
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun i => f i • g i) μ
-- Mathlib.Algebra.Order.Sub.Defs
add_tsub_cancel_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α]
  [AddLeftReflectLE α] (a b : α), a + b - a = b
-- Mathlib.LinearAlgebra.Prod
Submodule.sndEquiv_symm_apply_coe : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (n : M₂), ↑((Submodule.sndEquiv R M M₂).symm n) = (0, n)
-- Mathlib.MeasureTheory.Measure.DiracProba
/-- In a T0 topological space `X`, the assignment `x ↦ diracProba x` is a bijection to its
range in `ProbabilityMeasure X`.  -/
MeasureTheory.diracProbaEquiv : {X : Type u_1} →
  [inst : MeasurableSpace X] →
    [inst_1 : TopologicalSpace X] → [OpensMeasurableSpace X] → [T0Space X] → X ≃ ↑(Set.range MeasureTheory.diracProba)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.instSMulHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} →
        [inst_2 : CategoryTheory.Preadditive C] →
          {R : Type u_1} →
            [inst_3 : Semiring R] →
              [inst_4 : CategoryTheory.Linear R C] →
                [∀ (n : ℤ), CategoryTheory.Functor.Linear R (CategoryTheory.shiftFunctor C n)] → SMul R (T₁ ⟶ T₂)
-- Mathlib.Data.Set.Finite.Basic
Set.card_empty : ∀ {α : Type u}, Fintype.card ↑∅ = 0
-- Mathlib.Topology.Order.LeftRightNhds
eventually_mabs_div_lt : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : CommGroup α] [inst_2 : LinearOrder α] [IsOrderedMonoid α]
  [OrderTopology α] (a : α) {ε : α}, 1 < ε → ∀ᶠ (x : α) in nhds a, |x / a|ₘ < ε
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive monoid have an addition and an additive identity.  -/
AddUnits.instAddZeroClass : {α : Type u} → [inst : AddMonoid α] → AddZeroClass (AddUnits α)
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Rcc.count_iter : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerableLE α] [Std.Rxc.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.Rxc.HasSize α] [Std.Rxc.LawfulHasSize α] {r : Std.Rcc α},
  r.iter.length = r.size
-- Init.Prelude
/-- Remove the macro scopes from the name.  -/
Lean.Name.eraseMacroScopes : Lean.Name → Lean.Name
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f` is meromorphic of infinite order at `x`, the trailing coefficient is zero by definition.
 -/
MeromorphicAt.meromorphicTrailingCoeffAt_of_order_eq_top : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, meromorphicOrderAt f x = ⊤ → meromorphicTrailingCoeffAt f x = 0
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.isClosed_topologicalClosure : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [inst_2 : SeparatelyContinuousMul M]
  (s : Subsemigroup M), IsClosed ↑s.topologicalClosure
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.add_smul_aux : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {T : Type u_1} [inst_3 : CommSemiring T] [inst_4 : Algebra R T] [inst_5 : IsLocalization S T] (x y : T)
  (p : LocalizedModule S M), (x + y) • p = x • p + y • p
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_modify : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : β → β}, m.WF → (k' ∈ m.modify k f ↔ k' ∈ m)
-- Mathlib.Algebra.Lie.OfAssociative
/-- A Lie module yields a Lie algebra morphism into the linear endomorphisms of the module.

See also `LieModule.toModuleHom`.  -/
LieModule.toEnd : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → [LieModule R L M] → L →ₗ⁅R⁆ Module.End R M
-- Mathlib.Data.EReal.Basic
EReal.toReal_zero : EReal.toReal 0 = 0
-- Mathlib.Computability.Partrec
Partrec.sumCasesOn_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
  [inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ →. σ},
  Computable f → Computable₂ g → Partrec₂ h → Partrec fun a => Sum.casesOn (f a) (fun b => Part.some (g a b)) (h a)
-- Mathlib.Algebra.Homology.TotalComplex
/-- The inclusion of a summand in the total complex, or zero if the degrees do not match.  -/
HomologicalComplex₂.ιTotalOrZero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  (c₁₂ : ComplexShape I₁₂) →
                    [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                      [inst_3 : DecidableEq I₁₂] →
                        [inst_4 : K.HasTotal c₁₂] →
                          (i₁ : I₁) → (i₂ : I₂) → (i₁₂ : I₁₂) → (K.X i₁).X i₂ ⟶ (K.total c₁₂).X i₁₂
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trPosNum.match_1.eq_2 : ∀ (motive : PosNum → Sort u_1) (n : PosNum) (h_1 : Unit → motive PosNum.one) (h_2 : (n : PosNum) → motive n.bit0)
  (h_3 : (n : PosNum) → motive n.bit1),
  (match n.bit0 with
    | PosNum.one => h_1 ()
    | n.bit0 => h_2 n
    | n.bit1 => h_3 n) =
    h_2 n
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.mem_succ_iff : ∀ {α : Type u} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.PRange.LinearlyUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_4 : Std.PRange.InfinitelyUpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α]
  [Std.PRange.LawfulUpwardEnumerable α] {lo a : α},
  a ∈ (Std.PRange.succ lo)<...* ↔ ∃ a', a = Std.PRange.succ a' ∧ a' ∈ lo<...*
-- Mathlib.Data.Set.Operations
Set.notMem_ofPred_iff : ∀ {α : Type u} {a : α} {p : α → Prop}, a ∉ {x | p x} ↔ ¬p a
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.tensorHom_left_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  {R S T U : CategoryTheory.Over X} (f : R ⟶ S) (g : T ⟶ U),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.ChosenPullbacksAlong.fst S.hom U.hom) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst R.hom T.hom)
      (CategoryTheory.Over.Hom.left f)