mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Field.Basic
/-- A version of `inv_lt_zero` which holds with different assumptions. In particular, the type
must be a field, not just a `GroupWithZero`, but the order assumptions replace `LinearOrder` and
`PosMulMono` with `PartialOrder`, `IsStrictOrderedRing` and `PosMulReflectLT`. Thus neither version
is more general than the other. This one applies, for instance, to `ℂ`.  -/
inv_lt_zero' : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α},
  a⁻¹ < 0 ↔ a < 0
-- Mathlib.Algebra.Algebra.Bilinear
NonUnitalAlgHom.coe_lmul_eq_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A], ⇑(NonUnitalAlgHom.lmul R A) = ⇑(LinearMap.mul R A)
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The terms corresponding to the `⁅H, E⁆`-relations.  -/
CartanMatrix.Relations.HE : (R : Type u) → {B : Type v} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Subsemigroups of semigroup `M` are isomorphic to additive subsemigroups of `Additive M`.  -/
Subsemigroup.toAddSubsemigroup : {M : Type u_1} → [inst : Mul M] → Subsemigroup M ≃o AddSubsemigroup (Additive M)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal_map_hom_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.AddMon C} (f : X ⟶ Y) (x : CategoryTheory.Discrete PUnit.{w + 1}),
  ((CategoryTheory.AddMon.EquivLaxMonoidalFunctorPUnit.addMonToLaxMonoidal C).map f).hom.app x = f.hom
-- Init.Data.UInt.Lemmas
UInt16.toNat_mod_size : ∀ (n : UInt16), n.toNat % UInt16.size = n.toNat
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_mono_on₀ : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E] {μ : MeasureTheory.Measure X} {f g : X → E}
  {s : Set X} [ClosedIciTopology E],
  MeasureTheory.IntegrableOn f s μ →
    MeasureTheory.IntegrableOn g s μ →
      MeasureTheory.NullMeasurableSet s μ → (∀ x ∈ s, f x ≤ g x) → ∫ (x : X) in s, f x ∂μ ≤ ∫ (x : X) in s, g x ∂μ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {v : β k}, ⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inr_zero : ∀ (R : Type u) {M : Type v} [inst : Zero R] [inst_1 : Zero M], TrivSqZeroExt.inr 0 = 0
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
/-- Consider a real vector bundle in which each fiber is endowed with a scalar product.
We say that the bundle is Riemannian if the scalar product depends smoothly on the base point.
This assumption is spelled `IsContMDiffRiemannianBundle IB n F E` where `IB` is the model space of
the base, `n` is the smoothness, `F` is the model fiber, and `E : B → Type*` is the bundle.  -/
IsContMDiffRiemannianBundle : {EB : Type u_1} →
  [inst : NormedAddCommGroup EB] →
    [inst_1 : NormedSpace ℝ EB] →
      {HB : Type u_2} →
        [inst_2 : TopologicalSpace HB] →
          ModelWithCorners ℝ EB HB →
            WithTop ℕ∞ →
              {B : Type u_3} →
                [inst : TopologicalSpace B] →
                  [ChartedSpace HB B] →
                    (F : Type u_4) →
                      [inst_4 : NormedAddCommGroup F] →
                        [inst_5 : NormedSpace ℝ F] →
                          (E : B → Type u_5) →
                            [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)] →
                              [inst_7 : (x : B) → NormedAddCommGroup (E x)] →
                                [inst_8 : (x : B) → InnerProductSpace ℝ (E x)] →
                                  [inst_9 : FiberBundle F E] → [VectorBundle ℝ F E] → Prop
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.vonMangoldt_apply_one : ArithmeticFunction.vonMangoldt 1 = 0
-- Init.Data.SInt.Bitwise
Int8.neg_one_and : ∀ {a : Int8}, -1 &&& a = a
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_ne_top_iff : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α}, s.einfsep ≠ ⊤ ↔ s.Nontrivial
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.srange.congr_simp : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f f_1 : F),
  f = f_1 → NonUnitalRingHom.srange f = NonUnitalRingHom.srange f_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey? =
        some (t.minKey?.elim k fun k' => if compare k k' = Ordering.lt then k else k')
-- Mathlib.Data.Fin.Basic
/-- Converting the value of a `Fin n` to `Fin n` results in the same value.  -/
Fin.cast_val_eq_self : ∀ {n : ℕ} (a : Fin n), ↑↑a = a
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- The `FVarId` of the instance of concern within the current telescope.  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern.fvarId : Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern✝ → Lean.FVarId
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.mcasesPat.quot : Lean.ParserDescr
-- Mathlib.Order.LiminfLimsup
Filter.liminf_eq_iSup_iInf_of_nat : ∀ {α : Type u_1} [inst : CompleteLattice α] {u : ℕ → α}, Filter.liminf u Filter.atTop = ⨆ n, ⨅ i, ⨅ (_ : i ≥ n), u i
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instAddCommMonoid : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddCommMonoid R] → AddCommMonoid (HahnSeries Γ R)
-- Mathlib.Data.Set.Card
Set.ncard_sdiff_singleton_lt_of_mem : ∀ {α : Type u_1} {s : Set α} {a : α},
  a ∈ s → autoParam s.Finite Set.ncard_sdiff_singleton_lt_of_mem._auto_1 → (s \ {a}).ncard < s.ncard
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.Semiconj.mapsTo_periodicPts : ∀ {α : Type u_1} {β : Type u_2} {fa : α → α} {fb : β → β} {g : α → β},
  Function.Semiconj g fa fb → Set.MapsTo g (Function.periodicPts fa) (Function.periodicPts fb)
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.homologySequence_epi_shift_map_mor₁_iff : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological] [inst_9 : F.ShiftSequence ℤ],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ : ℤ), CategoryTheory.Epi ((F.shift n₀).map T.mor₁) ↔ (F.shift n₀).map T.mor₂ = 0
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.lhom_ext' : ∀ {R : Type u} [inst : Semiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f g : Polynomial R →ₗ[R] M}, (∀ (n : ℕ), f ∘ₗ Polynomial.monomial n = g ∘ₗ Polynomial.monomial n) → f = g
-- Batteries.Recycling.RBTree.Alter
/-- `path.RootOrdered cmp v` is true if `v` would be able to fit into the hole
without violating the ordering invariant.
 -/
