mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
/-- `map_cocone` commutes with `precompose`. In particular, for `F : J ⥤ C`, given a cocone
`c : Cocone F`, a natural transformation `α : F ⟶ G` and a functor `H : C ⥤ D`, we have two obvious
ways of producing a cocone over `G ⋙ H`, and they are both isomorphic.
 -/
CategoryTheory.Functor.mapCoconePrecompose : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            (H : CategoryTheory.Functor C D) →
              {F G : CategoryTheory.Functor J C} →
                {α : G ⟶ F} →
                  {c : CategoryTheory.Limits.Cocone F} →
                    H.mapCocone ((CategoryTheory.Limits.Cocone.precompose α).obj c) ≅
                      (CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Functor.whiskerRight α H)).obj
                        (H.mapCocone c)
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- A separable contraction of a polynomial `f` is a separable polynomial `g` such that
`g(x^(q^m)) = f(x)` for some `m : ℕ`.  -/
Polynomial.IsSeparableContraction : {F : Type u_1} → [inst : CommSemiring F] → ℕ → Polynomial F → Polynomial F → Prop
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.updateCode : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Alt pu → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Alt pu
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_closure_iff_ball : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set α} {x : α},
  x ∈ closure s ↔ ∀ {V : Set (α × α)}, V ∈ uniformity α → (UniformSpace.ball x V ∩ s).Nonempty
-- Init.Data.BitVec.Bitblast
BitVec.getElem_sdiv : ∀ {w i : ℕ} {x y : BitVec w} (h : i < w),
  (x.sdiv y)[i] =
    match x.msb, y.msb with
    | false, false => (x / y)[i]
    | false, true => (-(x / -y))[i]
    | true, false => (-(-x / y))[i]
    | true, true => (-x / -y)[i]
-- Mathlib.Data.Nat.Log
_private.Mathlib.Data.Nat.Log.0.Nat.log.go.match_3.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive x 0) (h_2 : (b fuel : ℕ) → motive b fuel.succ),
  (match x, 0 with
    | x, 0 => h_1 x
    | b, fuel.succ => h_2 b fuel) =
    h_1 x
-- Mathlib.Algebra.Category.Grp.Images
/-- the image of a morphism in `AddCommGrpCat` is just the bundling of `AddMonoidHom.range f`  -/
AddCommGrpCat.image : {G H : AddCommGrpCat} → (G ⟶ H) → AddCommGrpCat
-- Init.Data.String.Lemmas.StringOrder
String.lt_asymm : ∀ {a b : String}, a < b → ¬b < a
-- Mathlib.Analysis.Calculus.BumpFunction.Normed
ContDiffBump.normed.congr_simp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E]
  [inst_3 : MeasurableSpace E] {c : E} (f f_1 : ContDiffBump c),
  f = f_1 → ∀ (μ μ_1 : MeasureTheory.Measure E), μ = μ_1 → ∀ (a a_1 : E), a = a_1 → f.normed μ a = f_1.normed μ_1 a_1
-- Init.Data.Range.Polymorphic.Basic
/-- If the smallest value in the range satisfies the upper bound and has no successor, the size is
  one.
   -/
Std.Rxo.LawfulHasSize.size_eq_one_of_succ?_eq_none : ∀ {α : Type u} {inst : LT α} {inst_1 : Std.PRange.UpwardEnumerable α} {inst_2 : Std.Rxo.HasSize α}
  [self : Std.Rxo.LawfulHasSize α] (lo hi : α), lo < hi → Std.PRange.succ? lo = none → Std.Rxo.HasSize.size lo hi = 1
-- Mathlib.Algebra.Regular.Basic
/-- An element is left-regular if and only if multiplying it on the left by a left-regular element
is left-regular.  -/
mul_isLeftRegular_iff : ∀ {R : Type u_1} [inst : Semigroup R] {a : R} (b : R), IsLeftRegular a → (IsLeftRegular (a * b) ↔ IsLeftRegular b)
-- Mathlib.Data.Part
Part.left_dom_of_div_dom : ∀ {α : Type u_1} [inst : Div α] {a b : Part α}, (a / b).Dom → a.Dom
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.hsymm.eq_1 : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] (n : ℕ),
  MvPolynomial.hsymm σ R n = ∑ s, (Multiset.map MvPolynomial.X ↑s).prod
-- Mathlib.CategoryTheory.Center.Linear
/-- `a • f = f ≫ (φ a).app Y`.  -/
CategoryTheory.Linear.smulOfRingMorphism_smul_eq' : ∀ {R : Type w} [inst : Ring R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Preadditive C] (φ : R →+* CategoryTheory.CatCenter C) {X Y : C} (a : R) (f : X ⟶ Y),
  a • f = CategoryTheory.CategoryStruct.comp f ((φ a).app Y)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Given a left extension `E` of `F : C ⥤ H` along `L : C ⥤ D` and a functor `G : H ⥤ D'`,
