mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] [inst_4 : SizeOf 𝕜] [inst_5 : SizeOf E]
  [inst_6 : SizeOf H] (toPartialEquiv : PartialEquiv H E) (source_eq : toPartialEquiv.source = Set.univ)
  (convex_range' :
    if h : IsRCLikeNormedField 𝕜 then Convex ℝ (Set.range ↑toPartialEquiv) else Set.range ↑toPartialEquiv = Set.univ)
  (nonempty_interior' : (interior (Set.range ↑toPartialEquiv)).Nonempty)
  (continuous_toFun : autoParam (Continuous ↑toPartialEquiv) ModelWithCorners.continuous_toFun._autoParam)
  (continuous_invFun : autoParam (Continuous toPartialEquiv.invFun) ModelWithCorners.continuous_invFun._autoParam),
  sizeOf
      { toPartialEquiv := toPartialEquiv, source_eq := source_eq, convex_range' := convex_range',
        nonempty_interior' := nonempty_interior', continuous_toFun := continuous_toFun,
        continuous_invFun := continuous_invFun } =
    1 + sizeOf toPartialEquiv + sizeOf source_eq + sizeOf convex_range' + sizeOf nonempty_interior' +
        sizeOf continuous_toFun +
      sizeOf continuous_invFun
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. An integrable function is smaller than its mean on a set of positive
measure.  -/
MeasureTheory.measure_le_average_pos : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ} [MeasureTheory.IsFiniteMeasure μ],
  μ ≠ 0 → MeasureTheory.Integrable f μ → 0 < μ {x | f x ≤ ⨍ (a : α), f a ∂μ}
-- Lean.Elab.PreDefinition.TerminationHint
Lean.Elab.DecreasingBy.mk.injEq : ∀ (ref : Lean.Syntax) (tactic : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq) (ref_1 : Lean.Syntax)
  (tactic_1 : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq),
  ({ ref := ref, tactic := tactic } = { ref := ref_1, tactic := tactic_1 }) = (ref = ref_1 ∧ tactic = tactic_1)
-- Init.Data.String.Lemmas.Order
String.Pos.ne_startPos_of_sliceFrom_ne_startPos : ∀ {s : String} {p p₀ : s.Pos} {h₀ : p₀ ≤ p}, p₀.sliceFrom p h₀ ≠ (s.sliceFrom p₀).startPos → p ≠ s.startPos
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Real.abs_cos_eq_one_iff : ∀ {x : ℝ}, |Real.cos x| = 1 ↔ ∃ k, ↑k * Real.pi = x
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.instDecidableRelFinAdjTuranGraph : {n r : ℕ} → DecidableRel (SimpleGraph.turanGraph n r).Adj
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_comp : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R} [NoZeroDivisors R],
  (p.comp q).natDegree = p.natDegree * q.natDegree
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a right absorbing element for multiplication  -/
SemigroupWithZero.mul_zero : ∀ {S₀ : Type u} [self : SemigroupWithZero S₀] (a : S₀), a * 0 = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.PInfty_toNormalizedChainComplex_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) {Z : ChainComplex C ℕ}
  (h : X.normalizedChainComplex R ⟶ Z),
  CategoryTheory.CategoryStruct.comp AlgebraicTopology.DoldKan.PInfty
      (CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) h) =
    CategoryTheory.CategoryStruct.comp (X.toNormalizedChainComplex R) h
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalStarAlgHom.range.congr_simp : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (φ φ_1 : F),
  φ = φ_1 → NonUnitalStarAlgHom.range φ = NonUnitalStarAlgHom.range φ_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.cofan_inj_comp_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : CategoryTheory.SimplicialObject C}
  (s : X.Splitting) (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ),
  CategoryTheory.CategoryStruct.comp ((s.cofan Δ).inj A) (f.app Δ) =
    CategoryTheory.CategoryStruct.comp (s.φ f (Opposite.unop A.fst).len) (Y.map A.e.op)
