mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Finset.Powerset
Finset.empty_mem_ssubsets : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α}, s.Nonempty → ∅ ∈ s.ssubsets
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.one_lt_rootMultiplicity_iff_isRoot_iterate_derivative : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R},
  p ≠ 0 → (1 < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ 1, ((⇑Polynomial.derivative)^[m] p).IsRoot t)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `S` is a multiplicative subset of a ring `R` and `M` an `R`-module, then
we can localize `M` by `S`.
 -/
LocalizedModule : {R : Type u} →
  [inst : CommSemiring R] → Submonoid R → (M : Type v) → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u v)
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonUnitalCommSemiringWithConvMatrix : {m : Type u_1} →
  {n : Type u_2} → {α : Type u_3} → [NonUnitalCommSemiring α] → NonUnitalCommSemiring (WithConv (Matrix m n α))
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.finsetProd : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι] {𝔸' : Type u_3}
  [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'} {f' : ι → 𝔸'},
  (∀ i ∈ u, HasStrictDerivAt (f i) (f' i) x) →
    HasStrictDerivAt (∏ i ∈ u, f i) (∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • f' i) x
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_inf_comap_of_surjective : ∀ {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₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Surjective ⇑f →
    ∀ (p q : Submodule R₂ M₂), Submodule.map f (Submodule.comap f p ⊓ Submodule.comap f q) = p ⊓ q
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.stalkIso.eq_1 : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (x : ↥(AlgebraicGeometry.Proj 𝒜)),
  AlgebraicGeometry.Proj.stalkIso 𝒜 x = (AlgebraicGeometry.Proj.stalkIso' 𝒜 x).toCommRingCatIso
-- Mathlib.Algebra.Module.Equiv.Basic
addMonoidHomLequivInt_symm_apply : ∀ {A : Type u_9} {B : Type u_10} (R : Type u_11) [inst : Semiring R] [inst_1 : AddCommGroup A] [inst_2 : AddCommGroup B]
  [inst_3 : Module R B] (f : A →ₗ[ℤ] B), (addMonoidHomLequivInt R).symm f = f.toAddMonoidHom
-- Mathlib.LinearAlgebra.DirectSum.TensorProduct
TensorProduct.directSumRight_tmul : ∀ (R : Type u) [inst : CommSemiring R] (S : Type u_1) [inst_1 : Semiring S] [inst_2 : Algebra R S] {ι₂ : Type v₂}
  [inst_3 : DecidableEq ι₂] {M₁' : Type w₁'} {M₂ : ι₂ → Type w₂} [inst_4 : AddCommMonoid M₁']
  [inst_5 : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)] [inst_6 : Module R M₁'] [inst_7 : (i₂ : ι₂) → Module R (M₂ i₂)]
  [inst_8 : Module S M₁'] [inst_9 : IsScalarTower R S M₁'] (m : M₁') (n : DirectSum ι₂ fun i => M₂ i) (i : ι₂),
  ((TensorProduct.directSumRight R S M₁' M₂) (m ⊗ₜ[R] n)) i = m ⊗ₜ[R] n i
-- Mathlib.Tactic.Simps.Basic
/-- Configuration for `@[simps]` attribute.  -/
Lean.Parser.Attr.simpsConfig : Lean.ParserDescr
-- Init.Data.Vector.Zip
_private.Init.Data.Vector.Zip.0.Vector.getElem?_zipWith.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : Option α → Option β → Sort u_3) →
      (x : Option α) →
        (x_1 : Option β) →
          ((a : α) → (b : β) → motive (some a) (some b)) →
            ((x : Option α) →
                (x_2 : Option β) → (∀ (a : α) (b : β), x = some a → x_2 = some b → False) → motive x x_2) →
              motive x x_1
-- Init.Data.Array.Lemmas
Array.all_flatten : ∀ {α : Type u_1} {f : α → Bool} {xss : Array (Array α)}, xss.flatten.all f = xss.all fun x => x.all f
-- Lean.Expr
/-- Annotate `e` with `pp.universes := flag`
The delaborator uses `pp` options.
 -/
Lean.Expr.setPPUniverses : Lean.Expr → Bool → Lean.Expr
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkItem.mk : Std.Format → ℤ → ℕ → Std.Format.WorkItem✝
-- Init.Data.UInt.Lemmas
USize.toNat_mod_lt : ∀ {m : ℕ} (u : USize), 0 < m → (u % USize.ofNat m).toNat < m
-- Mathlib.Combinatorics.Graph.Basic
Graph.mk.injEq : ∀ {α : Type u_3} {β : Type u_4} (vertexSet : Set α) (IsLink : β → α → α → Prop) (edgeSet : Set β)
  (isLink_symm : ∀ ⦃e : β⦄, e ∈ edgeSet → Std.Symm (IsLink e))
  (eq_or_eq_of_isLink_of_isLink : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink e x y → IsLink e v w → x = v ∨ x = w)
  (edge_mem_iff_exists_isLink :
    autoParam (∀ (e : β), e ∈ edgeSet ↔ ∃ x y, IsLink e x y) Graph.edge_mem_iff_exists_isLink._autoParam)
  (left_mem_of_isLink :
    autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink e x y → x ∈ vertexSet) Graph.left_mem_of_isLink._autoParam)
  (vertexSet_1 : Set α) (IsLink_1 : β → α → α → Prop) (edgeSet_1 : Set β)
  (isLink_symm_1 : ∀ ⦃e : β⦄, e ∈ edgeSet_1 → Std.Symm (IsLink_1 e))
  (eq_or_eq_of_isLink_of_isLink_1 : ∀ ⦃e : β⦄ ⦃x y v w : α⦄, IsLink_1 e x y → IsLink_1 e v w → x = v ∨ x = w)
  (edge_mem_iff_exists_isLink_1 :
    autoParam (∀ (e : β), e ∈ edgeSet_1 ↔ ∃ x y, IsLink_1 e x y) Graph.edge_mem_iff_exists_isLink._autoParam)
  (left_mem_of_isLink_1 :
    autoParam (∀ ⦃e : β⦄ ⦃x y : α⦄, IsLink_1 e x y → x ∈ vertexSet_1) Graph.left_mem_of_isLink._autoParam),
  ({ vertexSet := vertexSet, IsLink := IsLink, edgeSet := edgeSet, isLink_symm := isLink_symm,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink, left_mem_of_isLink := left_mem_of_isLink } =
      { vertexSet := vertexSet_1, IsLink := IsLink_1, edgeSet := edgeSet_1, isLink_symm := isLink_symm_1,
        eq_or_eq_of_isLink_of_isLink := eq_or_eq_of_isLink_of_isLink_1,
        edge_mem_iff_exists_isLink := edge_mem_iff_exists_isLink_1, left_mem_of_isLink := left_mem_of_isLink_1 }) =
    (vertexSet = vertexSet_1 ∧ IsLink = IsLink_1 ∧ edgeSet = edgeSet_1)
-- Init.Prelude
instMulNat : Mul ℕ
-- Lean.Parser.Term
Lean.Parser.Term.matchExprPat.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.RingHomProperties
RingHom.StableUnderComposition.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Mathlib.NumberTheory.MulChar.Basic
/-- Evaluation of the trivial character  -/
MulChar.one_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] {x : R}, IsUnit x → 1 x = 1
-- Lean.Data.AssocList
Lean.AssocList.isEmpty : {α : Type u} → {β : Type v} → Lean.AssocList α β → Bool
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- If `R` is a presieve such that `F.IsPrestackFor R`, then the functor
`F.toDescentData (fun (f : R.category) ↦ f.obj.hom)` is fully faithful.  -/
CategoryTheory.Pseudofunctor.IsPrestackFor.fullyFaithful : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {S : C} → {R : CategoryTheory.Presieve S} → F.IsPrestackFor R → (F.toDescentData fun f => f.obj.hom).FullyFaithful
-- Mathlib.MeasureTheory.PiSystem
/-- The least Dynkin system containing a collection of basic sets.
This inductive type gives the underlying collection of sets.  -/
MeasurableSpace.DynkinSystem.GenerateHas : {α : Type u_3} → Set (Set α) → Set α → Prop
-- Mathlib.RingTheory.Ideal.Maps
RingHom.instIsTwoSidedKer : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S]
  [rcf : RingHomClass F R S] (f : F), (RingHom.ker f).IsTwoSided
-- Lean.Parser.Term
/-- `let` is used to declare a local definition. Example:
```
let x := 1
let y := x + 1
x + y
```
Since functions are first class citizens in Lean, you can use `let` to declare
local functions too.
```
let double := fun x => 2*x
double (double 3)
```
For recursive definitions, you should use `let rec`.
You can also perform pattern matching using `let`. For example,
assume `p` has type `Nat × Nat`, then you can write
```
let (x, y) := p
x + y
```

The *anaphoric let* `let := v` defines a variable called `this`.
 -/
Lean.Parser.Term.let : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_eq_integral_norm_rpow_toReal : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E},
  p ≠ 0 →
    p ≠ ⊤ →
      MeasureTheory.AEStronglyMeasurable f μ →
        MeasureTheory.lpNorm f p μ = (∫ (x : α), ‖f x‖ ^ p.toReal ∂μ) ^ p.toReal⁻¹
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.Context : Type
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.preimage_image_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (p : F' ⟶ F) [hp : CategoryTheory.Epi p], (G.preimage p).image p = G
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.ι_additiveObjIsoBiproduct_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D) [inst_4 : F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι)
  {Z : D} (h : F.obj M ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.ι (fun i => F.obj ((CategoryTheory.Mat_.embedding C).obj (M.X i))) i)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv h) =
    CategoryTheory.CategoryStruct.comp
      (F.map
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.biproduct.ι (fun i => (CategoryTheory.Mat_.embedding C).obj (M.X i)) i)
          M.isoBiproductEmbedding.inv))
      h
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedLinearMap.isBigO_id : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : Module 𝕜 F] {f : E → F},
  IsBoundedLinearMap 𝕜 f → ∀ (l : Filter E), f =O[l] fun x => x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k},
      (t.insert k v).maxKey? = some (t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k')
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.symm_ofSnowflaking : ∀ {X : Type u_1} {α : ℝ} {hα₀ : 0 < α} {hα₁ : α ≤ 1},
  Metric.Snowflaking.ofSnowflaking.symm = Metric.Snowflaking.toSnowflaking
-- Mathlib.MeasureTheory.Measure.Haar.Basic
MeasureTheory.Measure.haar.chaar.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G]
  (K₀ : TopologicalSpace.PositiveCompacts G) (K : TopologicalSpace.Compacts G),
  MeasureTheory.Measure.haar.chaar K₀ K = Classical.choose ⋯ K
-- Mathlib.RingTheory.WittVector.Defs
WittVector.add_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x y : WittVector p R) (n : ℕ),
  (x + y).coeff n = WittVector.peval (WittVector.wittAdd p n) ![x.coeff, y.coeff]
