mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_union!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₂ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true}, (m₁.union! m₂).getKey k h' = m₁.getKey k ⋯
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_zero : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k], SkewMonoidAlgebra.coeff 0 = 0
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.adjoinNegOne_eq_self_iff : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R] {𝒢 : Subgroup (GL n R)},
  𝒢.adjoinNegOne = 𝒢 ↔ -1 ∈ 𝒢
-- Mathlib.Data.Prod.Basic
Prod.swap_surjective : ∀ {α : Type u_1} {β : Type u_2}, Function.Surjective Prod.swap
-- Lean.MetavarContext
Lean.assignLevelMVarExp : Lean.MetavarContext → Lean.LMVarId → Lean.Level → Lean.MetavarContext
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.FunctorPushforwardStructure.mk : {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} →
            {S : CategoryTheory.Presieve X} →
              {Y : D} →
                {f : Y ⟶ F.obj X} →
                  (preobj : C) →
                    (premap : preobj ⟶ X) →
                      (lift : Y ⟶ F.obj preobj) →
                        S premap →
                          f = CategoryTheory.CategoryStruct.comp lift (F.map premap) →
                            CategoryTheory.Presieve.FunctorPushforwardStructure F S f
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_one_nat_atTop_iff : ∀ {E'' : Type u_9} [inst : NormedAddCommGroup E''] {f : ℕ → E''},
  (f =O[Filter.atTop] fun _n => 1) ↔ ∃ C, ∀ (n : ℕ), ‖f n‖ ≤ C
-- Lean.Meta.Tactic.Grind.Main
Lean.Meta.Grind.Result : Type
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.prev_nat_zero : (ComplexShape.up ℕ).prev 0 = 0
-- Mathlib.CategoryTheory.FintypeCat
FintypeCat.Skeleton.instFaithfulIncl : FintypeCat.Skeleton.incl.Faithful
-- Lean.Meta.BinderNameHint
_private.Lean.Meta.BinderNameHint.0.Lean.exitScope : Array Lean.Name → Lean.Name × Array Lean.Name
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.coe_comp : ∀ {X Y Z : GrpCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Order.Preorder.Chain
IsMaxChain.not_superChain : ∀ {α : Type u_1} {r : α → α → Prop} {s t : Set α}, IsMaxChain r s → ¬SuperChain r s t
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.instHasProductsOfShapeOfHasCountableProductsOfCountable : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableProducts C]
  (J : Type u_3) [Countable J], CategoryTheory.Limits.HasProductsOfShape J C
-- Init.Omega.LinearCombo
/-- Implementation of negation on `LinearCombo`.  -/
Lean.Omega.LinearCombo.neg : Lean.Omega.LinearCombo → Lean.Omega.LinearCombo
-- Init.Data.Rat.Lemmas
Rat.natCast_eq_zero_iff : ∀ {a : ℕ}, ↑a = 0 ↔ a = 0
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The map is always nonempty. This lemma is needed to apply `SubMulAction.zero_mem`.  -/
MultilinearMap.map_nonempty : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Ring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : Nonempty ι] (f : MultilinearMap R M₁ M₂) (p : (i : ι) → Submodule R (M₁ i)),
  (↑(f.map p)).Nonempty
-- Mathlib.Topology.Order.Monotone
/-- In a second countable space, the set of points where a monotone function is not left-continuous
within a set is at most countable. Superseded by `MonotoneOn.countable_not_continuousWithinAt`
which gives the two-sided version.  -/
MonotoneOn.countable_not_continuousWithinAt_Iio : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {s : Set α} {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β]
  [SecondCountableTopology β], MonotoneOn f s → {x | x ∈ s ∧ ¬ContinuousWithinAt f (s ∩ Set.Iio x) x}.Countable
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred.pp : Lean.Meta.Grind.Arith.Cutsat.CooperSplitPred → Lean.Meta.Grind.GoalM Lean.MessageData
-- Mathlib.Algebra.BigOperators.WithTop
WithTop.prod_eq_top_ne_zero : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
  [inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} {i : ι}, i ∈ s → ∏ j ∈ s, f j = ⊤ → f i ≠ 0
