mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalSourceTargetProperty
/-- If `P` is a local property, by monotonicity w.r.t. restricting `domChart`,
if `f` is continuous at `x`, to prove `LiftSourceTargetPropertyAt I I' n f x P`
we need not check the condition `f '' domChart.source ⊆ codChart.source`.  -/
Manifold.LiftSourceTargetPropertyAt.mk_of_continuousAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_4} {H : Type u_6} {G : Type u_8} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H} {J : ModelWithCorners 𝕜 F G}
  {M : Type u_10} {N : Type u_12} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  {P : (M → N) → OpenPartialHomeomorph M H → OpenPartialHomeomorph N G → Prop},
  ContinuousAt f x →
    Manifold.IsLocalSourceTargetProperty P →
      ∀ (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
        x ∈ domChart.source →
          f x ∈ codChart.source →
            domChart ∈ IsManifold.maximalAtlas I n M →
              codChart ∈ IsManifold.maximalAtlas J n N →
                P f domChart codChart → Manifold.LiftSourceTargetPropertyAt I J n f x P
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intAdicAbv_le_one : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R)
  {b : NNReal} (hb : 1 < b) (r : R), (v.intAdicAbv hb) r ≤ 1
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.comp_mul : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LinearOrderedCommMonoidWithZero α]
  [inst_1 : LinearOrderedCommMonoidWithZero β] [inst_2 : LinearOrderedCommMonoidWithZero γ] (g : β →*₀o γ)
  (f₁ f₂ : α →*₀o β), g.comp (f₁ * f₂) = g.comp f₁ * g.comp f₂
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_lt_mul_iff_left₀`. -/
mul_lt_mul_iff_of_pos_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosStrictMono α]
  [MulPosReflectLT α], 0 < a → (b * a < c * a ↔ b < c)
-- Std.Data.ExtTreeSet.Basic
/-- Checks whether an element is present in a set and inserts the element if it was not found.
If the tree set already contains an element that is equal (with regard to `cmp` to the given
element, then the tree set is returned unchanged.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.ExtTreeSet.containsThenInsert : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → Bool × Std.ExtTreeSet α cmp
-- Init.Grind.AC
Lean.Grind.AC.Seq.denote_union : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (s₁ s₂ : Lean.Grind.AC.Seq),
  Lean.Grind.AC.Seq.denote ctx (s₁.union s₂) =
    ctx.op (Lean.Grind.AC.Seq.denote ctx s₁) (Lean.Grind.AC.Seq.denote ctx s₂)
-- Mathlib.Data.Num.Bitwise
/-- Bitwise "xor" for `Num`.  -/
Num.lxor : Num → Num → Num
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.step_dropWhileWithPostcondition : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → Std.Iterators.PostconditionT m (ULift.{u_1, 0} Bool)},
  (Std.IterM.dropWhileWithPostcondition P it).step = do
    let __do_lift ← it.step
    match __do_lift.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ => do
        let __do_lift ← (P out).operation
        match __do_lift with
          | ⟨{ down := true }, h''⟩ =>
            pure
              (Std.Shrink.deflate
                (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileWithPostcondition P true it') ⋯))
          | ⟨{ down := false }, h''⟩ =>
            pure
              (Std.Shrink.deflate
                (Std.PlausibleIterStep.yield (Std.IterM.Intermediate.dropWhileWithPostcondition P false it') out ⋯))
      | ⟨Std.IterStep.skip it', h⟩ =>
        pure
          (Std.Shrink.deflate
            (Std.PlausibleIterStep.skip (Std.IterM.Intermediate.dropWhileWithPostcondition P true it') ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Order.Cover
Set.Iio_eq_singleton_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio a = {b} ↔ IsBot b ∧ b ⋖ a
-- Mathlib.Analysis.Convex.Between
sbtw_one_zero_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedRing R] {x : R}, Sbtw R 1 x 0 ↔ x ∈ Set.Ioo 0 1
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.Precheck.Context.mk.sizeOf_spec : ∀ (quotLCtx : Lean.NameSet), sizeOf { quotLCtx := quotLCtx } = 1 + sizeOf quotLCtx
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.functorPullback_mem : ∀ {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} (R : CategoryTheory.Presieve (F.obj X)) {Y : C} (f : Y ⟶ X),
  CategoryTheory.Presieve.functorPullback F R f ↔ R (F.map f)
-- Mathlib.RingTheory.RingHom.FiniteType
RingHom.finiteType_isStableUnderBaseChange : RingHom.IsStableUnderBaseChange @RingHom.FiniteType
-- Mathlib.Data.TypeVec
TypeVec.const_append1 : ∀ {β : Type u_1} {γ : Type u_2} (x : γ) {n : ℕ} (α : TypeVec.{u_1} n),
  TypeVec.const x (α ::: β) = (TypeVec.const x α ::: fun x_1 => x)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- Given a continuous `𝕜`-bilinear map `B : F₁ →L[𝕜] F₂ →L[𝕜] F₃`, a measure `μ` on `E`,
and a function `φ : E → F₂` which is `μ`-integrable on `K`, this is the `𝕜`-linear map
`f ↦ ∫ x, B (f x) (φ x) ∂μ` from `𝓓^{n}_{K}(E, F₁)` to `F₃`. Otherwise, this is the zero map.

You should probably use `integralAgainstBilinCLM`, which bundles the continuity.  -/
ContDiffMapSupportedIn.integralAgainstBilinLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {n : ℕ∞} →
            {K : TopologicalSpace.Compacts E} →
              {m : MeasurableSpace E} →
                [OpensMeasurableSpace E] →
                  {F₁ : Type u_5} →
                    {F₂ : Type u_6} →
                      {F₃ : Type u_7} →
                        [inst_4 : NormedAddCommGroup F₁] →
                          [inst_5 : NormedSpace 𝕜 F₁] →
                            [inst_6 : NormedSpace ℝ F₁] →
                              [inst_7 : NormedAddCommGroup F₂] →
                                [inst_8 : NormedSpace 𝕜 F₂] →
                                  [inst_9 : NormedAddCommGroup F₃] →
                                    [inst_10 : NormedSpace 𝕜 F₃] →
                                      [inst_11 : SMulCommClass ℝ 𝕜 F₁] →
                                        [inst_12 : NormedSpace ℝ F₃] →
                                          [SMulCommClass ℝ 𝕜 F₃] →
                                            (F₁ →L[𝕜] F₂ →L[𝕜] F₃) →
                                              MeasureTheory.Measure E →
                                                (E → F₂) → ContDiffMapSupportedIn E F₁ n K →ₗ[𝕜] F₃
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.esymm_mul_psum_summand_to_weight : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : Fintype σ] (k : ℕ),
  ∀ a ∈ Finset.HasAntidiagonal.antidiagonal k,
    ∑ A ∈ Finset.powersetCard a.1 Finset.univ, ∑ j, MvPolynomial.NewtonIdentities.weight✝ σ R k (A, j) =
      (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
-- Std.Time.Zoned.RecurringRule
Std.Time.TimeZone.instReprTransitionSpec : Repr Std.Time.TimeZone.TransitionSpec
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.norm_applyOrderedFinpartition_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (c : OrderedFinpartition n) (p : (i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) (v : Fin n → E) (m : Fin c.length),
  ‖c.applyOrderedFinpartition p v m‖ ≤ ‖p m‖ * ∏ i, ‖v (c.emb m i)‖
-- Mathlib.Algebra.TrivSqZeroExt.Basic
/-- In the general non-commutative case, the power operator is

$$\begin{align}
(r + m)^n &= r^n + r^{n-1}m + r^{n-2}mr + \cdots + rmr^{n-2} + mr^{n-1} \\
          & =r^n + \sum_{i = 0}^{n - 1} r^{(n - 1) - i} m r^{i}
\end{align}$$

In the commutative case this becomes the simpler $(r + m)^n = r^n + nr^{n-1}m$.
 -/
TrivSqZeroExt.instPowNatOfDistribMulActionMulOpposite : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] →
      [inst_1 : AddMonoid M] → [DistribMulAction R M] → [DistribMulAction Rᵐᵒᵖ M] → Pow (TrivSqZeroExt R M) ℕ
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
DerivedCategory.triangleOfSES.map_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} (h₁ : S₁.ShortExact)
  (h₂ : S₂.ShortExact) (f : S₁ ⟶ S₂), (DerivedCategory.triangleOfSES.map h₁ h₂ f).hom₃ = DerivedCategory.Q.map f.τ₃
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.stepRet.eq_2 : ∀ (x : List ℕ) (fs : Turing.ToPartrec.Code) (as : List ℕ) (k : Turing.ToPartrec.Cont),
  Turing.ToPartrec.stepRet (Turing.ToPartrec.Cont.cons₁ fs as k) x =
    Turing.ToPartrec.stepNormal fs (Turing.ToPartrec.Cont.cons₂ x k) as
-- Mathlib.Algebra.Ring.Action.Invariant
IsInvariantSubring.coe_subtypeHom' : ∀ (M : Type u_1) [inst : Monoid M] {R' : Type u_2} [inst_1 : Ring R'] [inst_2 : MulSemiringAction M R'] (U : Subring R')
  [inst_3 : IsInvariantSubring M U], ↑(IsInvariantSubring.subtypeHom M U) = U.subtype
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
/-- The image of the good products in the module `LocallyConstant C ℤ`.  -/
Profinite.NobelingProof.GoodProducts.range : {I : Type u} → (C : Set (I → Bool)) → [LinearOrder I] → Set (LocallyConstant ↑C ℤ)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.π_comp_H0IsoOfIsTrivial_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) [inst_2 : A.IsTrivial],
  CategoryTheory.CategoryStruct.comp (groupHomology.π A 0) (groupHomology.H0IsoOfIsTrivial A).hom =
    (groupHomology.cyclesIso₀ A).hom
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closure_openCell_eq_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {n : ℕ}
  {j : Topology.RelCWComplex.cell C n},
  closure (Topology.RelCWComplex.openCell n j) = Topology.RelCWComplex.closedCell n j
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.max : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f g : β → α}
  {b : Filter β} {a₁ a₂ : α},
  Filter.Tendsto f b (nhds a₁) →
    Filter.Tendsto g b (nhds a₂) → Filter.Tendsto (fun b => max (f b) (g b)) b (nhds (max a₁ a₂))
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.instCategoryStruct : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor C C) →
      CategoryTheory.CategoryStruct.{v, max u v} (CategoryTheory.Endofunctor.Coalgebra F)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instBot : {R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Bot (LieSubalgebra R L)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.hasPushouts_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Limits.HasPushouts Cᵒᵖ
-- Mathlib.RingTheory.PowerSeries.Trunc
/-- Split off the first `n` coefficients.  -/
PowerSeries.eq_shift_mul_X_pow_add_trunc : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (f : PowerSeries R),
  f = (PowerSeries.mk fun i => (PowerSeries.coeff (i + n)) f) * PowerSeries.X ^ n + ↑((PowerSeries.trunc n) f)
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.naturality : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (self : CategoryTheory.Lax.StrongTrans F G) →
            {a b : B} →
              (f : a ⟶ b) →
                CategoryTheory.CategoryStruct.comp (self.app a) (G.map f) ≅
                  CategoryTheory.CategoryStruct.comp (F.map f) (self.app b)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorInfo.kind : Lean.Elab.Term.MVarErrorInfo → Lean.Elab.Term.MVarErrorKind
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.exists_genWeightSpace_smul_add_eq_bot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (χ₁ χ₂ : L → R) [IsAddTorsionFree R] [IsDomain R] [Module.IsTorsionFree R M]
  [IsNoetherian R M], χ₁ ≠ 0 → ∃ k > 0, LieModule.genWeightSpace M (k • χ₁ + χ₂) = ⊥
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_mul : ∀ {m n : ℕ},
  m.Coprime n →
    ArithmeticFunction.cardDistinctFactors (m * n) =
      ArithmeticFunction.cardDistinctFactors m + ArithmeticFunction.cardDistinctFactors n
-- Mathlib.Algebra.Torsor.Basic
vadd_eq_vadd_iff_sub_eq_vsub : ∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] {v₁ v₂ : G} {p₁ p₂ : P},
  v₁ +ᵥ p₁ = v₂ +ᵥ p₂ ↔ v₂ - v₁ = p₁ -ᵥ p₂
-- Mathlib.Topology.Algebra.Monoid
/-- The (topological-space) closure of a submonoid of a space `M` with `ContinuousMul` is
itself a submonoid.  -/
Submonoid.topologicalClosure : {M : Type u_3} →
  [inst : TopologicalSpace M] → [inst_1 : Monoid M] → [SeparatelyContinuousMul M] → Submonoid M → Submonoid M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Extract
Std.Tactic.BVDecide.BVExpr.bitblast.instLawfulVecOperatorExtractTargetBlastExtract : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.ExtractTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastExtract
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.Presieve.categoryMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Presieve X) {Y : C}
  (f f_1 : Y ⟶ X) (e_f : f = f_1) (hf : P f), P.categoryMk f hf = P.categoryMk f_1 ⋯
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_smul` with the discrete norm on `α`.  -/
hammingDist_smul : ∀ {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → SMul α (β i)] {k : α} {x y : (i : ι) → β i},
  (∀ (i : ι), IsSMulRegular (β i) k) → hammingDist (k • x) (k • y) = hammingDist x y
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_inv_eq_iff : ∀ {x y : NNReal} {z : ℝ}, z ≠ 0 → (x ^ z⁻¹ = y ↔ x = y ^ z)
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.comp_apply : ∀ {R : Type u} [inst : CommRing R] {A B C : CommBialgCat R} (f : A ⟶ B) (g : B ⟶ C) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) a =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) a)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.isLoop_tfae : ∀ {α : Type u_1} (M : Matroid α) (e : α),
  [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
-- Mathlib.Probability.Kernel.IonescuTulcea.Traj
/-- This theorem shows that `traj κ n` is, up to an equivalence, the product of
a deterministic kernel with another kernel. This is an intermediate result to compute integrals
with respect to this kernel.  -/
ProbabilityTheory.Kernel.traj_eq_prod : ∀ {X : ℕ → Type u_1} [inst : (n : ℕ) → MeasurableSpace (X n)]
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [inst_1 : ∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ),
  ProbabilityTheory.Kernel.traj κ a =
    (ProbabilityTheory.Kernel.id.prod ((ProbabilityTheory.Kernel.traj κ a).map (Set.Ioi a).domRestrict)).map
      ⇑(MeasurableEquiv.IicProdIoi a)
-- Lean.Elab.Quotation
/-- Bind right-hand side to new `let_delayed` decl in order to prevent code duplication  -/
_private.Lean.Elab.Quotation.0.Lean.Elab.Term.Quotation.deduplicate : Array Lean.Syntax →
  Lean.Elab.Term.Quotation.Alt → Lean.Elab.TermElabM (Array Lean.Syntax × Lean.Elab.Term.Quotation.Alt)
-- Mathlib.Algebra.Homology.SpectralSequence.ComplexShape
ComplexShape.spectralSequenceFin_rel_iff : ∀ {l : ℕ} (u : ℤ × ℤ) (a b : ℤ × Fin l),
  (ComplexShape.spectralSequenceFin l u).Rel a b ↔ a.1 + u.1 = b.1 ∧ ↑↑a.2 + u.2 = ↑↑b.2
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instIsSMulApplyReal : ∀ {R : Type u_1} {E : Type u_3} [inst : AddGroup E] [inst_1 : SMul R ℝ] [inst_2 : SMul R NNReal]
  [inst_3 : IsScalarTower R NNReal ℝ], IsSMulApply R (AddGroupSeminorm E) E ℝ
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiringClass.mulMemClass : ∀ (S : Type u_1) (R : Type u) [inst : NonUnitalNonAssocSemiring R] [inst_1 : SetLike S R]
  [h : NonUnitalSubsemiringClass S R], MulMemClass S R
-- Mathlib.Logic.Equiv.Set
/-- `sumDiffSubset s t` is the natural equivalence between
`s ⊕ (t \ s)` and `t`, where `s` and `t` are two sets.  -/
Equiv.Set.sumDiffSubset : {α : Type u_3} → {s t : Set α} → s ⊆ t → [DecidablePred fun x => x ∈ s] → ↑s ⊕ ↑(t \ s) ≃ ↑t
-- Mathlib.Condensed.Discrete.Colimit
LightCondensed.lanPresheafExt_hom : ∀ {F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (S : LightProfiniteᵒᵖ)
  (i : FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G),
  (LightCondensed.lanPresheafExt i).hom.app S =
    CategoryTheory.Limits.colimMap
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op S).whiskerLeft i.hom)
-- Mathlib.Order.Filter.Map
Filter.map_surjOn_Iic_iff_le_map : ∀ {α : Type u_1} {β : Type u_2} {F : Filter α} {G : Filter β} {m : α → β},
  Set.SurjOn (Filter.map m) (Set.Iic F) (Set.Iic G) ↔ G ≤ Filter.map m F
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_zero_right : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [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₃), f.coprod 0 = f ∘ₗ LinearMap.fst R M M₂
-- Mathlib.MeasureTheory.Measure.Tilted
/-- Exponentially tilted measure. When `x ↦ exp (f x)` is integrable, `μ.tilted f` is the
probability measure with density with respect to `μ` proportional to `exp (f x)`. Otherwise it is 0.
 -/