-- Std.Data.TreeSet.Basic
/-- Inserts the given element into the set. 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.

Note: this non-replacement behavior is true for `TreeSet` and `TreeSet.Raw`.
The `insert` function on `TreeMap`, `DTreeMap`, `TreeMap.Raw` and `DTreeMap.Raw` behaves
differently: it will overwrite an existing mapping.
 -/
Std.TreeSet.insert : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → α → Std.TreeSet α cmp
-- Lean.Widget.Diff
/-- A description of the differences between a pair of expressions `before`, `after : Expr`.
The information can be used to display a 'visual diff' for
either `before`, showing the parts of the expression that are about to change,
or `after` showing which parts of the expression have changed.  -/
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff : Type
-- Mathlib.Algebra.Category.CommAlgCat.Monoidal
CommAlgCat.fst_unop_hom : ∀ {R : Type u} [inst : CommRing R] (A B : (CommAlgCat R)ᵒᵖ),
  CommAlgCat.Hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst A B).unop = Algebra.TensorProduct.includeLeft
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instNeg.eq_1 : ∀ {α : Type u_1} [inst : Neg α], Lex.instNeg = inst
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Asserts that `IteratorLoop.rel` is well-founded.
 -/
Std.IteratorLoop.WellFounded : (α : Type w) →
  (m : Type w → Type w') → {β : Type w} → [Std.Iterator α m β] → {γ : Type x} → (β → γ → ForInStep γ → Prop) → Prop
-- Lean.Meta.DecLevel
/-- If `true`, then `decAux? ?m` returns a fresh metavariable `?n` s.t.
`?m := ?n+1`.
 -/
Lean.Meta.DecLevelContext.canAssignMVars : Lean.Meta.DecLevelContext → Bool
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.instNorm : {ι : Type u_1} →
  [Fintype ι] →
    {𝕜 : Type u_2} →
      {E : ι → Type u_3} →
        [inst : (i : ι) → SeminormedAddCommGroup (E i)] →
          [inst_1 : NormedField 𝕜] → [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] → Norm (PiTensorProduct 𝕜 fun i => E i)
-- Mathlib.RingTheory.NormalClosure
Ring.instIsFractionRingNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsDomain R] [inst_3 : IsDomain S]
  [inst_4 : Algebra R S] [inst_5 : Module.IsTorsionFree R S] [Module.Finite R S],
  IsFractionRing (Ring.NormalClosure R S)
    ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S) (AlgebraicClosure (FractionRing S)))
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyFunctor_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.homologyFunctor C).obj S = S.homology
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (D : F.DescentData' sq sq₃) ⦃Y : C⦄ (q : Y ⟶ S) ⦃i : ι⦄ (g : Y ⟶ X i)
  (hg :
    autoParam (CategoryTheory.CategoryStruct.comp g (f i) = q)
      CategoryTheory.Pseudofunctor.DescentData'.pullHom'_self._auto_1),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' D.hom q g g hg hg =
    CategoryTheory.CategoryStruct.id ((F.map g.op.toLoc).toFunctor.obj (D.obj i))
-- Std.Sync.Notify
Std.Notify.Consumer.select.injEq : ∀ {α : Type} (finished finished_1 : Std.Async.Waiter α),
  (Std.Notify.Consumer.select finished = Std.Notify.Consumer.select finished_1) = (finished = finished_1)
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {_P : CategoryTheory.MorphismProperty C}
  {inst_1 : _P.IsMultiplicative} {x y : CategoryTheory.WideSubcategory _P}, x.obj = y.obj → x = y
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.associator_inv_hom : ∀ (X Y Z : SFinKer),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.hom =
    ProbabilityTheory.Kernel.deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯
-- Init.Data.SInt.Lemmas
ISize.add_right_neg : ∀ (a : ISize), a + -a = 0
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.det_eq_sum_mul_adjugate_row : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (i : n), A.det = ∑ j, A i j * A.adjugate j i
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The completed Riemann zeta function `Λ(s)` is differentiable away from `s = 0` and `s = 1`.  -/
differentiableAt_completedZeta : ∀ {s : ℂ}, s ≠ 0 → s ≠ 1 → DifferentiableAt ℂ completedRiemannZeta s
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative
`1` at zero, as long as it converges on a neighborhood of zero.  -/
hasDerivAt_exp_zero_of_radius_pos : ∀ {𝕂 : Type u_1} [inst : NontriviallyNormedField 𝕂] [CompleteSpace 𝕂] [CharZero 𝕂],
  0 < (NormedSpace.expSeries 𝕂 𝕂).radius → HasDerivAt NormedSpace.exp 1 0
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
MeasureTheory.Measure.sigmaFiniteSetWRT.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ ν : MeasureTheory.Measure α),
  μ.sigmaFiniteSetWRT ν =
    if h : ∃ s, MeasurableSet s ∧ MeasureTheory.SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤ then h.choose
    else ∅
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.mono_measure' : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s : Set α} {μ ν : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε],
  MeasureTheory.IntegrableOn f s ν → μ.restrict s ≤ ν.restrict s → MeasureTheory.IntegrableOn f s μ