-- Init.WFComputable
/-- A computable version of `Acc.rec`.  -/
Acc.recC : {α : Sort u_1} →
  {r : α → α → Prop} →
    {motive : (a : α) → Acc r a → Sort v} →
      ((x : α) → (h : ∀ (y : α), r y x → Acc r y) → ((y : α) → (hr : r y x) → motive y ⋯) → motive x ⋯) →
        {a : α} → (t : Acc r a) → motive a t
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_sub : ∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E],
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ∀ (m : MeasurableSpace α), μ[f - g | m] =ᵐ[μ] μ[f | m] - μ[g | m]
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.divLeft.congr_simp : ∀ {G : Type w} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] (x x_1 : G),
  x = x_1 → Homeomorph.divLeft x = Homeomorph.divLeft x_1
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Ioc_mul_Ico_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftStrictMono α] [MulRightStrictMono α] (a b c d : α),
  Set.Ioc a b * Set.Ico c d ⊆ Set.Ioo (a * c) (b * d)
-- Mathlib.Algebra.Group.Basic
eq_of_div_eq_one : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, a / b = 1 → a = b
-- Mathlib.Tactic.Order.CollectFacts
/-- Extracts facts and atoms from the expression.  -/
_private.Mathlib.Tactic.Order.CollectFacts.0.Mathlib.Tactic.Order.collectFactsImp.processExpr : Lean.Expr → Mathlib.Tactic.Order.CollectFactsM Unit
-- Mathlib.Probability.BrownianMotion.Basic
/-- If `B` is a Brownian motion and `c > 0`, then `t ↦ (√c)⁻¹ B (c t)` is a Brownian motion.  -/
ProbabilityTheory.IsBrownianReal.smul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {B : NNReal → Ω → ℝ},
  ProbabilityTheory.IsBrownianReal B P →
    ∀ {c : NNReal}, c ≠ 0 → ProbabilityTheory.IsBrownianReal (fun t ω => (√↑c)⁻¹ * B (c * t) ω) P
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Binary products are symmetric.  -/
CategoryTheory.Limits.BinaryFan.isLimitFlip : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {c : CategoryTheory.Limits.BinaryFan X Y} →
        CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk c.snd c.fst)
-- Init.Data.Fin.Lemmas
Fin.mk_le_mk : ∀ {n x y : ℕ} {hx : x < n} {hy : y < n}, ⟨x, hx⟩ ≤ ⟨y, hy⟩ ↔ x ≤ y
-- Mathlib.Topology.Constructions.SumProd
Homeomorph.sumCongr_trans : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {X' : Type u_5} {Y' : Type u_6}
  [inst_2 : TopologicalSpace X'] [inst_3 : TopologicalSpace Y'] {X'' : Type u_7} {Y'' : Type u_8}
  [inst_4 : TopologicalSpace X''] [inst_5 : TopologicalSpace Y''] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y') (h₃ : X' ≃ₜ X'')
  (h₄ : Y' ≃ₜ Y''), (h₁.sumCongr h₂).trans (h₃.sumCongr h₄) = (h₁.trans h₃).sumCongr (h₂.trans h₄)
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
/-- If the target is reduced and the map is quasi-compact, then scheme-theoretically dominant
is equivalent to dominant.  -/
AlgebraicGeometry.isSchemeTheoreticallyDominant_iff_isDominant : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] [AlgebraicGeometry.IsReduced Y],
  AlgebraicGeometry.IsSchemeTheoreticallyDominant f ↔ AlgebraicGeometry.IsDominant f
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.mk₀_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (f g : X ⟶ Y),
  CategoryTheory.Abelian.Ext.mk₀ (f + g) = CategoryTheory.Abelian.Ext.mk₀ f + CategoryTheory.Abelian.Ext.mk₀ g
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivRangeS_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (c : RingCon M) (f : N →+* M)
  {d : RingCon N} (hcd : d = c.comap f) (x : N), (c.comapQuotientEquivRangeS f hcd) ↑x = ⟨↑(f x), ⋯⟩
-- Mathlib.Algebra.CharP.Defs
CharP.nontrivial_of_char_ne_one : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {v : ℕ}, v ≠ 1 → ∀ [hr : CharP R v], Nontrivial R
-- Mathlib.Analysis.Convex.Join
convexJoin_right_comm : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (s t u : Set E),
  convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 (convexJoin 𝕜 s u) t