MeasureTheory.Measure.tilted : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure α → (α → ℝ) → MeasureTheory.Measure α
-- Mathlib.Data.ENat.Basic
instLinearOrderedAddCommMonoidWithTopENat : LinearOrderedAddCommMonoidWithTop ℕ∞
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀ArrowIso_hom_right : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  (groupHomology.d₁₀ArrowIso A).hom.right = (groupHomology.chainsIso₀ A).hom
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotEquivQuotMap_apply_mk : ∀ {R : Type u_1} [inst : CommRing R] (f g : Polynomial R) (I : Ideal R),
  (AdjoinRoot.quotEquivQuotMap f I) ((Ideal.Quotient.mk (Ideal.map (AdjoinRoot.of f) I)) ((AdjoinRoot.mk f) g)) =
    (Ideal.Quotient.mk (Ideal.span {Polynomial.map (Ideal.Quotient.mk I) f})) (Polynomial.map (Ideal.Quotient.mk I) g)
-- Mathlib.Order.Cover
/-- **Alias** of the forward direction of `wcovBy_iff_eq_or_covBy`. -/
WCovBy.eq_or_covBy : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a ⩿ b → a = b ∨ a ⋖ b
-- Mathlib.Algebra.Free
FreeAddSemigroup.length_of : ∀ {α : Type u} (x : α), (FreeAddSemigroup.of x).length = 1
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.entails.rfl : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ⊢ₛ P
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.tensorProductTo.eq_1 : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D : Derivation R S M),
  D.tensorProductTo = TensorProduct.AlgebraTensorModule.lift ((LinearMap.lsmul S (S →ₗ[R] M)).flip ↑D)