-- Mathlib.Order.CountableSupClosed
countableSupClosure_eq_sInter : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), countableSupClosure s = ⋂₀ {t | s ⊆ t ∧ CountableSupClosed t}
-- Mathlib.Order.Filter.Pointwise
Filter.instAdd.eq_1 : ∀ {α : Type u_2} [inst : Add α],
  Filter.instAdd =
    {
      add := fun f g =>
        let __src := Filter.map₂ (fun x1 x2 => x1 + x2) f g;
        { sets := {s | ∃ t₁ ∈ f, ∃ t₂ ∈ g, t₁ + t₂ ⊆ s}, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ } }
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.forget_createsLimits.eq_1 : MonCat.forget_createsLimits = MonCat.forget_createsLimitsOfSize
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α} [inst_4 : Inhabited β],
  (List.map Prod.fst l).contains k = false →
    Std.DHashMap.Internal.Raw₀.Const.get!
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k =
      default
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mul : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : Mul β] [ContinuousMul β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f * g) μ
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instLT : {n : ℕ} → LT (BitVec n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_inj : ∀ {x y : ℝ}, Real.arctan x = Real.arctan y ↔ x = y
-- Batteries.Data.Nat.Lemmas
Nat.recDiag_zero_succ : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 n → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive m 0 → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive m n → motive (m + 1) (n + 1))
  (n : ℕ),
  Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 (n + 1) =
    zero_succ n (Nat.recDiag zero_zero zero_succ succ_zero succ_succ 0 n)