-- Mathlib.Algebra.Homology.Homotopy
HomotopyEquiv.mk.inj : ∀ {ι : Type u_1} {V : Type u} {inst : CategoryTheory.Category.{v, u} V} {inst_1 : CategoryTheory.Preadditive V}
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {hom : C ⟶ D} {inv : D ⟶ C}
  {homotopyHomInvId : Homotopy (CategoryTheory.CategoryStruct.comp hom inv) (CategoryTheory.CategoryStruct.id C)}
  {homotopyInvHomId : Homotopy (CategoryTheory.CategoryStruct.comp inv hom) (CategoryTheory.CategoryStruct.id D)}
  {hom_1 : C ⟶ D} {inv_1 : D ⟶ C}
  {homotopyHomInvId_1 : Homotopy (CategoryTheory.CategoryStruct.comp hom_1 inv_1) (CategoryTheory.CategoryStruct.id C)}
  {homotopyInvHomId_1 : Homotopy (CategoryTheory.CategoryStruct.comp inv_1 hom_1) (CategoryTheory.CategoryStruct.id D)},
  { hom := hom, inv := inv, homotopyHomInvId := homotopyHomInvId, homotopyInvHomId := homotopyInvHomId } =
      { hom := hom_1, inv := inv_1, homotopyHomInvId := homotopyHomInvId_1, homotopyInvHomId := homotopyInvHomId_1 } →
    hom = hom_1 ∧ inv = inv_1 ∧ homotopyHomInvId ≍ homotopyHomInvId_1 ∧ homotopyInvHomId ≍ homotopyInvHomId_1
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shift_iSup : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] {ι : Sort u_4} (P : ι → CategoryTheory.ObjectProperty C) (a : A),
  (⨆ i, P i).shift a = ⨆ i, (P i).shift a
-- Mathlib.Algebra.Homology.ImageToKernel
/-- `imageToKernel` for `A --0--> B --g--> C`, where `g` is a mono is itself an epi
(i.e. the sequence is exact at `B`).
 -/
imageToKernel_epi_of_zero_of_mono : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V}
  (g : B ⟶ C) [inst_2 : CategoryTheory.Limits.HasKernels V] [inst_3 : CategoryTheory.Limits.HasZeroObject V]
  [CategoryTheory.Mono g], CategoryTheory.Epi (imageToKernel 0 g ⋯)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.spineToSimplex_arrow : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ} (i : Fin n) (f : X.Path n),
  (CategoryTheory.ConcreteCategory.hom (X.map (SimplexCategory.mkOfSucc i).op)) (sx.spineToSimplex f) = f.arrow i
-- Mathlib.Algebra.Group.Commute.Basic
Commute.zpow_left : ∀ {G : Type u_1} [inst : Group G] {a b : G}, Commute a b → ∀ (m : ℤ), Commute (a ^ m) b
-- Lean.Data.Lsp.Extra
/-- `$/lean/fileProgress` client<-server notification.

Contains the ranges of the document that are currently being processed by the server.  -/
Lean.Lsp.LeanFileProgressParams : Type
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α Unit cmp} [inst : Std.TransCmp cmp] [inst_1 : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k fallback : α},
  k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKeyD k fallback = fallback
-- Mathlib.Data.Matrix.Reflection
Matrix.Forall.eq_def : ∀ {α : Type u_1} (x x_1 : ℕ) (x_2 : Matrix (Fin x) (Fin x_1) α → Prop),
  Matrix.Forall x_2 =
    match x, x_1, x_2 with
    | 0, x, P => P (Matrix.of ![])
    | n.succ, x, P => FinVec.Forall fun r => Matrix.Forall fun A => P (Matrix.of (Matrix.vecCons r A))
-- Mathlib.CategoryTheory.FiberedCategory.Fibered
/-- Alternate constructor for `IsFibered`, a functor `p : 𝒳 ⥤ 𝒴` is fibered if any diagram of the
form
```
          a
          -
          |
          v
R --f--> p(a)
```
admits a strongly Cartesian lift `b ⟶ a` of `f`.  -/
CategoryTheory.Functor.IsFibered.of_exists_isStronglyCartesian : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮},
  (∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ) → p.IsFibered
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- To show `P` is a sheaf for the binding of `U` with `B`, it suffices to show that `P` is a sheaf for
`U`, that `P` is a sheaf for each sieve in `B`, and that it is separated for any pullback of any
sieve in `B`.

