mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Given a diagram
```
a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S
```
such that `φ` is strongly Cartesian, and morphisms `φ' : a' ⟶ b`, `ψ : a' ⟶ a` such that
`ψ ≫ φ = φ'`. Then `ψ` is the map induced by the universal property.  -/
CategoryTheory.Functor.IsStronglyCartesian.map_uniq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsStronglyCartesian f φ]
  {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b)
  [inst_3 : p.IsHomLift f' φ'] (ψ : a' ⟶ a) [p.IsHomLift g ψ],
  CategoryTheory.CategoryStruct.comp ψ φ = φ' → ψ = CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ'
-- Mathlib.Algebra.Algebra.Epi
Algebra.tmul_comm : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [Algebra.IsEpi R A] (a b : A), a ⊗ₜ[R] b = b ⊗ₜ[R] a
-- Mathlib.RingTheory.IsGaloisGroup.Defs
/-- `G` is a Galois group for `L/K` if the action of `G` on `L` is faithful with fixed field `K`.
In particular, we do not assume that `L` is an algebraic extension of `K`.

See the implementation notes in this file for the meaning of this definition in the case of rings.
 -/
IsGaloisGroup : (G : Type u_1) →
  (A : Type u_2) →
    (B : Type u_4) →
      [inst : Group G] →
        [inst_1 : CommSemiring A] → [inst_2 : Semiring B] → [Algebra A B] → [MulSemiringAction G B] → Prop
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.appIso_hom_naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] {U V : X.Opens}
  (i : Opposite.op U ⟶ Opposite.op V) {Z : CommRingCat} (h : X.presheaf.obj (Opposite.op V) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).map i.unop).op)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f V).hom h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appIso f U).hom
      (CategoryTheory.CategoryStruct.comp (X.presheaf.map i) h)
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
/-- The base change of `R[M]` to an `R`-algebra `A` is isomorphic to `A[M]` as an `A`-algebra.  -/
AddMonoidAlgebra.scalarTensorEquiv : (R : Type u_1) →
  {M : Type u_2} →
    (A : Type u_5) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] → TensorProduct R A (AddMonoidAlgebra R M) ≃ₐ[A] AddMonoidAlgebra A M
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.coe_orderMonoidHom : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β] (f : α →*₀o β), ⇑↑f = ⇑f
-- Init.Omega.Constraint
/-- A constraint is satisfied at `t` is both the lower bound and upper bound are satisfied.  -/
Lean.Omega.Constraint.sat : Lean.Omega.Constraint → ℤ → Bool
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instInhabited.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M], SubMulAction.instInhabited = { default := ⊥ }
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalizedFactorsEquiv_apply : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {β : Type u_2} [inst_3 : CommMonoidWithZero β] [inst_4 : NormalizationMonoid β] [inst_5 : UniqueFactorizationMonoid β]
  {F : Type u_3} [inst_6 : EquivLike F α β] [inst_7 : MulEquivClass F α β] {f : F}
  (he : ∀ (x : α), normalize (f x) = f (normalize x)) {a p : α}
  (hp : p ∈ UniqueFactorizationMonoid.normalizedFactors a),
  ↑((UniqueFactorizationMonoid.normalizedFactorsEquiv he a) ⟨p, hp⟩) = f p
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.isStandardSmooth_algebraMap : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (algebraMap R S).IsStandardSmooth ↔ Algebra.IsStandardSmooth R S
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
/-- The composition of two spans: if the relevant pullback exists and if the
morphism properties are stable under the relevant base change, it is given by the
total span
```
     P
    /  \
   /    \
  X₁     X₂
 /  \   /  \
c     c'    c''
```
where the top diamond is a pullback square
 -/