-- Std.Http.Internal.IndexMultiMap
/-- Like `get?`, but panics if absent.
 -/
Std.Internal.IndexMultiMap.get! : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → [Inhabited β] → Std.Internal.IndexMultiMap α β → α → β
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.monodromy_ext_iff : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x y : X}
  {γ γ' : Path.Homotopic.Quotient x y} (e : ↑(p ⁻¹' {x})),
  ⋯.monodromy γ e = ⋯.monodromy γ' e ↔ ⋯.monodromy γ = ⋯.monodromy γ'
-- Init.Data.Slice.Array.Iterator
SubarrayIterator.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (xs : Subarray α), sizeOf { xs := xs } = 1 + sizeOf xs
-- Mathlib.Data.Finset.NoncommProd
Multiset.noncommFoldr_empty : ∀ {α : Type u_3} {β : Type u_4} (f : α → β → β)
  (h : {x | x ∈ 0}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)) (b : β), Multiset.noncommFoldr f 0 h b = b
-- Mathlib.ModelTheory.Order
FirstOrder.Language.Term.le.eq_1 : ∀ {L : FirstOrder.Language} {α : Type w} {n : ℕ} [inst : L.IsOrdered] (t₁ t₂ : L.Term (α ⊕ Fin n)),
  t₁.le t₂ = FirstOrder.Language.leSymb.boundedFormula₂ t₁ t₂
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_trinomial_subset : ∀ {R : Type u} [inst : Semiring R] (k m n : ℕ) (x y z : R),
  (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m + Polynomial.C z * Polynomial.X ^ n).support ⊆
    {k, m, n}