RBTree.RBNode.Path.RootOrdered : {α : Type u_1} → (α → α → Ordering) → RBTree.RBNode.Path α → α → Prop
-- Mathlib.FieldTheory.PrimitiveElement
_private.Mathlib.FieldTheory.PrimitiveElement.0.Field.primitive_element_inf_aux_of_finite_intermediateField : ∀ (F : Type u_1) [inst : Field F] [Infinite F] {E : Type u_2} [inst_2 : Field E] (α β : E) [inst_3 : Algebra F E]
  [Finite (IntermediateField F E)], ∃ γ, F⟮α, β⟯ = F⟮γ⟯
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_insert : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  [inst_2 : TopologicalSpace α] {x : α} {s : Set α} {g : α → E'} {g' : α → F'},
  g x = 0 → (g =o[nhdsWithin x (insert x s)] g' ↔ g =o[nhdsWithin x s] g')
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_hom_associator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom.unop =
    (CategoryTheory.MonoidalCategoryStruct.associator (Opposite.unop X) (Opposite.unop Y) (Opposite.unop Z)).inv
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.mul.inj : ∀ {a b a_1 b_1 : Nat.Internal.SOM.Expr}, a.mul b = a_1.mul b_1 → a = a_1 ∧ b = b_1
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_norm_toLp : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] (f : α × β),
  ‖WithLp.toLp ⊤ f‖ = ‖f‖
-- Mathlib.GroupTheory.MonoidLocalization.Order
Localization.le : {α : Type u_1} →
  [inst : CommMonoid α] →
    [inst_1 : PartialOrder α] → [IsOrderedCancelMonoid α] → {s : Submonoid α} → LE (Localization s)
-- Mathlib.NumberTheory.ModularForms.Discriminant
_private.Mathlib.NumberTheory.ModularForms.Discriminant.0.CuspForm.termΔ : Lean.ParserDescr
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.a₁_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF], W.a₁ = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {k a : α}
  {h' : a ∈ t.erase k}, (t.erase k).get a h' = t.get a ⋯
-- Mathlib.Order.KrullDimension
Order.coe_lt_coheight_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α} {n : ℕ},
  Order.coheight x < ⊤ → (↑n < Order.coheight x ↔ ∃ y > x, Order.coheight y = ↑n)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
/-- `IsOverTower X Y S` is the typeclass asserting that the structure morphisms
`X ↘ Y`, `Y ↘ S`, and `X ↘ S` commute.  -/
CategoryTheory.IsOverTower : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X Y S : C) →
      [CategoryTheory.OverClass X S] → [CategoryTheory.OverClass Y S] → [CategoryTheory.OverClass X Y] → Prop