-- Std.Data.DHashMap.Basic
/-- The number of mappings present in the hash map  -/
Std.DHashMap.size : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → Std.DHashMap α β → ℕ
-- Mathlib.NumberTheory.SmoothNumbers
/-- The `k`-smooth numbers up to and including `N` as a `Finset`  -/
Nat.smoothNumbersUpTo : ℕ → ℕ → Finset ℕ
-- Mathlib.Topology.Algebra.Group.Matrix
/-- The natural map from `SL n A` to `GL n A` is continuous.  -/
Matrix.SpecialLinearGroup.continuous_toGL : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R], Continuous ⇑Matrix.SpecialLinearGroup.toGL
-- Mathlib.RingTheory.LocalRing.Module
/-- If `M` is a finite flat module over a commutative semilocal ring `R` that has the same rank `n`
at every maximal ideal, then `M` is free of rank `n`.  -/
Module.nonempty_basis_of_flat_of_finrank_eq : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [Finite (MaximalSpectrum R)] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.Finite R M] [Module.Flat R M] (n : ℕ),
  (∀ (P : MaximalSpectrum R), Module.finrank (R ⧸ P.asIdeal) (TensorProduct R (R ⧸ P.asIdeal) M) = n) →
    Nonempty (Module.Basis (Fin n) R M)
-- Init.Dynamic
/-- Retrieves the value stored in the `Dynamic`.
Returns `some a` if the value has the right type, and `none` otherwise.
 -/
Dynamic.get? : (α : Type u_1) → Dynamic → [TypeName α] → Option α
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientKerEquivRangeₐ_mkₐ : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (f : M →ₐ[R] P) (x : M), (RingCon.quotientKerEquivRangeₐ f) ↑x = ⟨f x, ⋯⟩
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.instIsScalarTower : ∀ (X : Type u_2) {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : SMul R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A],
  IsScalarTower R S (FreeAlgebra A X)