`E.postcompose₂ G` is the extension of `F ⋙ G` along `L` obtained by whiskering by `G`
on the right.  -/
CategoryTheory.Functor.LeftExtension.postcompose₂ : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      {D' : Type u_5} →
        [inst : CategoryTheory.Category.{v_1, u_1} C] →
          [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
            [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
              [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] →
                (L : CategoryTheory.Functor C D) →
                  (F : CategoryTheory.Functor C H) →
                    (G : CategoryTheory.Functor H D') →
                      CategoryTheory.Functor (L.LeftExtension F) (L.LeftExtension (F.comp G))
-- Mathlib.Algebra.Category.Grp.Zero
AddGrpCat.subsingleton_of_isZero : ∀ {G : AddGrpCat}, CategoryTheory.Limits.IsZero G → Subsingleton ↑G
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.NormNoninc.comp : ∀ {V₁ : Type u_3} {V₂ : Type u_4} {V₃ : Type u_5} [inst : SeminormedAddCommGroup V₁]
  [inst_1 : SeminormedAddCommGroup V₂] [inst_2 : SeminormedAddCommGroup V₃] {g : NormedAddGroupHom V₂ V₃}
  {f : NormedAddGroupHom V₁ V₂}, g.NormNoninc → f.NormNoninc → (g.comp f).NormNoninc
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.addLECancellable_sum : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LE α] [AddLeftMono α] {s : Finset ι} {f : ι → α},
  AddLECancellable (∑ i ∈ s, f i) ↔ ∀ ⦃i : ι⦄, i ∈ s → AddLECancellable (f i)
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.restrictScalars.congr_simp : ∀ (K : Type u_1) {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] [inst_5 : Algebra L' L] [inst_6 : IsScalarTower K L' L]
  (E E_1 : IntermediateField L' L),
  E = E_1 → IntermediateField.restrictScalars K E = IntermediateField.restrictScalars K E_1
-- Std.Do.WP.SimpLemmas
Std.Do.WP.monadLift_trans : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {o : Type u → Type u_1} {n : Type u → Type u_2} {α : Type u} {x : m α}
  {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP o ps] [inst_1 : MonadLift n o] [inst_2 : MonadLiftT m n],
  (Std.Do.wp (monadLift x)).apply Q = (Std.Do.wp (MonadLift.monadLift (monadLift x))).apply Q
-- Mathlib.RingTheory.PowerSeries.Order
/-- The `n`th coefficient of a formal power series is `0` if `n` is strictly
smaller than the order of the power series.  -/
PowerSeries.coeff_of_lt_order : ∀ {R : Type u_1} [inst : Semiring R] {φ : PowerSeries R} (n : ℕ), ↑n < φ.order → (PowerSeries.coeff n) φ = 0
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sshiftRight_of_msb_false : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, x.msb = false → (x.sshiftRight n).toNat = x.toNat >>> n
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices.eq_1 : ∀ (n : ℕ),
  n.bitIndices =
    Nat.binaryRec [] (fun b x s => Bool.casesOn b (List.map (fun x => x + 1) s) (0 :: List.map (fun x => x + 1) s)) n
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic
SSet.strongAnodyneExtensions.mono : ∀ {X Y : SSet} {f : X ⟶ Y}, SSet.strongAnodyneExtensions f → CategoryTheory.Mono f
-- Mathlib.AlgebraicGeometry.Sites.Etale
/-- A separably closed field `Ω` defines a point on the étale topology by the fiber
functor `X ↦ Hom(Spec Ω, X)`.  -/
AlgebraicGeometry.Scheme.geometricFiber : (Ω : Type u) → [inst : Field Ω] → [IsSepClosed Ω] → AlgebraicGeometry.Scheme.etaleTopology.Point
-- Mathlib.Order.Minimal
maximalFor_id : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α], MaximalFor P id x ↔ Maximal P x
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.lt_exp_of_log_lt : ∀ {G : Type u_3} [inst : Preorder G] {a : G} [inst_1 : AddGroup G] {x : WithZero (Multiplicative G)},
  x.log < a → x < WithZero.exp a
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.whisker_right_comp : ∀ {B : Type u} [inst : Quiver B] {a b c d : B} {f f' : CategoryTheory.FreeBicategory.Hom a b}
  (g : CategoryTheory.FreeBicategory.Hom b c) (h : CategoryTheory.FreeBicategory.Hom c d)
  (η : CategoryTheory.FreeBicategory.Hom₂ f f'),
  CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_right (g.comp h) η)
    ((CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h).vcomp
      ((CategoryTheory.FreeBicategory.Hom₂.whisker_right h (CategoryTheory.FreeBicategory.Hom₂.whisker_right g η)).vcomp
        (CategoryTheory.FreeBicategory.Hom₂.associator f' g h)))
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.comp_tendsto : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F}
  {l : Filter α}, f =O[l] g → ∀ {k : β → α} {l' : Filter β}, Filter.Tendsto k l' l → (f ∘ k) =O[l'] (g ∘ k)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.primesOverFinset.congr_simp : ∀ {A : Type u_4} [inst : CommRing A] (p p_1 : Ideal A),
  p = p_1 →
    ∀ (B : Type u_5) [inst_1 : CommRing B] [inst_2 : IsDedekindDomain B] [inst_3 : Algebra A B],
      IsDedekindDomain.primesOverFinset p B = IsDedekindDomain.primesOverFinset p_1 B
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_left_monoOn₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] [MulPosMono G₀] {n : ℤ},
  0 ≤ n → MonotoneOn (fun a => a ^ n) {a | 0 ≤ a}
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.mono_enorm : ∀ {α : Type u_1} {ε : Type u_4} {ε' : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  MeasureTheory.HasFiniteIntegral g μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ ‖g a‖ₑ) → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.mem_support_left : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → u ∈ G.support
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.Subcomplex.eq_top_iff_of_hasDimensionLT : ∀ {X : SSet} (A : X.Subcomplex) (d : ℕ) [X.HasDimensionLT d],
  A = ⊤ ↔ ∀ i < d, X.nonDegenerate i ⊆ A.obj (Opposite.op { len := i })
-- Mathlib.LinearAlgebra.Projectivization.PSL.Stabilizer
/-- The candidate family of subgroups for the Iwasawa structure on
`PSL ι F` acting on the projective space `ℙ F (ι → F)`: the unipotent radical
attached to the line through `p`.  -/
PSL.iwasawaT : {F : Type u_1} →
  [inst : Field F] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] →
        [inst_2 : Fintype ι] → Projectivization F (ι → F) → Subgroup (Matrix.ProjectiveSpecialLinearGroup ι F)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Riesz's theorem applied to manifolds: a locally compact manifold must be modelled on a
finite-dimensional space. This is the converse to `Manifold.locallyCompact_of_finiteDimensional`.  -/
FiniteDimensional.of_locallyCompact_manifold : ∀ {E : Type u_8} {𝕜 : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_10} [inst_3 : TopologicalSpace H] (M : Type u_11) [inst_4 : TopologicalSpace M]
  [ChartedSpace H M] [CompleteSpace 𝕜] (I : ModelWithCorners 𝕜 E H) [Nonempty M] [LocallyCompactSpace M],
  FiniteDimensional 𝕜 E
-- Mathlib.MeasureTheory.Covering.Differentiation
/-- For every point `x`, sufficiently small sets in a Vitali family around `x` have finite measure.
(This is a trivial result, following from the fact that the measure is locally finite).  -/
VitaliFamily.eventually_measure_lt_top : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [MeasureTheory.IsLocallyFiniteMeasure μ] (x : α), ∀ᶠ (a : Set α) in v.filterAt x, μ a < ⊤
-- Mathlib.Order.IsNormal
/-- If `f : α → α` in a well-order, we can infer one of the hypotheses in
`Order.IsNormal.le_iff_le_sSup`.  -/
Order.IsNormal.le_iff_le_sSup' : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] [WellFoundedLT α] {f : α → α},
  Order.IsNormal f → ∀ {x y : α}, (f ⁻¹' Set.Iic y).Nonempty → (f x ≤ y ↔ x ≤ sSup (f ⁻¹' Set.Iic y))
-- Mathlib.Analysis.BoxIntegral.UnitPartition
BoxIntegral.unitPartition.prepartition.congr_simp : ∀ {ι : Type u_1} (n n_1 : ℕ) (e_n : n = n_1) [inst : NeZero n] [inst_1 : Fintype ι] (B : BoxIntegral.Box ι),
  BoxIntegral.unitPartition.prepartition n B = BoxIntegral.unitPartition.prepartition n_1 B
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Add G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G]
  {a b : G}, ContMDiffAt I I n (fun x => x + a) b
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
BoundedContinuousFunction.toLp_denseRange : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [inst_3 : BorelSpace α]
  (E : Type u_2) [inst_4 : NormedAddCommGroup E] (μ : MeasureTheory.Measure α) {p : ENNReal}
  [inst_5 : SecondCountableTopologyEither α E] [_i : Fact (1 ≤ p)] (𝕜 : Type u_3) [inst_6 : NormedRing 𝕜]
  [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E] [NormedSpace ℝ E] [μ.WeaklyRegular]
  [inst_11 : MeasureTheory.IsFiniteMeasure μ], p ≠ ⊤ → DenseRange ⇑(BoundedContinuousFunction.toLp p μ 𝕜)
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.map_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {f : β → γ} (κ : ProbabilityTheory.Kernel α β),
  Measurable f → ∀ (a : α) {s : Set γ}, MeasurableSet s → ((κ.map f) a) s = (κ a) (f ⁻¹' s)
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder γ] [inst_3 : Preorder δ] [inst_4 : BoundedOrder α] [inst_5 : BoundedOrder β]
  [inst_6 : BoundedOrder γ] [inst_7 : BoundedOrder δ] (f : BoundedOrderHom γ δ) (g : BoundedOrderHom β γ)
  (h : BoundedOrderHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.symm_trans_apply : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Mul A] [inst_1 : Mul B] [inst_2 : Mul C] [inst_3 : Star A]
  [inst_4 : Star B] [inst_5 : Star C] (e₁ : A ≃⋆* B) (e₂ : B ≃⋆* C) (x : C), (e₁.trans e₂).symm x = e₁.symm (e₂.symm x)
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.nullSingletonClass_gaussianReal : ∀ {μ : ℝ} {v : NNReal}, v ≠ 0 → MeasureTheory.NullSingletonClass (ProbabilityTheory.gaussianReal μ v)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.smul_apply : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : SMul R M] [inst_3 : ContinuousConstSMul R M] (c : R) (f : C(α, M)) (a : α), (c • f) a = c • f a
-- Mathlib.Probability.Distributions.Gaussian.Basic
/-- Mapping a Gaussian measure by a measurable and continuous linear map yields a Gaussian
measure. See also `isGaussian_map`, which does not assume measurability but has stronger hypotheses
on `E`. In particular, it requires `E` to be a Borel space, which requires some second countability
hypotheses if `E` is a product space. This version does not, which can be useful for instance
if `L := Prod.fst`, which is always measurable.  -/
ProbabilityTheory.isGaussian_map_of_measurable : ∀ {E : Type u_1} {F : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E]
  {mE : MeasurableSpace E} [inst_3 : TopologicalSpace F] [inst_4 : AddCommMonoid F] [inst_5 : Module ℝ F]
  {mF : MeasurableSpace F} [OpensMeasurableSpace F] {μ : MeasureTheory.Measure E} {L : E →L[ℝ] F}
  [ProbabilityTheory.IsGaussian μ], Measurable ⇑L → ProbabilityTheory.IsGaussian (MeasureTheory.Measure.map (⇑L) μ)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toAddSubgroup_injective : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G], Function.Injective OpenAddSubgroup.toAddSubgroup
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
IsCompact.nullMeasurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  [T2Space α] {μ : MeasureTheory.Measure α}, IsCompact s → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Topology.MetricSpace.Bounded
/-- Open balls are bounded  -/
Metric.isBounded_ball : ∀ {α : Type u} {x : α} {r : ℝ} [inst : PseudoMetricSpace α], Bornology.IsBounded (Metric.ball x r)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_apply_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {κ : ProbabilityTheory.Kernel α β} {η : ProbabilityTheory.Kernel (α × β) γ}
  [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] {a : α} {s : Set β} {t : Set γ},
  MeasurableSet s → MeasurableSet t → ((κ.compProd η) a) (s ×ˢ t) = ∫⁻ (b : β) in s, (η (a, b)) t ∂κ a
-- Mathlib.GroupTheory.Congruence.Defs
Con.instDecidableEqQuotientOfDecidableCoeForallProp.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (c : Con M) [inst_1 : (a b : M) → Decidable (c a b)],
  c.instDecidableEqQuotientOfDecidableCoeForallProp = Con.instDecidableEqQuotientOfDecidableCoeForallProp._aux_1 c
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeBallStruct.mk : {T : Type u_2} → Finset T → T → ℕ → PairReduction.logSizeBallStruct T
-- Mathlib.Order.Sublocale
nucleusIsoSublocale.eq_toSublocale : ∀ {X : Type u_1} [inst : Order.Frame X], Nucleus.toSublocale = ⇑nucleusIsoSublocale
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
NumberField.absNorm_differentIdeal : ∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsFractionRing 𝒪 K] [inst_5 : IsDedekindDomain 𝒪] [inst_6 : CharZero 𝒪] [inst_7 : Module.Finite ℤ 𝒪],
  Ideal.absNorm (differentIdeal ℤ 𝒪) = (NumberField.discr K).natAbs
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
contMDiffOn_inv₀ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Inv G] [inst_7 : Zero G] [ContMDiffInv₀ I n G],
  ContMDiffOn I I n Inv.inv {0}ᶜ
-- Lean.Meta.Match.Match
/-- Auxiliary method used at `mkMatcher`. It executes `k` in a local context that contains only
the local declarations `m` depends on. This is important because otherwise dependent elimination
may "refine" the types of unnecessary declarations and accidentally introduce unnecessary dependencies
in the auto-generated auxiliary declaration. Note that this is not just an optimization because the
unnecessary dependencies may prevent the termination checker from succeeding. For an example,
see issue #1237.
 -/
Lean.Meta.Match.withCleanLCtxFor : {α : Type} → Lean.Meta.Match.MkMatcherInput → Lean.MetaM α → Lean.MetaM α
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get!_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {k : α} [inst_1 : Inhabited (β k)], k ∈ m₂ → (m₁ \ m₂).get! k = default
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C) (x : ℕ),
  (CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.const X).s x =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.SimplicialObject.Augmented.const.obj X).left.obj (Opposite.op { len := x }))
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.SubmersivePresentation.toPreSubmersivePresentation : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              [inst_3 : Finite σ] → Algebra.SubmersivePresentation R S ι σ → Algebra.PreSubmersivePresentation R S ι σ
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.subtypeMop_injective : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R), Function.Injective ⇑I.subtypeMop
-- Batteries.Control.Nondet.Basic
/-- Filter and map a nondeterministic value.  -/
Nondet.filterMap : {σ : Type} →
  {m : Type → Type} →
    [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α β : Type} → (α → Option β) → Nondet m α → Nondet m β