-- Mathlib.Topology.Order.Monotone
AntitoneOn.tendsto_nhdsGT : ∀ {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {x : α},
  AntitoneOn f (Set.Ioi x) →
    BddAbove (f '' Set.Ioi x) → Filter.Tendsto f (nhdsWithin x (Set.Ioi x)) (nhds (sSup (f '' Set.Ioi x)))
-- Init.Data.String.Search
/-- Checks whether a string has a match of the pattern `pat` anywhere.

This function is generic over all currently supported patterns.

Examples:

* `"coffee tea water".contains Char.isWhitespace = true`

* `"tea".contains (fun (c : Char) => c == 'X') = false`

* `"coffee tea water".contains "tea" = true`
 -/
String.any : {ρ : Type} →
  {σ : String.Slice → Type} →
    [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)] →
      [(s : String.Slice) → Std.IteratorLoop (σ s) Id Id] →
        String → (pat : ρ) → [String.Slice.Pattern.ToForwardSearcher pat σ] → Bool
-- Mathlib.Topology.NhdsWithin
preimage_coe_mem_nhds_subtype : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α} {a : ↑s}, Subtype.val ⁻¹' t ∈ nhds a ↔ t ∈ nhdsWithin (↑a) s
-- Lean.DocString.Markdown
Lean.Doc.instToMarkdownInlineOfMarkdownInline : {i : Type u_1} → [Lean.Doc.MarkdownInline i] → Lean.Doc.ToMarkdown (Lean.Doc.Inline i)
-- Mathlib.Algebra.Tropical.Basic
Tropical.trop_top : ∀ {R : Type u} [inst : Top R], Tropical.trop ⊤ = 0
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- The map between affine spaces over affine bases is
isomorphic to the natural map between polynomial rings.  -/
AlgebraicGeometry.AffineSpace.mapSpecMap : {n : Type u} →
  {R S : CommRingCat} →
    (φ : R ⟶ S) →
      CategoryTheory.Arrow.mk (AlgebraicGeometry.AffineSpace.map n (AlgebraicGeometry.Spec.map φ)) ≅
        CategoryTheory.Arrow.mk
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.equivLike_neg_eq_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (f : α ≃+o β), EquivLike.inv f = ⇑f.symm
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.instInhabited : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → Inhabited (AddMonoidAlgebra R M)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.toLpCLM_apply : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E]
  [inst_5 : OpensMeasurableSpace E] [inst_6 : NormedField 𝕜] [inst_7 : NormedSpace 𝕜 F] [inst_8 : SMulCommClass ℝ 𝕜 F]
  [inst_9 : SecondCountableTopologyEither E F] {p : ENNReal} [inst_10 : Fact (1 ≤ p)] {μ : MeasureTheory.Measure E}
  [hμ : μ.HasTemperateGrowth] {f : SchwartzMap E F}, (SchwartzMap.toLpCLM 𝕜 F p μ) f = f.toLp p μ