-- Init.Data.Vector.Lex
Vector.le_iff_lt_or_eq : ∀ {α : Type u_1} {n : ℕ} [inst : LT α] [Std.Asymm fun x1 x2 => x1 < x2] [Std.Trichotomous fun x1 x2 => x1 < x2]
  {xs ys : Vector α n}, xs ≤ ys ↔ xs < ys ∨ xs = ys
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- The functor `StructuredArrow L R ⥤ StructuredArrow L' R'` that is deduced from
a natural transformation `R ⋙ G ⟶ F ⋙ R'` and a morphism `L' ⟶ G.obj L.`  -/
CategoryTheory.StructuredArrow.map₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {A : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} A] →
            {B : Type u₄} →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} B] →
                {L : D} →
                  {R : CategoryTheory.Functor C D} →
                    {L' : B} →
                      {R' : CategoryTheory.Functor A B} →
                        {F : CategoryTheory.Functor C A} →
                          {G : CategoryTheory.Functor D B} →
                            (L' ⟶ G.obj L) →
                              (R.comp G ⟶ F.comp R') →
                                CategoryTheory.Functor (CategoryTheory.StructuredArrow L R)
                                  (CategoryTheory.StructuredArrow L' R')
-- Mathlib.CategoryTheory.EffectiveEpi.Preserves
CategoryTheory.Functor.regularEpiOfPreserves_W : ∀ {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_3, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_4} D] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.EffectiveEpi f]
  (F : CategoryTheory.Functor C D) [inst_3 : F.PreservesEffectiveEpis]
  [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F]
  (c : CategoryTheory.Limits.PullbackCone f f) (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.Functor.regularEpiOfPreserves f F c hc).W = F.obj c.pt
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrLemma.mk.sizeOf_spec : ∀ (keys : List Mathlib.Tactic.GCongr.GCongrKey) (declName : Lean.Name)
  (mainSubgoals : Array Mathlib.Tactic.GCongr.GCongrHyp) (numHyps prio numVarying : ℕ) (forGrw : Bool),
  sizeOf
      { keys := keys, declName := declName, mainSubgoals := mainSubgoals, numHyps := numHyps, prio := prio,
        numVarying := numVarying, forGrw := forGrw } =
    1 + sizeOf keys + sizeOf declName + sizeOf mainSubgoals + sizeOf numHyps + sizeOf prio + sizeOf numVarying +
      sizeOf forGrw
-- Mathlib.Topology.Constructions.SumProd
/-- **Alias** of `Continuous.curry_right`.

---

Continuous functions on products are continuous in their second argument  -/
Continuous.along_snd : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X × Y → Z}, Continuous f → ∀ {x : X}, Continuous fun y => f (x, y)
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.continue.sizeOf_spec : ∀ (pat : Lean.Expr), sizeOf (Lean.Meta.Grind.EMatch.Cnstr.continue pat) = 1 + sizeOf pat
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.closure_latticeClosure : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (s : Set α),
  BooleanSubalgebra.closure (latticeClosure s) = BooleanSubalgebra.closure s
-- Mathlib.Util.CountHeartbeats
/-- `#count_heartbeats tac` counts the heartbeats used by the tactic sequence `tac`
and prints an info line with the number of heartbeats.

* `#count_heartbeats! n in tac`, where `n` is an optional natural number literal, runs `tac`
  `n` times on the same goal while counting the heartbeats, and prints an info line with range and
  standard deviation. `n` can be left out, and defaults to 10.

Example:

```
example : 1 + 1 = 2 := by
  -- The next line will print an info message of this format; the exact number may vary.
  -- info: 4646
  #count_heartbeats simp

example : 1 + 1 = 2 := by
  -- The next line will print an info message of this format; the exact numbers may vary.
  -- info: Min: 4 Max: 4 StdDev: 2%
  #count_heartbeats! 37 in simp
```
 -/
Mathlib.CountHeartbeats.«tactic#count_heartbeats_» : Lean.ParserDescr
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.get!.eq_2 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] (a k : α) (v : β)
  (es : Std.DHashMap.Internal.AssocList α fun x => β),
  Std.DHashMap.Internal.AssocList.get! a (Std.DHashMap.Internal.AssocList.cons k v es) =
    bif k == a then v else Std.DHashMap.Internal.AssocList.get! a es
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The multicoequalizer is isomorphic to the coequalizer of `∐ I.left ⇉ ∐ I.right`.  -/
CategoryTheory.Limits.Multicoequalizer.isoCoequalizer : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasMulticoequalizer I] →
          [inst_2 : CategoryTheory.Limits.HasCoproduct I.left] →
            [inst_3 : CategoryTheory.Limits.HasCoproduct I.right] →
              CategoryTheory.Limits.multicoequalizer I ≅ CategoryTheory.Limits.coequalizer I.fstSigmaMap I.sndSigmaMap
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.opParallelPairIso_inv_app_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f g : X ⟶ Y),
  (CategoryTheory.Limits.opParallelPairIso f g).inv.app (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Limits.walkingParallelPairOpEquiv.inverse.comp
            (CategoryTheory.Limits.parallelPair f.op g.op)).obj
        (Opposite.op CategoryTheory.Limits.WalkingParallelPair.zero))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKeyD_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k : α} {v : β k} {fallback : α},
  (compare k ((Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl.maxKeyD fallback)).isLE = true
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.noRepetition_cons_append_append_iff : ∀ {α : Type u} {a : α} {l : List α},
  NoRepetition✝ a (a :: (l ++ [a])) ↔ l ≠ [] ∧ ¬[a, a] <:+: l ∧ l.head? ≠ some a ∧ l.getLast? ≠ some a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.size_alter_eq_self_of_not_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : LawfulBEq α] {k : α} {f : Option β → Option β},
  m.WF →
    k ∉ m → (f (Std.DHashMap.Raw.Const.get? m k)).isNone = true → (Std.DHashMap.Raw.Const.alter m k f).size = m.size
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (x y : CochainComplex.HomComplex.CohomologyClass R.cochainComplex ((CochainComplex.singleFunctor C 0).obj Y) ↑n),
  R.extEquivCohomologyClass.symm (x - y) = R.extEquivCohomologyClass.symm x - R.extEquivCohomologyClass.symm y