CategoryTheory.Span.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} →
      [Wₗ.HasPullbacksAgainst Wᵣ] →
        [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] →
          [Wᵣ.IsStableUnderBaseChangeAgainst Wₗ] →
            [Wₗ.IsStableUnderComposition] →
              [Wᵣ.IsStableUnderComposition] →
                {c c' c'' : C} →
                  CategoryTheory.Span Wₗ Wᵣ c c' → CategoryTheory.Span Wₗ Wᵣ c' c'' → CategoryTheory.Span Wₗ Wᵣ c c''
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.toNonUnitalSubsemiring_eq_top : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S : NonUnitalSubring R}, S.toNonUnitalSubsemiring = ⊤ ↔ S = ⊤
-- Plausible.Testable
Plausible.instInhabitedConfiguration : Inhabited Plausible.Configuration
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.rightUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (P : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct P (⊤_ C)],
  (CategoryTheory.Limits.prod.rightUnitor P).hom = CategoryTheory.Limits.prod.fst
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.InverseDeriv
Real.differentiableOn_arccos : DifferentiableOn ℝ Real.arccos {-1, 1}ᶜ
-- Mathlib.Data.List.Zip
List.mem_zip_inits_tails : ∀ {α : Type u} {l init tail : List α}, (init, tail) ∈ l.inits.zip l.tails ↔ init ++ tail = l
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Any matrix can be reduced to diagonal form by elementary operations. Formulated here on `Type 0`
because we will make an induction using `Fin r`.
See `exists_list_transvec_mul_mul_list_transvec_eq_diagonal` for the general version (which follows
from this one and reindexing).  -/
Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_aux : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] (n : Type) [inst_1 : Fintype n] [inst_2 : DecidableEq n] (M : Matrix n n 𝕜),
  ∃ L L' D,
    (List.map Matrix.TransvectionStruct.toMatrix L).prod * M * (List.map Matrix.TransvectionStruct.toMatrix L').prod =
      Matrix.diagonal D
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_neg : ∀ (a : UInt8), (-a).toUInt64 = -a.toUInt64 % 256
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
contDiff_sigmoid : ContDiff ℝ ⊤ Real.sigmoid
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- Replace `toPartialEquiv` field to provide better definitional equalities.  -/
OpenPartialHomeomorph.replacePartialEquiv : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        (e : OpenPartialHomeomorph X Y) → (e' : PartialEquiv X Y) → e.toPartialEquiv = e' → OpenPartialHomeomorph X Y
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {s : Finset ι} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : NormedSpace ℝ E],
  (∀ i ∈ s, AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun (s.restrict X) P →
      MeasureTheory.charFunDual (MeasureTheory.Measure.map (∑ i ∈ s, X i) P) =
        ∏ i ∈ s, MeasureTheory.charFunDual (MeasureTheory.Measure.map (X i) P)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_eq_mapComp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂),
  F.mapComp' f g (CategoryTheory.CategoryStruct.comp f g) ⋯ = F.mapComp f g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey?_eq_getLast?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey? = t.keys.getLast?
-- Mathlib.Topology.Separation.Basic
Bornology.relativelyCompact.isBounded_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : R0Space X] {s : Set X},
  Bornology.IsBounded s ↔ IsCompact (closure s)
-- Std.Data.Iterators.Producers.Range
/-- Returns an iterator over the given range. This iterator will emit the elements of the range
in increasing order.
 -/
Std.Roo.iter : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → Std.Roo α → Std.Iter α
-- Mathlib.Computability.StateTransition
_private.Mathlib.Computability.StateTransition.0.StateTransition.Respects.match_1.eq_2 : ∀ {σ₁ : Type u_1} (motive : Option σ₁ → Sort u_2) (h_1 : (b₁ : σ₁) → motive (some b₁)) (h_2 : Unit → motive none),
  (match none with
    | some b₁ => h_1 b₁
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.corootSpan_dualAnnihilator_map_eq_iInf_ker_coroot' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  Submodule.map (↑P.toPerfPair.symm) (P.corootSpan R).dualAnnihilator = ⨅ i, LinearMap.ker (P.coroot' i)
-- Mathlib.Data.Seq.Computation
Computation.le_stable : ∀ {α : Type u} (s : Computation α) {a : α} {m n : ℕ}, m ≤ n → ↑s m = some a → ↑s n = some a
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_mul_eq_mk_right : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk b < MulArchimedeanClass.mk a → MulArchimedeanClass.mk (a * b) = MulArchimedeanClass.mk b
-- Init.Data.Array.Int
Array.prod_append_int : ∀ {as₁ as₂ : Array ℤ}, (as₁ ++ as₂).prod = as₁.prod * as₂.prod
-- Mathlib.Data.Finsupp.Single
Finsupp.erase_update_of_ne : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) {a a' : α},
  a ≠ a' → ∀ (b : M), Finsupp.erase a (f.update a' b) = (Finsupp.erase a f).update a' b
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuousOn_singleton_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  UpperHemicontinuousOn (fun x => {f x}) s ↔ ContinuousOn f s
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Instances
IsSelfAdjoint.instContinuousFunctionalCalculus : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [ContinuousFunctionalCalculus ℂ A IsStarNormal], ContinuousFunctionalCalculus ℝ A IsSelfAdjoint
-- Mathlib.Order.Monotone.Basic
/-- If `f` is an antitone function from `ℤ` to a preorder and `x` lies between `f (n + 1)` and
`f n`, then `x` doesn't lie in the range of `f`.  -/
Antitone.ne_of_lt_of_lt_int : ∀ {α : Type u} [inst : Preorder α] {f : ℤ → α},
  Antitone f → ∀ (n : ℤ) {x : α}, f (n + 1) < x → x < f n → ∀ (a : ℤ), f a ≠ x
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- An exponent of an element is less or equal than exponent of the extension.  -/
IsPurelyInseparable.elemExponent_le_exponent : ∀ (K : Type u_2) {L : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable K L] [inst_4 : IsPurelyInseparable.HasExponent K L] (a : L),
  IsPurelyInseparable.elemExponent K a ≤ IsPurelyInseparable.exponent K L