-- Mathlib.GroupTheory.Complement
AddSubgroup.exists_isComplement_left : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) (g : G), ∃ S, AddSubgroup.IsComplement S ↑H ∧ g ∈ S
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.le_maxKey!_of_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → ∀ {k : α}, t.contains k = true → (cmp k t.maxKey!).isLE = true
-- Mathlib.Topology.Homotopy.Lifting
/-- A continuous map `f` from a path connected, locally path-connected space `A` to another
space `X` lifts uniquely through a covering map `p : E → X` (such that `f a₀` is lifted to `e₀`)
if `f⁎ π₁(A, a₀) ⊆ p⁎ π₁(E, e₀)`. Proposition 1.33 of [hatcher02], known as
the lifting criterion.  -/
IsCoveringMap.existsUnique_continuousMap_lifts_of_range_le : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) [PathConnectedSpace A] [LocallyPathConnectedSpace A]
  {f : C(A, X)} {a₀ : A} {e₀ : E} (he : p e₀ = f a₀),
  (FundamentalGroup.map f a₀).range ≤ (FundamentalGroup.mapOfEq { toFun := p, continuous_toFun := ⋯ } he).range →
    ∃! F, F a₀ = e₀ ∧ p ∘ ⇑F = ⇑f
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMon.go.induct_unfolding : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k : ℤ), (k == 0) = true → motive (Lean.Grind.CommRing.Poly.num k) (Lean.Grind.CommRing.Poly.num 0)) →
    (∀ (k_1 : ℤ),
        (k_1 == 0) = false →
          motive (Lean.Grind.CommRing.Poly.num k_1)
            (Lean.Grind.CommRing.Poly.add (k * k_1) m (Lean.Grind.CommRing.Poly.num 0))) →
      (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
          motive p (Lean.Grind.CommRing.Poly.mulMon.go k m p) →
            motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p)
              (Lean.Grind.CommRing.Poly.add (k * k_1) (m.mul m_1) (Lean.Grind.CommRing.Poly.mulMon.go k m p))) →
        ∀ (a : Lean.Grind.CommRing.Poly), motive a (Lean.Grind.CommRing.Poly.mulMon.go k m a)
-- Mathlib.Data.Fintype.BigOperators
/-- The product over a product type equals the product of the fiberwise products. For rewriting
in the reverse direction, use `Fintype.prod_prod_type`.  -/
Fintype.prod_prod_type' : ∀ {γ : Type u_3} {α₁ : Type u_4} {α₂ : Type u_5} [inst : Fintype α₁] [inst_1 : Fintype α₂] [inst_2 : CommMonoid γ]
  (f : α₁ → α₂ → γ), ∏ x, f x.1 x.2 = ∏ x, ∏ y, f x y