mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.inlX_mapHomologicalComplexObjXIso_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] (i j : ι) (hij : c.Rel j i)
  {Z : D} (h : H.obj ((HomologicalComplex.homotopyCofiber φ).X j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.homotopyCofiber.inlX ((H.mapHomologicalComplex c).map φ) i j hij)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso φ H j).inv
        h) =
    CategoryTheory.CategoryStruct.comp (H.map (HomologicalComplex.homotopyCofiber.inlX φ i j hij)) h
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.mk_eta : ∀ {R : Type u_1} {a b : R} (z : QuadraticAlgebra R a b), { re := z.re, im := z.im } = z
-- Batteries.Recycling.RBTree.Basic
/-- An "iterator" over the keys of the map. This is a trivial wrapper over the underlying map,
but it comes with a small API to use it in a `for` loop or convert it to an array or list.
 -/
RBTree.RBMap.Keys : (α : Type u_1) → Type u_2 → (α → α → Ordering) → Type (max u_1 u_2)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.IsOrtho.all : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (x y : M), QuadraticMap.IsOrtho 0 x y
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.atIdx!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {i : ℕ},
  t₁.Equiv t₂ → t₁.atIdx! i = t₂.atIdx! i
-- Mathlib.Data.PNat.Factors
/-- If a `List ℕ+` consists only of primes, it can be recast as a `PrimeMultiset` with
the coercion from lists to multisets.  -/
PrimeMultiset.ofPNatList : (l : List ℕ+) → (∀ p ∈ l, p.Prime) → PrimeMultiset
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.EssImageSubcategory.associator_hom_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Full] [inst_5 : F.Faithful]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteProducts F] (X Y Z : F.EssImageSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).hom
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots_eval₂_eq_zero : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : CommSemiring R] {p : Polynomial S} (f : S →+* R) {r : R}
  {s : S}, Polynomial.eval₂ f r p = 0 → Polynomial.eval₂ f (f s * r) (p.scaleRoots s) = 0
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonFunctor_map_app_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (D : Type u₂)
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {X Y : CategoryTheory.LaxMonoidalFunctor C D} (α : X ⟶ Y) (A : CategoryTheory.AddMon C),
  (((CategoryTheory.Functor.mapAddMonFunctor C D).map α).app A).hom = α.hom.app A.X
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_lt_mul_of_lt_of_le_of_nonneg_of_pos`. -/
mul_lt_mul_of_nonneg_of_pos : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α]
  [MulPosStrictMono α], a < b → c ≤ d → 0 ≤ a → 0 < d → a * c < b * d
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instReflectsColimitWalkingParallelPairParallelPairOfIsSplitPairOfReflectsColimitOfIsSplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {A B : D} (f g : A ⟶ B) [G.IsSplitPair f g]
  [CategoryTheory.Monad.ReflectsColimitOfIsSplitPair G],
  CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.parallelPair f g) G
-- Mathlib.Order.PFilter
Order.PFilter.mk.inj : ∀ {P : Type u_1} {inst : Preorder P} {dual dual_1 : Order.Ideal Pᵒᵈ},
  { dual := dual } = { dual := dual_1 } → dual = dual_1
-- Mathlib.Order.Filter.Pointwise
Filter.mul.instNeBot : ∀ {α : Type u_2} [inst : Mul α] {f g : Filter α} [f.NeBot] [g.NeBot], (f * g).NeBot
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A morphism `ι` satisfying `ι ≫ f = 0` determines a kernel fork over `f`.  -/
CategoryTheory.Limits.KernelFork.ofι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {Z : C} → (ι : Z ⟶ X) → CategoryTheory.CategoryStruct.comp ι f = 0 → CategoryTheory.Limits.KernelFork f
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_zero : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.U R 0 = 1
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.dominatedFinMeasAdditive_cbmApplyMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G),
  MeasureTheory.DominatedFinMeasAdditive μ.variation ⇑(μ.transpose B) ‖B‖
-- Mathlib.Topology.UniformSpace.Cauchy
totallyBounded_iff_filter : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : Set α},
  TotallyBounded s ↔ ∀ (f : Filter α), f.NeBot → f ≤ Filter.principal s → ∃ c ≤ f, Cauchy c
-- Lean.Data.Json.Basic
Lean.Json.getStr? : Lean.Json → Except String String
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.Splitting.mk.inj : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} {inst : Group N} {inst_1 : Group E} {inst_2 : Group G}
  {S : GroupExtension N E G} {toMonoidHom : G →* E}
  {rightInverse_rightHom : Function.RightInverse (↑toMonoidHom).toFun ⇑S.rightHom} {toMonoidHom_1 : G →* E}
  {rightInverse_rightHom_1 : Function.RightInverse (↑toMonoidHom_1).toFun ⇑S.rightHom},
  { toMonoidHom := toMonoidHom, rightInverse_rightHom := rightInverse_rightHom } =
      { toMonoidHom := toMonoidHom_1, rightInverse_rightHom := rightInverse_rightHom_1 } →
    toMonoidHom = toMonoidHom_1
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.mul_mod : ∀ (x y : Ordinal.{u_4}), x * y % x = 0
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₂.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} {X : C}
  (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) {Y : C} (f : X ⟶ Y)
  (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y),
  CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p =
    CategoryTheory.OverPresheafAux.YonedaCollection.mk
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) p.fst)
      ((CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CostructuredArrow.mkPrecomp p.fst f).op)) p.snd)
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.Iic_coe : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Set.Iic ↑a = WithTop.some '' Set.Iic a
-- Mathlib.Algebra.Order.UpperLower
UpperSet.coe_add : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α] (s t : UpperSet α),
  ↑(s + t) = ↑s + ↑t
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.cast : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {len : ℕ} → {aig1 aig2 : Std.Sat.AIG α} → aig1.RefVec len → aig1.decls.size ≤ aig2.decls.size → aig2.RefVec len
-- Mathlib.Data.List.Destutter
List.destutter'_of_isChain_cons : ∀ {α : Type u_1} (l : List α) (R : α → α → Prop) [inst : DecidableRel R] {a : α},
  List.IsChain R (a :: l) → List.destutter' R a l = a :: l
-- Mathlib.RingTheory.PowerSeries.Derivative
/-- The `k`-th coefficient of the `n`-th formal derivative: differentiating `n` times multiplies the
`(k + n)`-th coefficient by the ascending factorial `(k + 1)(k + 2) ⋯ (k + n)`.  -/
PowerSeries.coeff_iterate_derivative : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (n k : ℕ),
  (PowerSeries.coeff k) ((⇑(PowerSeries.derivative R))^[n] f) =
    ↑((k + 1).ascFactorial n) * (PowerSeries.coeff (k + n)) f
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The constant map is multilinear when `ι` is empty.  -/
MultilinearMap.constOfIsEmpty : (R : Type uR) →
  {ι : Type uι} →
    (M₁ : ι → Type v₁) →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] → [inst_4 : Module R M₂] → [IsEmpty ι] → M₂ → MultilinearMap R M₁ M₂
-- Mathlib.Topology.UniformSpace.Separation
Filter.HasBasis.specializes_iff_uniformity : ∀ {α : Type u} [inst : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → Set (α × α)},
  (uniformity α).HasBasis p s → ∀ {x y : α}, x ⤳ y ↔ ∀ (i : ι), p i → (x, y) ∈ s i
-- Init.Data.SInt.Lemmas
instCommutativeInt16HAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.circulant_single : ∀ {α : Type u_1} (n : Type u_5) [inst : Semiring α] [inst_1 : DecidableEq n] [inst_2 : AddGroup n] [inst_3 : Fintype n]
  (a : α), Matrix.circulant (Pi.single 0 a) = (Matrix.scalar n) a
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.mk_map : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ x₁ : X} (P₀ : Path x₀ x₁)
  (f : C(X, Y)), Path.Homotopic.Quotient.mk (P₀.map ⋯) = (Path.Homotopic.Quotient.mk P₀).map f
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_atTop_atBot_iff_of_antitone : ∀ {α : Type u_3} {β : Type u_4} [Nonempty α] [inst : Preorder α] [IsDirectedOrder α] {f : α → β} [inst_2 : Preorder β],
  Antitone f → (Filter.Tendsto f Filter.atTop Filter.atBot ↔ ∀ (b : β), ∃ a, f a ≤ b)
-- Mathlib.Order.Interval.Finset.Gaps
/-- The second coordinate of `F.intervalGapsWithin h a b i` is `b` if `i = k`,
`x i` otherwise.  -/
Finset.intervalGapsWithin.snd : {α : Type u_1} → [LinearOrder α] → (F : Finset (α × α)) → {k : ℕ} → F.card = k → α → Fin (k + 1) → α
-- Mathlib.Data.List.Perm.Lattice
List.Perm.bagInter_left : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α) {t₁ t₂ : List α}, t₁.Perm t₂ → l.bagInter t₁ = l.bagInter t₂
-- Mathlib.Control.Bifunctor
Function.bicompl.lawfulBifunctor : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] (G : Type u_1 → Type u₀) (H : Type u_2 → Type u₁)
  [inst_1 : Functor G] [inst_2 : Functor H] [LawfulFunctor G] [LawfulFunctor H] [LawfulBifunctor F],
  LawfulBifunctor (Function.bicompl F G H)
-- Mathlib.Algebra.Ring.Center
Set.intCast_mem_center : ∀ (M : Type u_1) [inst : NonAssocRing M] (n : ℤ), ↑n ∈ Set.center M
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The ideal corresponding to a coarsening of a valuation ring.  -/
ValuationSubring.idealOfLE : {K : Type u} → [inst : Field K] → (R S : ValuationSubring K) → R ≤ S → Ideal ↥R
-- Mathlib.Order.CompleteLattice.Basic
iInf_of_empty : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [IsEmpty ι] (f : ι → α), iInf f = ⊤
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RooSliceData.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : SizeOf β]
  (treeMap : Std.DTreeMap.Internal.Impl α fun x => β) (range : Std.Roo α),
  sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Init.Data.Nat.Fold
Nat.foldRev_eq_finRange_foldr : ∀ {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n → α → α) (init : α),
  n.foldRev f init =
    List.foldr
      (fun x acc =>
        match x with
        | ⟨i, h⟩ => f i h acc)
      init (List.finRange n)
-- Init.Internal.Order.Basic
Lean.Order.inf : {α : Sort u} → [Lean.Order.CompleteLattice α] → (α → Prop) → α
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.mk.injEq : ∀ {G : Type u_6} [inst : AddGroup G] (toFun : G → ℝ) (map_zero' : toFun 0 = 0)
  (add_le' : ∀ (r s : G), toFun (r + s) ≤ toFun r + toFun s) (neg' : ∀ (r : G), toFun (-r) = toFun r) (toFun_1 : G → ℝ)
  (map_zero'_1 : toFun_1 0 = 0) (add_le'_1 : ∀ (r s : G), toFun_1 (r + s) ≤ toFun_1 r + toFun_1 s)
  (neg'_1 : ∀ (r : G), toFun_1 (-r) = toFun_1 r),
  ({ toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' } =
      { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 }) =
    (toFun = toFun_1)
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiffAt_comp_diffeomorph_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n m : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : N → M'} {x : M},
  m ≤ n → (ContMDiffAt I I' m (f ∘ ⇑h) x ↔ ContMDiffAt J I' m f (h x))
-- Std.Time.Time.PlainTime
Std.Time.PlainTime.instHAddOffset_2 : HAdd Std.Time.PlainTime Std.Time.Second.Offset Std.Time.PlainTime
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.map_X : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (s : σ),
  (MvPowerSeries.map f) (MvPowerSeries.X s) = MvPowerSeries.X s
-- Mathlib.Data.Multiset.AddSub
/-- **Alias** of the reverse direction of `Multiset.add_le_add_iff_left`. -/
Multiset.add_le_add_left : ∀ {α : Type u_1} {s t u : Multiset α}, t ≤ u → s + t ≤ s + u
-- Mathlib.Order.Interval.Finset.Basic
Finset.card_Ioo_eq_card_Ioc_sub_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : LocallyFiniteOrder α] (a b : α),
  (Finset.Ioo a b).card = (Finset.Ioc a b).card - 1
-- Mathlib.Order.Shrink
instPartialOrderShrink : {α : Type u_1} → [inst : Small.{u, u_1} α] → [PartialOrder α] → PartialOrder (Shrink.{u, u_1} α)
-- Mathlib.Topology.Algebra.Algebra
Algebra.elemental.self_mem : ∀ (R : Type u_1) [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] (x : A), x ∈ Algebra.elemental R x
-- Std.Internal.Do.Order.Basic
/-- Supremum for Prop: true iff some element of the set is true  -/
Lean.Order.propSup : (Prop → Prop) → Prop
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIdsM.Context.mk.sizeOf_spec : ∀ (commonMCtx? : Option Lean.MetavarContext) (mctx₁ mctx₂ : Lean.MetavarContext) (allowAssignmentDiff : Bool),
  sizeOf { commonMCtx? := commonMCtx?, mctx₁ := mctx₁, mctx₂ := mctx₂, allowAssignmentDiff := allowAssignmentDiff } =
    1 + sizeOf commonMCtx? + sizeOf mctx₁ + sizeOf mctx₂ + sizeOf allowAssignmentDiff
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyMeasure_zero_scale : ∀ (x₀ : ℝ), ProbabilityTheory.cauchyMeasure x₀ 0 = MeasureTheory.Measure.dirac x₀
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_const_smul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x}
  {c : 𝕜} [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt[s] (T% W) x →
    UniqueMDiffAt[s] x → VectorField.mlieBracketWithin I V (c • W) s x = c • VectorField.mlieBracketWithin I V W s x
-- Mathlib.Data.Fintype.BigOperators
/-- The number of strings of length `s` in any finite set is at most `D^s`.  -/
Finset.card_filter_length_eq_le : ∀ {α : Type u_1} [inst : Fintype α] {T : Finset (List α)} {s : ℕ}, {x ∈ T | x.length = s}.card ≤ Fintype.card α ^ s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.Point.toAffineLift_neg : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} (P : W.Point), (-P).toAffineLift = -P.toAffineLift
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  m.WF → Std.HashMap.Raw.forIn (fun a x d => f a d) init m = forIn m.keysArray init f
-- Mathlib.Topology.Algebra.Algebra
Algebra.elemental.le_of_mem : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : IsSemitopologicalSemiring A] {x : A} {s : Subalgebra R A},
  IsClosed ↑s → x ∈ s → Algebra.elemental R x ≤ s
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.eval_apply_apply : ∀ {M : Type uM} {N : Type uN} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N] (y : M) (x : M →+ N),
  (AddMonoidHom.eval y) x = x y
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitBall.instIsLeftCancelMulZero : ∀ {𝕜 : Type u_1} [inst : NonUnitalSeminormedRing 𝕜] [IsLeftCancelMulZero 𝕜], IsLeftCancelMulZero ↑(Metric.ball 0 1)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V),
  I.glueDataObjMap h =
    AlgebraicGeometry.Spec.map
      (CommRingCat.ofHom
        (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) ⋯))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α} {v : β k},
  (t.insert k v).maxKey! = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.RingTheory.Artinian.Ring
IsArtinianRing.localization_artinian : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R] (S : Submonoid R) (L : Type u_2) [inst_2 : CommSemiring L]
  [inst_3 : Algebra R L] [IsLocalization S L], IsArtinianRing L
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects limits of `K.leftOp : Jᵒᵖ ⥤ C`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects
colimits of `K : J ⥤ Cᵒᵖ`.  -/
CategoryTheory.Limits.reflectsColimit_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J Cᵒᵖ)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.ReflectsLimit K.leftOp F],
  CategoryTheory.Limits.ReflectsColimit K F.op
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.left_neg_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  (X : C) [self : CategoryTheory.AddGrpObj X] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.AddGrpObj.neg (CategoryTheory.CategoryStruct.id X))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero h)
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.dual_isBase_iff : ∀ {α : Type u_1} {M : Matroid α} {B : Set α},
  autoParam (B ⊆ M.E) Matroid.dual_isBase_iff._auto_1 → (M✶.IsBase B ↔ M.IsBase (M.E \ B))
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.pullback_map_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] (g : CategoryTheory.Over Y) {h : CategoryTheory.Over Y}
  {k : g ⟶ h},
  ((CategoryTheory.Over.pullback f).map k).left =
    CategoryTheory.Limits.pullback.lift
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g.hom f) (CategoryTheory.Over.Hom.left k))
      (CategoryTheory.Limits.pullback.snd g.hom f) ⋯
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom_naturality_left_symm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  {𝒢 : CategoryTheory.Functor Dᵒᵖ A} (f : 𝒢 ⟶ ℱ) (g : ℱ ⟶ ℱ'.obj) {Z : CategoryTheory.Functor Cᵒᵖ A}
  (h : G.op.comp ℱ'.obj ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.symm (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (G.op.whiskerLeft f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCoverDense.restrictHomEquivHom.symm g) h)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_natCast : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (n : ℕ), (↑n).toCLM = ↑n
-- Mathlib.Data.EReal.Operations
EReal.neg_eq_zero_iff : ∀ {x : EReal}, -x = 0 ↔ x = 0
-- Init.Data.List.Lemmas
List.getLast!_nil : ∀ {α : Type u_1} [inst : Inhabited α], [].getLast! = default
-- Mathlib.Algebra.Group.Hom.Defs
/-- Makes a group homomorphism from a proof that the map preserves multiplication.  -/
MonoidHom.mk' : {M : Type u_4} →
  {G : Type u_7} →
    [inst : Group G] → [inst_1 : MulOneClass M] → (f : M → G) → (∀ (a b : M), f (a * b) = f a * f b) → M →* G
-- Mathlib.Topology.Sheaves.CommRingCat
/-- The map into the localization presheaf.  -/
TopCat.Presheaf.SubmonoidPresheaf.toLocalizationPresheaf : {X : TopCat} → {F : TopCat.Presheaf CommRingCat X} → (G : F.SubmonoidPresheaf) → F ⟶ G.localizationPresheaf
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_pow_subset : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : Monoid β] [inst_2 : FunLike F α β]
  [MonoidHomClass F α β] (f : F) (s : Set β) (n : ℕ), (⇑f ⁻¹' s) ^ n ⊆ ⇑f ⁻¹' s ^ n
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_alter_eq_add_one : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {f : Option (β k) → Option (β k)},
      m.contains k = false → (f (m.get? k)).isSome = true → (↑(m.alter k f)).size = (↑m).size + 1
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.apply_symm_apply : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (e : P ≃ᵃⁱ[𝕜] P₂) (x : P₂), e (e.symm x) = x