-- Mathlib.Data.Finset.Lattice.Basic
Finset.coe_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), ↑(s₁ ∪ s₂) = ↑s₁ ∪ ↑s₂
-- Mathlib.Algebra.Lie.Weights.RootSystem
LieAlgebra.IsKilling.biSup_corootSpace_eq_top : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [CharZero K] [inst_2 : LieRing L] [inst_3 : LieAlgebra K L]
  [LieAlgebra.IsKilling K L] [inst_5 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_6 : H.IsCartanSubalgebra]
  [LieModule.IsTriangularizable K (↥H) L], ⨆ α, ⨆ (_ : α.IsNonZero), LieAlgebra.corootSpace ⇑α = ⊤
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
/-- The partial derivative `W_X(X, Y)` with respect to `X` of the polynomial `W(X, Y)` associated to
a Weierstrass curve `W` in affine coordinates.  -/
WeierstrassCurve.Affine.polynomialX : {R : Type r} → [inst : CommRing R] → WeierstrassCurve.Affine R → Polynomial (Polynomial R)
-- Mathlib.Topology.Order.OrderClosed
SuccOrder.nhdsLT_eq_nhdsNE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] [SuccOrder α] (a : α),
  nhdsWithin a (Set.Iio a) = nhdsWithin a {a}ᶜ
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.down'_Rel : ∀ {α : Type u_2} [inst : Add α] [inst_1 : IsRightCancelAdd α] (a i j : α), (ComplexShape.down' a).Rel i j = (j + a = i)
-- Mathlib.SetTheory.Cardinal.EventuallyConst
Ordinal.eventuallyConst_of_monotone : ∀ {β : Type v} [inst : PartialOrder β] {f : Ordinal.{v} → β} [Small.{v, v} β],
  Monotone f → Filter.EventuallyConst f Filter.atTop
-- Mathlib.Analysis.Convex.Strict
StrictConvex.add_left : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] [ContinuousAdd E] {s : Set E},
  StrictConvex 𝕜 s → ∀ (z : E), StrictConvex 𝕜 ((fun x => z + x) '' s)
-- Mathlib.Analysis.Complex.Exponential
Complex.sum_div_factorial_le : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (n j : ℕ),
  0 < n → ∑ m ∈ Finset.range j with n ≤ m, 1 / ↑m.factorial ≤ ↑n.succ / (↑n.factorial * ↑n)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.pseudofunctor_mapComp : ∀ {a b c : CategoryTheory.Cat} (x : a ⟶ b) (x_1 : b ⟶ c),
  CategoryTheory.WithTerminal.pseudofunctor.mapComp x x_1 =
    CategoryTheory.Cat.Hom.isoMk (CategoryTheory.WithTerminal.mapComp x.toFunctor x_1.toFunctor)