-- Mathlib.CategoryTheory.ObjectProperty.Extensions
CategoryTheory.ObjectProperty.instIsClosedUnderExtensionsInverseImageOfPreservesZeroMorphismsOfPreservesFiniteLimitsOfPreservesFiniteColimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [P.IsClosedUnderExtensions]
  (F : CategoryTheory.Functor D C) [inst_4 : CategoryTheory.Limits.HasZeroMorphisms D] [F.PreservesZeroMorphisms]
  [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.PreservesFiniteColimits F],
  (P.inverseImage F).IsClosedUnderExtensions
-- Mathlib.Analysis.Calculus.LocalExtr.Basic
/-- **Fermat's Theorem**: the derivative of a function at a local maximum equals zero.  -/
IsLocalMax.hasFDerivAt_eq_zero : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {a : E},
  IsLocalMax f a → HasFDerivAt f f' a → f' = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.size_filter_le_size : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] {f : α → β → Bool},
  (↑m).WF → (↑(Std.DHashMap.Internal.Raw₀.filter f m)).size ≤ (↑m).size
-- Mathlib.Order.Hom.CompleteLattice
Equiv.toOrderIsoSet_apply : ∀ {α : Type u_2} {β : Type u_3} (e : α ≃ β) (s : Set α), e.toOrderIsoSet s = ⇑e '' s
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.reduct_struc : ∀ {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} (φ : L →ᴸ L') (M : (φ.onTheory T).ModelType),
  (FirstOrder.Language.Theory.ModelType.reduct φ M).struc = φ.reduct ↑M
-- Lean.Util.Trace
Lean.instExceptToTraceResultBool : {ε : Type} → Lean.ExceptToTraceResult ε Bool
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkCoyonedaEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X : Cᵒᵖ}
  {P : CategoryTheory.Functor C (Type w)},
  CategoryTheory.shrinkCoyonedaEquiv =
    {
      toFun := fun τ =>
        (CategoryTheory.ConcreteCategory.hom (τ.app (Opposite.unop X)))
          ((equivShrink ((CategoryTheory.yoneda.obj (Opposite.unop X)).obj X))
            (CategoryTheory.CategoryStruct.id (Opposite.unop X))),
      invFun := fun x =>
        {
          app := fun Y =>
            TypeCat.ofHom fun f =>
              (CategoryTheory.ConcreteCategory.hom (P.map ((equivShrink (Opposite.unop X ⟶ Y)).symm f))) x,
          naturality := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_cast_Icc : ∀ {m n : ℕ} (h : m = n) (i j : Fin n), Fin.cast h ⁻¹' Set.Icc i j = Set.Icc (Fin.cast ⋯ i) (Fin.cast ⋯ j)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- Two finite measures give equal values to all closed sets if the integrals of all bounded
continuous functions with respect to the two measures agree.  -/
MeasureTheory.measure_isClosed_eq_of_forall_lintegral_eq_of_isFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω]
  [OpensMeasurableSpace Ω] {μ ν : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  (∀ (f : BoundedContinuousFunction Ω NNReal), ∫⁻ (x : Ω), ↑(f x) ∂μ = ∫⁻ (x : Ω), ↑(f x) ∂ν) →
    ∀ {F : Set Ω}, IsClosed F → μ F = ν F
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq.eq_3 : ∀ (a b : ℤ), Lean.Grind.instBEqIntInterval.beq (Lean.Grind.IntInterval.io a) (Lean.Grind.IntInterval.io b) = (a == b)
-- Mathlib.Order.PiLex
Pi.toColex_strictMono : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedGT ι],
  StrictMono ⇑toColex
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
CategoryTheory.Projective.Type.enoughProjectives : CategoryTheory.EnoughProjectives (Type u)
-- Mathlib.Analysis.Normed.Group.Pointwise
closedBall_one_mul_singleton : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), Metric.closedBall 1 δ * {x} = Metric.closedBall x δ