This is mostly an auxiliary lemma to show `Presieve.isSheafFor_trans`.
Adapted from [Elephant], Lemma C2.1.7(i) with suggestions as mentioned in
https://math.stackexchange.com/a/358709/
 -/
CategoryTheory.Presieve.isSheafFor_bind : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (P : CategoryTheory.Functor Cᵒᵖ (Type u_1))
  (U : CategoryTheory.Sieve X) (B : ⦃Y : C⦄ → ⦃f : Y ⟶ X⦄ → U.arrows f → CategoryTheory.Sieve Y),
  CategoryTheory.Presieve.IsSheafFor P U.arrows →
    (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (hf : U.arrows f), CategoryTheory.Presieve.IsSheafFor P (B hf).arrows) →
      (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄ (h : U.arrows f) ⦃Z : C⦄ (g : Z ⟶ Y),
          CategoryTheory.Presieve.IsSeparatedFor P (CategoryTheory.Sieve.pullback g (B h)).arrows) →
        CategoryTheory.Presieve.IsSheafFor P (CategoryTheory.Sieve.bind U.arrows B).arrows
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_comp_mul_add : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
  c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (c * x + d) = c⁻¹ • ∫ (x : ℝ) in c * a + d..c * b + d, f x
-- Mathlib.Data.Finset.Image
Finset.empty_eq_image : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] {f : α → β} {s : Finset α}, ∅ = Finset.image f s ↔ s = ∅
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.break.inj : ∀ {ref ref_1 : Lean.Syntax}, Lean.Elab.Term.Do.Code.break ref = Lean.Elab.Term.Do.Code.break ref_1 → ref = ref_1
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The multiplicative equivalence between the value group of the completion's valuation, pulled
back along `equiv`, and that of the completion.  -/
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      (K : Type u_2) →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] →
            [inst_4 : IsFractionRing R K] →
              (v : IsDedekindDomain.HeightOneSpectrum R) →
                ↥(MonoidWithZeroHom.ofClass
                        (IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation K v)).valueGroup ≃*
                  ↥(MonoidWithZeroHom.ofClass Valued.v).valueGroup
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.instSliceableImplUnitRiiSlice : {α : Type u} → Std.Rii.Sliceable (Std.DTreeMap.Internal.Impl α fun x => Unit) α (Std.DTreeMap.Internal.Unit.RiiSlice α)
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
_private.Mathlib.Data.Fin.Tuple.NatAntidiagonal.0.List.Nat.antidiagonalTuple.match_1.eq_2 : ∀ (motive : ℕ → ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (k n : ℕ) → motive k.succ n),
  (match 0, n.succ with
    | 0, 0 => h_1 ()
    | 0, n.succ => h_2 n
    | k.succ, n => h_3 k n) =
    h_2 n
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
MeasureTheory.Integrable.integral_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  [inst_3 : NormedSpace ℝ E] ⦃f : β × γ → E⦄,
  MeasureTheory.Integrable f ((κ.compProd η) a) →
    MeasureTheory.Integrable (fun x => ∫ (y : γ), f (x, y) ∂η (a, x)) (κ a)
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instName : Lean.Elab.ConfigEval.EvalTerm Lean.Name
-- Init.Data.List.Nat.Modify
List.modify_zero_cons : ∀ {α : Type u_1} (f : α → α) (a : α) (l : List α), (a :: l).modify 0 f = f a :: l
-- Mathlib.Logic.Equiv.Defs
/-- equivalence of propositions is the same as iff  -/
Equiv.ofIff : {P Q : Prop} → (P ↔ Q) → P ≃ Q
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_eq_some_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a fallback : α},
  a ∈ m → m.get? a = some (m.getD a fallback)
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.one.eq_1 : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.one = H.one
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.coe_symm_toEquiv : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b),
  ⇑e.symm = ⇑e.symm