-- Mathlib.Probability.Distributions.Gamma
/-- The gamma pdf is strongly measurable  -/
ProbabilityTheory.stronglyMeasurable_gammaPDFReal : ∀ (a r : ℝ), MeasureTheory.StronglyMeasurable (ProbabilityTheory.gammaPDFReal a r)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_Ioi_ae_eq_pi_Ici : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  {μ : (i : ι) → MeasureTheory.Measure (α i)} [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), MeasureTheory.NullSingletonClass (μ i)] {s : Set ι}
  {f : (i : ι) → α i}, (s.pi fun i => Set.Ioi (f i)) =ᵐ[MeasureTheory.Measure.pi μ] s.pi fun i => Set.Ici (f i)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.lowerCentralSeries_normal : ∀ {G : Type u_1} [inst : Group G] (S : Subgroup G) [S.Normal] (n : ℕ), (S.lowerCentralSeries n).Normal
-- Mathlib.Topology.Algebra.Ring.Compact
Ideal.isOpen_pow_of_isMaximal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal] (n : ℕ), IsOpen ↑(I ^ n)
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.IsIntegrallyClosed.unique_of_degree_le_degree_minpoly : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {s : S} {p : Polynomial R},
  p.Monic → (Polynomial.aeval s) p = 0 → p.degree ≤ (minpoly R s).degree → p = minpoly R s
-- Mathlib.LinearAlgebra.Complex.Module
Complex.coe_basisOneI : ⇑Complex.basisOneI = ![1, Complex.I]
-- Std.Http.Data.Method
Std.Http.Method.unlock.sizeOf_spec : sizeOf Std.Http.Method.unlock = 1
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_cons_left : ∀ {α : Type u_1} {a : α} {s t : Multiset α}, Disjoint (a ::ₘ s) t ↔ a ∉ t ∧ Disjoint s t
-- Mathlib.Topology.Convenient.ContinuousMapGeneratedBy
/-- The identity `WithGeneratedByTopology.equiv : WithGeneratedByTopology X Y → Y`
as a `X`-continuous map.  -/
Topology.WithGeneratedByTopology.equivAsContinuousMapGeneratedBy : {ι : Type t} →
  (X : ι → Type u) →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      (Y : Type v) →
        [inst_1 : TopologicalSpace Y] → Topology.ContinuousMapGeneratedBy X (Topology.WithGeneratedByTopology X Y) Y
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.bot_mem_precoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} (X : C),
  ⊥ ∈ P.precoverage.coverings X
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- A choice of a right fraction deduced from a left fraction for a morphism property `W`
when `W` has right calculus of fractions.  -/
CategoryTheory.MorphismProperty.LeftFraction.rightFraction : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} →
      [W.HasRightCalculusOfFractions] → {X Y : C} → W.LeftFraction X Y → W.RightFraction X Y
-- Init.PropLemmas
Decidable.not_imp_self : ∀ {a : Prop} [Decidable a], ¬a → a ↔ a
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Iic_pred_eq_Iio_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrderBot α] [inst_2 : PredOrder α] {b : α},
  ¬IsMin b → Finset.Iic (Order.pred b) = Finset.Iio b
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
/-- For any trivialization `e`, the differentiability of a section on `e.baseSet`
can be determined using `e`.  -/
Bundle.Trivialization.mdifferentiableOn_section_baseSet_iff : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (x : B) → TopologicalSpace (E x)] {EB : Type u_7} [inst_5 : NormedAddCommGroup EB]
  [inst_6 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_7 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB}
  [inst_8 : TopologicalSpace B] [inst_9 : ChartedSpace HB B] [inst_10 : FiberBundle F E]
  [inst_11 : (x : B) → AddCommMonoid (E x)] [inst_12 : (x : B) → Module 𝕜 (E x)] [inst_13 : VectorBundle 𝕜 F E]
  [ContMDiffVectorBundle 1 F E IB] {s : (x : B) → E x} (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [MemTrivializationAtlas e], MDiff[e.baseSet] (T% s) ↔ MDiff[e.baseSet] fun x => (↑e ⟨x, s x⟩).2
-- Mathlib.Order.SymmDiff
symmDiff_top : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] (a : α), symmDiff a ⊤ = ￢a
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.Overlap.zero.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {bt : Q(«$α») → Type} {sα : Q(CommSemiring «$α»)} {e : Q(«$α»)}
  (x x_1 : Q(Mathlib.Meta.NormNum.IsNat «$e» 0)),
  (Mathlib.Tactic.Ring.Common.Overlap.zero x = Mathlib.Tactic.Ring.Common.Overlap.zero x_1) = (x = x_1)