-- Mathlib.RingTheory.Extension.Presentation.Core
Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul : ∀ {R : Type u_1} {S : Type u_2} {ι : Type u_3} {σ : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {P : Algebra.Presentation R S ι σ} (R₀ : Type u_5) [inst_3 : CommRing R₀]
  [inst_4 : Algebra R₀ R] [inst_5 : Algebra R₀ S] [inst_6 : IsScalarTower R₀ R S] [inst_7 : P.HasCoeffs R₀] (x : R)
  (y : MvPolynomial ι R₀),
  (P.tensorModelOfHasCoeffsHom R₀)
      (x ⊗ₜ[R₀] (Ideal.Quotient.mk (Ideal.span (Set.range (Algebra.Presentation.relationOfHasCoeffs R₀)))) y) =
    (algebraMap R S) x * (MvPolynomial.aeval P.val) y
-- Mathlib.CategoryTheory.Sites.Adjunction
CategoryTheory.Sheaf.instIsRightAdjointSheafComposeOfHasWeakSheafify : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E]
  {F : CategoryTheory.Functor D E} [CategoryTheory.HasWeakSheafify J D] [inst_4 : F.IsRightAdjoint],
  (CategoryTheory.sheafCompose J F).IsRightAdjoint
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.projectMapAux.eq_10 : ∀ {C : Type u} {D : Type u'} [inst : CategoryTheory.Category.{v', u'} D] [inst_1 : CategoryTheory.MonoidalCategory D]
  (f : C → D) (X₁ X₂ : CategoryTheory.FreeMonoidalCategory C) (p : X₁.Hom X₂)
  (X : CategoryTheory.FreeMonoidalCategory C),
  CategoryTheory.FreeMonoidalCategory.projectMapAux f (p.whiskerRight X) =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.FreeMonoidalCategory.projectMapAux f p)
      (CategoryTheory.FreeMonoidalCategory.projectObj f X)
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] [inst_3 : CategoryTheory.BraidedCategory D],
  (CategoryTheory.Monoidal.commMonFunctorCategoryEquivalence C D).functor =
    CategoryTheory.Monoidal.CommMonFunctorCategoryEquivalence.functor
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.transportIso.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  (x : CategoryTheory.Grothendieck F) {c : C} (α : x.base ≅ c),
  x.transportIso α =
    (CategoryTheory.Grothendieck.isoMk α (CategoryTheory.Iso.refl ((F.map α.hom).toFunctor.obj x.fiber))).symm
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instInhabitedΓ' : Inhabited Turing.PartrecToTM2.Γ'
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.cross_mk_of_cross_eq_zero : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0),
  (crossProduct v) w = 0 → (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F v hv
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forgetToTop_comp_forget : AlgebraicGeometry.Scheme.forgetToTop.comp (CategoryTheory.forget TopCat) = AlgebraicGeometry.Scheme.forget
-- Init.Data.UInt.Bitwise
UInt32.ofNat_and : ∀ (a b : ℕ), UInt32.ofNat (a &&& b) = UInt32.ofNat a &&& UInt32.ofNat b
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instIsPartialOrder : ∀ {n : ℕ}, Std.IsPartialOrder (BitVec n)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.Nonempty.sub : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, s.Nonempty → t.Nonempty → (s - t).Nonempty
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
/-- The second-lowest coefficient, or 0 for constants  -/
Polynomial.nextCoeffUp : {R : Type u} → [inst : Semiring R] → Polynomial R → R
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sup_left : ∀ {G : Type u_1} [inst : AddGroup G] {S T : AddSubgroup G} {x : G}, x ∈ S → x ∈ S ⊔ T
-- Mathlib.Topology.FiberPartition
TopologicalSpace.Fiber.sigmaIsoHom_apply : ∀ {S : Type u_1} {Y : Type u_2} (f : S → Y) [inst : TopologicalSpace S] (x : (x : Function.Fiber f) × ↑↑x),
  (TopologicalSpace.Fiber.sigmaIsoHom f) x =
    match x with
    | ⟨a, x⟩ => ↑x
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
Matrix.IsIrreducible.mk : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R},
  (∀ (i j : n), 0 ≤ A i j) → Quiver.IsSStronglyConnected n → A.IsIrreducible
-- Mathlib.Algebra.Order.Pi
Function.const_lt_one : ∀ {α : Type u_2} {β : Type u_3} [inst : One α] [inst_1 : Preorder α] {a : α} [Nonempty β],
  Function.const β a < 1 ↔ a < 1
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.isZero_H_map_mk₁_of_isIso : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) (n : ℤ) {i₀ i₁ : ι} (f : i₀ ⟶ i₁) [CategoryTheory.IsIso f],
  CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f))
-- Init.Data.Order.Ord
Nat.instTransOrd : Std.TransOrd ℕ
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.symm_bijective : ∀ {X Y : TopPair} {f₀ f₁ : X ⟶ Y}, Function.Bijective TopPair.Homotopy.symm
-- Mathlib.Algebra.Order.Ring.Abs
abs_sub_sq : ∀ {α : Type u_1} [inst : CommRing α] [inst_1 : LinearOrder α] (a b : α),
  |a - b| * |a - b| = a * a + b * b - (1 + 1) * a * b