-- Mathlib.Data.Finset.Defs
Finset.subset_iff_notMem : ∀ {α : Type u_1} {s t : Finset α}, s ⊆ t ↔ ∀ ⦃a : α⦄, a ∉ t → a ∉ s
-- Mathlib.MeasureTheory.Measure.Dirac
MeasureTheory.Measure.dirac_apply_of_mem : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : Set α} {a : α}, a ∈ s → (MeasureTheory.Measure.dirac a) s = 1
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- If two measures coincide locally, then a set which is everywhere positive for the former is
also everywhere positive for the latter.  -/
MeasureTheory.Measure.IsEverywherePos.of_forall_exists_nhds_eq : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ ν : MeasureTheory.Measure α} {s : Set α},
  μ.IsEverywherePos s → (∀ x ∈ s, ∃ t ∈ nhds x, ∀ u ⊆ t, ν u = μ u) → ν.IsEverywherePos s
-- Mathlib.Tactic.WLOG
/-- The original goal with the additional assumption `h : P`.  -/
Mathlib.Tactic.WLOGResult.hypothesisGoal : Mathlib.Tactic.WLOGResult → Lean.MVarId
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.lsmul_flip_inj : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (R : Type u_3) [inst_3 : SeminormedRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : IsBoundedSMul R E] [inst_7 : IsScalarTower 𝕜 R E] {x y : E},
  (ContinuousLinearMap.lsmul 𝕜 R).flip x = (ContinuousLinearMap.lsmul 𝕜 R).flip y ↔ x = y
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize.eq_def : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (v : α → M) (x : L.Term α),
  FirstOrder.Language.Term.realize v x =
    match x with
    | FirstOrder.Language.var k => v k
    | FirstOrder.Language.func f ts =>
      FirstOrder.Language.Structure.funMap f fun i => FirstOrder.Language.Term.realize v (ts i)