-- Mathlib.Data.DFinsupp.Multiset
Multiset.toDFinsupp_apply : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α) (a : α), (Multiset.toDFinsupp s) a = Multiset.count a s
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.Zoomed.match_1.eq_3 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → Sort u_2) (c : RBTree.RBColor) (l : RBTree.RBNode α) (x : α)
  (parent : RBTree.RBNode.Path α) (h_1 : Unit → motive RBTree.RBNode.Path.root)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) → (x : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent x r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (x : α) → (parent : RBTree.RBNode.Path α) → motive (RBTree.RBNode.Path.right c l x parent)),
  (match RBTree.RBNode.Path.right c l x parent with
    | RBTree.RBNode.Path.root => h_1 ()
    | RBTree.RBNode.Path.left c parent x r => h_2 c parent x r
    | RBTree.RBNode.Path.right c l x parent => h_3 c l x parent) =
    h_3 c l x parent
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.evaln.eq_4 : ∀ (k : ℕ),
  Nat.Partrec.Code.evaln k.succ Nat.Partrec.Code.left = fun n => do
    guard (n ≤ k)
    pure (Nat.unpair n).1
-- Mathlib.Analysis.Normed.Field.UnitBall
/-- Closed unit ball in a non-unital seminormed ring as a bundled `Subsemigroup`.  -/
Subsemigroup.unitClosedBall : (𝕜 : Type u_2) → [inst : NonUnitalSeminormedRing 𝕜] → Subsemigroup 𝕜
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Functor.mapArrowFunctor_map_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X Y : CategoryTheory.Functor C D} (τ : X ⟶ Y) (f : CategoryTheory.Arrow C),
  ((CategoryTheory.Functor.mapArrowFunctor C D).map τ).app f =
    CategoryTheory.Arrow.homMk (τ.app f.left) (τ.app f.right) ⋯
-- Mathlib.Order.Category.BddOrd
BddOrd.coe_id : ∀ {X : BddOrd}, ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id X)) = id
-- Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
CategoryTheory.SmallObject.SuccStruct.arrowSucc_extendToSucc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J]
  [inst_2 : SuccOrder J] {j : J} (hj : ¬IsMax j) (F : CategoryTheory.Functor (↑(Set.Iic j)) C) {X : C}
  (τ : F.obj ⟨j, ⋯⟩ ⟶ X),
  CategoryTheory.SmallObject.SuccStruct.arrowSucc (CategoryTheory.SmallObject.SuccStruct.extendToSucc hj F τ) j ⋯ =
    CategoryTheory.Arrow.mk τ
-- Init.Data.Int.Order
Int.le_add_one_iff : ∀ {m n : ℤ}, m ≤ n + 1 ↔ m ≤ n ∨ m = n + 1
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.nndist_coe_le_nndist : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β} (x : α), nndist (f x) (g x) ≤ nndist f g
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- A measurable set `t` such that `f =ᵐ[μ.restrict tᶜ] 0` and `sigma_finite (μ.restrict t)`.  -/
MeasureTheory.AEFinStronglyMeasurable.sigmaFiniteSet : {α : Type u_1} →
  {β : Type u_2} →
    {m : MeasurableSpace α} →
      {μ : MeasureTheory.Measure α} →
        [inst : TopologicalSpace β] →
          {f : α → β} → [inst_1 : Zero β] → [T2Space β] → MeasureTheory.AEFinStronglyMeasurable f μ → Set α
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.foldr.eq_1 : ∀ {α : Type u_1} {σ : Sort u_2} (f : α → σ → σ) (x : σ), RBTree.RBNode.foldr f RBTree.RBNode.nil x = x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Hom.monoid.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X : C} [inst_2 : CategoryTheory.MonObj M],
  CategoryTheory.Hom.monoid =
    {
      mul := fun f₁ f₂ =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
          CategoryTheory.MonObj.mul,
      mul_assoc := ⋯,
      one :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
          CategoryTheory.MonObj.one,
      one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- The equivalence between the abstract colimit of `F` in `TypeCat u`
and the "concrete" definition as a quotient.
 -/
CategoryTheory.Limits.Types.colimitEquivColimitType : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type u)) →
      [inst_1 : CategoryTheory.Limits.HasColimit F] → CategoryTheory.Limits.colimit F ≃ F.ColimitType
-- Init.Data.List.Zip
List.map_uncurry_zip_eq_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {l : List α} {l' : List β},
  List.map (Function.uncurry f) (l.zip l') = List.zipWith f l l'