-- Init.Data.UInt.Lemmas
UInt32.add_mul : ∀ {a b c : UInt32}, (a + b) * c = a * c + b * c
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- Assuming `G : C` is a generator, `X : C`, and `A : Subobject X`,
this is a subobject of `X` which is `⊤` if `A = ⊤`, and otherwise
it is a larger subobject given by the lemma `exists_larger_subobject`.
The inclusion of `A` in `largerSubobject hG A` is a pushout of
a monomorphism in the family `generatingMonomorphisms G`
(see `pushouts_ofLE_le_largerSubobject`).  -/
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms.largerSubobject : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : C} →
      [CategoryTheory.Abelian C] →
        CategoryTheory.IsSeparator G → {X : C} → CategoryTheory.Subobject X → CategoryTheory.Subobject X
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toList_toArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β}, m.toArray.toList = m.toList
-- Init.Data.Option.Lemmas
Option.not_comp_isNone : ∀ {α : Type u_1}, (fun x => !x) ∘ Option.isNone = Option.isSome
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.primeSpectrumOrderIsoSpec_symm_apply : ∀ (R : Type u) [inst : CommRing R] (x : (↥(AlgebraicGeometry.Spec (CommRingCat.of R)))ᵒᵈ),
  (RelIso.symm (AlgebraicGeometry.primeSpectrumOrderIsoSpec R)) x = OrderDual.ofDual x
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hasSum_int_sinKernel : ∀ (a : ℝ) {t : ℝ},
  0 < t →
    HasSum
      (fun n =>
        -Complex.I * ↑n * Complex.exp (2 * ↑Real.pi * Complex.I * ↑a * ↑n) * ↑(Real.exp (-Real.pi * ↑n ^ 2 * t)))
      ↑(HurwitzZeta.sinKernel (↑a) t)
-- Lean.ToLevel
Lean.instToLevel_1 : [Lean.ToLevel] → Lean.ToLevel
-- Mathlib.GroupTheory.Nilpotent
Group.nilpotencyClass_zero_iff_subsingleton : ∀ {G : Type u_1} [inst : Group G] [Group.IsNilpotent G], Group.nilpotencyClass G = 0 ↔ Subsingleton G
-- Lean.Util.HasConstCache
Lean.HasConstCache : Array Lean.Name → Type
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.mul_iff_right : ∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : CommGroup G]
  [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure α} {f g : α → G},
  AEMeasurable f μ → (AEMeasurable (f * g) μ ↔ AEMeasurable g μ)
-- Mathlib.Order.Category.BddOrd
/-- The type of morphisms in `BddOrd R`.  -/
BddOrd.Hom : BddOrd → BddOrd → Type u
-- Mathlib.Data.Option.Basic
Option.getD_comp_some : ∀ {α : Type u_1} (d : α), (fun x => x.getD d) ∘ some = id
-- Mathlib.Order.Antisymmetrization
le_of_le_of_antisymmRel : ∀ {α : Type u_1} {a b c : α} [inst : Preorder α], a ≤ b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → a ≤ c
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.isZero_normalizedChainComplex_X_of_hasDimensionLT : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C) (n d : ℕ) [X.HasDimensionLT d],
  autoParam (d ≤ n) SSet.isZero_normalizedChainComplex_X_of_hasDimensionLT._auto_1 →
    CategoryTheory.Limits.IsZero ((X.normalizedChainComplex R).X n)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eq_none : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = false → Std.Internal.List.getKey? a l = none
-- Mathlib.Algebra.Group.Ext
DivInvMonoid.ext_iff : ∀ {M : Type u_1} {m₁ m₂ : DivInvMonoid M}, m₁ = m₂ ↔ HMul.hMul = HMul.hMul ∧ Inv.inv = Inv.inv
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Indep.insert_dep_iff : ∀ {α : Type u_2} {M : Matroid α} {e : α} {I : Set α}, M.Indep I → (M.Dep (insert e I) ↔ e ∈ M.closure I \ I)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertMany_empty_list_nil : ∀ {α : Type u} {instOrd : Ord α} {β : Type v},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty [] ⋯) =
    Std.DTreeMap.Internal.Impl.empty
-- Init.Data.Bool
/-- De Morgan's law for boolean or  -/
Bool.not_or : ∀ (x y : Bool), (!(x || y)) = (!x && !y)
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
/-- The orthogonal complement of the closure of a submodule (as a `ClosedSubmodule`) is equal to
the closure of the orthogonal complement.  -/
ClosedSubmodule.orthogonal_closure'' : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), K.closureᗮ = Kᗮ.closure
-- Lean.Meta.Tactic.Replace
/-- Replace the target type of `mvarId` with `typeNew`.
If `checkDefEq = false`, this method assumes that `typeNew` is definitionally equal to the current target type.
If `checkDefEq = true`, throw an error if `typeNew` is not definitionally equal to the current target type.
 -/
Lean.MVarId.change : Lean.MVarId → Lean.Expr → optParam Bool true → Lean.MetaM Lean.MVarId
-- Mathlib.GroupTheory.GroupAction.Period
AddAction.period_zero : ∀ {α : Type v} (M : Type u) [inst : AddMonoid M] [inst_1 : AddAction M α] (a : α), AddAction.period 0 a = 1