-- Mathlib.Algebra.Algebra.Hom
RingHom.toIntAlgHom_coe : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), ⇑f.toIntAlgHom = ⇑f
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [inst_1 : Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).isEmpty = false →
    ((t.alter k f).minKey! = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] {Δ Δ' : SimplexCategoryᵒᵖ}
  (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) (θ : Δ ⟶ Δ') {Z : C}
  (h : (AlgebraicTopology.DoldKan.Γ₀.obj K).obj Δ' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ).inj A)
      (CategoryTheory.CategoryStruct.comp ((AlgebraicTopology.DoldKan.Γ₀.obj K).map θ) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K
          (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e)))
        (((AlgebraicTopology.DoldKan.Γ₀.splitting K).cofan Δ').inj (A.pull θ)))
      h
-- Mathlib.Probability.ProbabilityMassFunction.Monad
PMF.mem_support_pure_iff : ∀ {α : Type u_1} (a a' : α), a' ∈ (PMF.pure a).support ↔ a' = a
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.copy_eq : ∀ {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K)
  (f' : E → F) (h : f' = ⇑f), f.copy f' h = f
-- Mathlib.Data.Ordmap.Invariants
Ordnode.findMax'.eq_1 : ∀ {α : Type u_1} (x : α), Ordnode.findMax' x Ordnode.nil = x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- The Bochner integral  -/
MeasureTheory.«term∫_In_,_∂_» : Lean.ParserDescr
-- Std.Time.Format.DateFormat
/-- Short era names (2 elements: index 0 = BCE, index 1 = CE).
 -/
Std.Time.DateFormatSymbols.eraShort : Std.Time.DateFormatSymbols → Vector String 2
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.dropn_cons : ∀ {α : Type u} (a : α) (s : Stream'.WSeq α) (n : ℕ), (Stream'.WSeq.cons a s).drop (n + 1) = s.drop n
-- Init.Data.SInt.Basic
/-- Obtains the `Int8` that is 2's complement equivalent to the `UInt8`.  -/
UInt8.toInt8 : UInt8 → Int8
-- Mathlib.Algebra.Order.Archimedean.Hom
/-- There is at most one ordered ring isomorphism between a linear ordered field and an archimedean
linear ordered field.  -/
OrderRingIso.subsingleton_right : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : Field β] [inst_3 : LinearOrder β]
  [IsStrictOrderedRing β] [Archimedean β], Subsingleton (α ≃+*o β)
-- Init.Data.Range.Polymorphic.Nat
Std.instHasRcoIntersectionNat_4 : Std.Rcc.HasRcoIntersection ℕ
-- Mathlib.Topology.Neighborhoods
all_mem_nhds_filter : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} (x : X) (f : Set X → Set α),
  (∀ (s t : Set X), s ⊆ t → f s ⊆ f t) →
    ∀ (l : Filter α), (∀ s ∈ nhds x, f s ∈ l) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → f s ∈ l
-- Init.Data.List.Erase
List.IsPrefix.erase : ∀ {α : Type u_1} [inst : BEq α] (a : α) {l₁ l₂ : List α}, l₁ <+: l₂ → l₁.erase a <+: l₂.erase a
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.symm_refl : ∀ {k : Type u_1} {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁],
  (ContinuousAffineEquiv.refl k P₁).symm = ContinuousAffineEquiv.refl k P₁
-- Mathlib.Probability.Distributions.Binomial
ProbabilityTheory.isProbabilityMeasure_map_cast_binomial : ∀ {R : Type u_1} [inst : MeasurableSpace R] [inst_1 : AddMonoidWithOne R] {n : ℕ} {p : ↑unitInterval},
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.map Nat.cast (ProbabilityTheory.binomial n p))
-- Mathlib.Combinatorics.Additive.Dissociation
AddEquiv.addDissociated_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommGroup α] [inst_1 : AddCommGroup β] {s : Set α} (e : β ≃+ α),
  AddDissociated (⇑e ⁻¹' s) ↔ AddDissociated s
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (h : F = G) (X : C), (CategoryTheory.eqToHom h).app X = CategoryTheory.eqToHom ⋯
-- Mathlib.CategoryTheory.Adjunction.Reflective
/-- A reflective functor is fully faithful.  -/
CategoryTheory.Functor.fullyFaithfulOfReflective : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (i : CategoryTheory.Functor D C) → [CategoryTheory.Reflective i] → i.FullyFaithful
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_inter_subset : ∀ {α : Type u_2} [inst : Sub α] {s t₁ t₂ : Set α}, s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.meta : Lean.Parser.Parser
-- Mathlib.Order.BooleanAlgebra.Basic
compl_eq_comm : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], xᶜ = y ↔ yᶜ = x
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_unique : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C)
  {A : ↥(MeasureTheory.Lp E 1 μ) →L[ℝ] F},
  (∀ (f : ↥(α →₁ₛ[μ] E)), (MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT) f = A ↑f) →
    ∀ (f : ↥(MeasureTheory.Lp E 1 μ)), (MeasureTheory.L1.setToL1 hT) f = A f
-- Mathlib.Algebra.Order.Monoid.Lex
MonoidHom.snd_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Monoid α] [inst_1 : Preorder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  Monotone ⇑(MonoidHom.snd α β)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.RightUnitorBimod.hom_left_act_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C] {R S : CategoryTheory.Mon C} (P : Bimod R S)
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)],
  CategoryTheory.CategoryStruct.comp (P.tensorBimod (Bimod.regular S)).actLeft (Bimod.RightUnitorBimod.hom P) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R.X (Bimod.RightUnitorBimod.hom P)) P.actLeft
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.ne_top_of_tsum_ne_top : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (a : α), f a ≠ ⊤ → ∀ (a : α), f a ≠ ⊤