-- Lean.Meta.Instances
/-- The order in which the instance's arguments are to be synthesized.  -/
Lean.Meta.InstanceEntry.synthOrder : Lean.Meta.InstanceEntry → Array ℕ
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_eq_contract_delete : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → M.contract X = (M.contract I).delete (X \ I)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.instInnerProductSpaceH₀ : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              {K : Matrix X X (V →L[𝕜] V)} → [inst_4 : Fact K.PosSemidef] → InnerProductSpace 𝕜 (RKHS.H₀ K)
-- Mathlib.Data.Int.Cast.Defs
/-- The canonical homomorphism `ℤ → R` for negative values is just the negation of the values
of the canonical homomorphism `ℕ → R`.  -/
AddGroupWithOne.intCast_negSucc : ∀ {R : Type u} [self : AddGroupWithOne R] (n : ℕ), IntCast.intCast (Int.negSucc n) = -↑(n + 1)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sub_le : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R} {g : Γ₀}, v x ≤ g → v y ≤ g → v (x - y) ≤ g
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
_private.Mathlib.MeasureTheory.Constructions.BorelSpace.Real.0.EReal.measurable_const_mul : ∀ (c : EReal), Measurable fun x => c * x
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the complex plane is given by evaluating
its Taylor series at any point `c`.  -/
Complex.taylorSeries_eq_of_entire' : ∀ (c z : ℂ) {f : ℂ → ℂ}, Differentiable ℂ f → ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z