-- Mathlib.Data.ENat.Basic
ENat.top_ne_ofNat : ∀ (a : ℕ) [inst : a.AtLeastTwo], ⊤ ≠ OfNat.ofNat a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomologyMapData.add_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ φ' : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (γ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂) (γ' : CategoryTheory.ShortComplex.HomologyMapData φ' h₁ h₂),
  (γ.add γ').left = γ.left.add γ'.left
-- Mathlib.Topology.Algebra.Module.IsWeak
/-- The coercion `(B · ·) : E → (F → 𝕜)` is continuous.  -/
LinearMap.IsWeak.coeFn_continuous : ∀ {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommMonoid F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) [hB : B.IsWeak], Continuous fun x1 x2 => (B x1) x2
-- Mathlib.Topology.Algebra.Group.Basic
AddGroup.continuousSMul_int : ∀ {A : Type u_1} [inst : AddGroup A] [inst_1 : TopologicalSpace A] [IsTopologicalAddGroup A], ContinuousSMul ℤ A
-- Mathlib.LinearAlgebra.Ray
SameRay.of_subsingleton' : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Subsingleton R] (x y : M), SameRay R x y
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapAlgHom.eq_1 : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B),
  MonoidAlgebra.mapAlgHom M f = { toRingHom := MonoidAlgebra.mapRingHom M ↑f, commutes' := ⋯ }
-- Init.Data.List.MapIdx
List.mapIdx_eq_cons_iff' : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {l₂ : List β} {l : List α} {b : β},
  List.mapIdx f l = b :: l₂ ↔
    Option.map (f 0) l.head? = some b ∧ Option.map (List.mapIdx fun i => f (i + 1)) l.tail? = some l₂
-- Lean.SubExpr
Lean.SubExpr.Pos.instFromJson : Lean.FromJson Lean.SubExpr.Pos
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
/-- A presheaf is a sheaf after composing with a universe lift if and only if it is a sheaf.  -/
CategoryTheory.Presieve.isSheafFor_comp_uliftFunctor_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X},
  CategoryTheory.Presieve.IsSheafFor (P.comp CategoryTheory.uliftFunctor.{w', w}) R ↔
    CategoryTheory.Presieve.IsSheafFor P R
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.toFinsupp_sub : ∀ {R : Type u} [inst : Ring R] (a b : Polynomial R), (a - b).toFinsupp = a.toFinsupp - b.toFinsupp
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.pair_eq_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ),
  f.pair g = MeasureTheory.AEEqFun.mk (fun x => (↑f x, ↑g x)) ⋯
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_erase : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {h' : a ∈ m.erase k},
  Std.DHashMap.Raw.Const.get (m.erase k) a h' = Std.DHashMap.Raw.Const.get m a ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer.0.CategoryTheory.Limits.equalizerPullbackMapIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasEqualizers C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y S T : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S}
  (hf : CategoryTheory.CategoryStruct.comp f t = s) (hg : CategoryTheory.CategoryStruct.comp g t = s) (v : T ⟶ S),
  CategoryTheory.Limits.equalizerPullbackMapIso hf hg v =
    {
      hom :=
        CategoryTheory.Limits.pullback.lift
          (CategoryTheory.Limits.equalizer.lift
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.equalizer.ι
                (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
                  (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
                (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
                  (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
              (CategoryTheory.Limits.pullback.fst s v))
            ⋯)
          (CategoryTheory.Limits.pullback.lift
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.equalizer.ι
                (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
                  (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
                (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
                  (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
              (CategoryTheory.Limits.pullback.fst s v))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.equalizer.ι
                (CategoryTheory.Limits.pullback.map s v t v f (CategoryTheory.CategoryStruct.id T)
                  (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
                (CategoryTheory.Limits.pullback.map s v t v g (CategoryTheory.CategoryStruct.id T)
                  (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))
              (CategoryTheory.Limits.pullback.snd s v))
            ⋯)
          ⋯,
      inv :=
        CategoryTheory.Limits.equalizer.lift
          (CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.equalizer.ι f g)
            (CategoryTheory.Limits.pullback.fst s v) s v (CategoryTheory.Limits.equalizer.ι f g)
            (CategoryTheory.Limits.pullback.snd s v) s ⋯ ⋯)
          ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }