mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderCobaseChange.respectsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderCobaseChange], P.RespectsIso
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.pentagon : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} E]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor B C) (H : CategoryTheory.Functor C D)
  (K : CategoryTheory.Functor D E),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (F.associator G H).hom K)
      (CategoryTheory.CategoryStruct.comp (F.associator (G.comp H) K).hom (F.whiskerLeft (G.associator H K).hom)) =
    CategoryTheory.CategoryStruct.comp ((F.comp G).associator H K).hom (F.associator G (H.comp K)).hom
-- Init.Data.UInt.Lemmas
UInt8.ofNat_one : UInt8.ofNat 1 = 1
-- Mathlib.RingTheory.PicardGroup
/-- The Picard group of a semilocal ring is trivial.  -/
CommRing.Pic.instSubsingletonOfFiniteMaximalSpectrum : ∀ (R : Type u_5) [inst : CommRing R] [Finite (MaximalSpectrum R)], Subsingleton (CommRing.Pic R)
-- Mathlib.Algebra.Free
FreeAddMagma.traverse_add' : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β),
  Function.comp (traverse F) ∘ HAdd.hAdd = fun x y => (fun x1 x2 => x1 + x2) <$> traverse F x <*> traverse F y
-- Mathlib.Order.Closure
ClosureOperator.ofCompletePred_isClosed : ∀ {α : Type u_1} [inst : CompleteLattice α] (p : α → Prop) (hsinf : ∀ (s : Set α), (∀ a ∈ s, p a) → p (sInf s)) (a : α),
  (ClosureOperator.ofCompletePred p hsinf).IsClosed a = p a
-- Mathlib.Topology.Homotopy.HSpaces
HSpace.hmulE : {X : Type u} →
  {inst : TopologicalSpace X} →
    [self : HSpace X] →
      (HSpace.hmul.comp ((ContinuousMap.id X).prodMk (ContinuousMap.const X HSpace.e))).HomotopyRel (ContinuousMap.id X)
        {HSpace.e}
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mk : {α : Type u_4} → [inst : TopologicalSpace α] → (carrier : Set α) → IsClosed carrier → TopologicalSpace.Closeds α
-- Mathlib.Algebra.Lie.Derivation.Killing
/-- The range of the adjoint action on a finite-dimensional Killing Lie algebra is full.  -/
LieDerivation.IsKilling.range_ad_eq_top : ∀ (R : Type u_1) (L : Type u_2) [inst : Field R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Module.Finite R L]
  [LieAlgebra.IsKilling R L], (LieDerivation.ad R L).range = ⊤
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.HasShift C ℤ}
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} {x y : CategoryTheory.Pretriangulated.TriangleMorphism T₁ T₂},
  x = y ↔ x.hom₁ = y.hom₁ ∧ x.hom₂ = y.hom₂ ∧ x.hom₃ = y.hom₃
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.sndKernelFork_ι : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} (c : CategoryTheory.Limits.BinaryBicone X Y), CategoryTheory.Limits.Fork.ι c.sndKernelFork = c.inl
-- Mathlib.Topology.MetricSpace.Contracting
/-- Let `x` be a point of a complete emetric space. Suppose that `f` is a contracting map,
and `edist x (f x) ≠ ∞`. Then `efixedPoint` is the unique fixed point of `f`
in `Metric.eball x ∞`.  -/
ContractingWith.efixedPoint : {α : Type u_1} →
  [inst : EMetricSpace α] →
    {K : NNReal} → (f : α → α) → [CompleteSpace α] → ContractingWith K f → (x : α) → edist x (f x) ≠ ⊤ → α
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- Uniform convergence on a singleton is equivalent to regular convergence  -/
tendstoUniformlyOn_singleton_iff_tendsto : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {f : α → β} {x : α}
  {p : Filter ι}, TendstoUniformlyOn F f p {x} ↔ Filter.Tendsto (fun n => F n x) p (nhds (f x))
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toEnd_apply : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (φ : A →ₐ[R] A),
  AlgHom.toEnd φ = φ.toLinearMap
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.restr_target : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t),
  h.restr.target = e.target ∩ t
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Fmla.subsumes.mk : ∀ {f f' : Sat.Fmla}, (∀ x ∈ f', x ∈ f) → f.subsumes f'
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.toSpecΓ_SpecMap_ΓSpecIso_inv : ∀ (R : CommRingCat),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec R).toSpecΓ
      (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.ΓSpecIso R).inv) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.starGraph_center_adj' : ∀ {V : Type u_1} {r v : V}, r ≠ v → (SimpleGraph.starGraph r).Adj v r
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.compContinuousCLM_apply : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] {𝕜 : Type u_2}
  [inst_2 : TopologicalSpace γ] [inst_3 : NormedField 𝕜] [inst_4 : NormedSpace 𝕜 β] (f : BoundedContinuousFunction α β)
  (g : C(γ, α)), (BoundedContinuousFunction.compContinuousCLM β 𝕜 g) f = f.compContinuous g
-- Mathlib.Analysis.Distribution.Sobolev
FourierTransform.fourierCLM.congr_simp : ∀ (R : Type u_2) (E : Type u_3) {F : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : TopologicalSpace E] [inst_9 : TopologicalSpace F]
  [inst_10 : ContinuousFourier E F], FourierTransform.fourierCLM R E = FourierTransform.fourierCLM R E
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.typein_apply : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  (f : InitialSeg r s) (a : α), (Ordinal.typein s).toRelEmbedding (f a) = (Ordinal.typein r).toRelEmbedding a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.toList_inj : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  t₁.toList = t₂.toList ↔ t₁ = t₂
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.laxBraided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (self : CategoryTheory.LaxBraidedFunctor C D) → self.LaxBraided
-- Std.Data.Internal.List.Associative
Std.Internal.List.insertEntry_cons_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.insertEntry k v (⟨k, v⟩ :: l) = ⟨k, v⟩ :: l
-- Mathlib.MeasureTheory.Group.Prod
MeasureTheory.measure_mul_right_ne_zero : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ : MeasureTheory.Measure G)
  [MeasureTheory.SFinite μ] {s : Set G} [MeasurableInv G] [μ.IsMulLeftInvariant],
  μ s ≠ 0 → ∀ (y : G), μ ((fun x => x * y) ⁻¹' s) ≠ 0
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.List.filter.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Std.Http.Data.Headers
Std.Http.Headers.instEncodeV11 : Std.Http.Internal.Encode Std.Http.Version.v11 Std.Http.Headers
-- Init.Data.UInt.Bitwise
instCommutativeUInt16HAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Mathlib.Algebra.Lie.TransferInstance
/-- Transfer `LieAlgebra` across a `LinearEquiv`  -/
LinearEquiv.lieAlgebra : {R : Type u_1} →
  {M : Type u_2} →
    {L : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (e : M ≃ₗ[R] L) → LieAlgebra R M
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace),
  AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U =
    CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))
-- Mathlib.Order.Monotone.Basic
StrictMono.isMax_of_apply : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a : α},
  StrictMono f → IsMax (f a) → IsMax a
-- Mathlib.LinearAlgebra.FreeModule.PID
instFreeSubtypeMemIdealOfFiniteOfIsTorsionFree : ∀ {R : Type u_2} [inst : CommRing R] [IsPrincipalIdealRing R] [IsDomain R] {S : Type u_4} [inst_3 : CommRing S]
  [inst_4 : Algebra R S] {I : Ideal S} [hI₁ : Module.Finite R ↥I] [hI₂ : Module.IsTorsionFree R ↥I], Module.Free R ↥I
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  [CategoryTheory.Limits.HasZeroObject D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  {F : CategoryTheory.Functor C D}, CategoryTheory.Limits.IsZero F → ∀ {X Y : C} (f : X ⟶ Y), F.map f = 0
-- Mathlib.Algebra.Order.Hom.Monoid
/-- See also `NonnegHomClass.apply_nonneg`.  -/
map_nonneg : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Preorder α] [inst_2 : Zero α]
  [inst_3 : Preorder β] [inst_4 : Zero β] [OrderHomClass F α β] [ZeroHomClass F α β] (f : F) {a : α}, 0 ≤ a → 0 ≤ f a
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
SimpleGraph.IsFiveWheelLike.fst_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} {r k : ℕ} {v w₁ w₂ : α} {s t : Finset α},
  G.IsFiveWheelLike r k v w₁ w₂ s t → w₁ ∉ s
-- Mathlib.Data.EReal.Operations
EReal.top_mul_of_neg : ∀ {x : EReal}, x < 0 → ⊤ * x = ⊥
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.Real
/-- If two regular measures give the same integral for every function in `C_c(X, ℝ)`,
then they are equal.  -/
MeasureTheory.Measure.ext_of_integral_eq_on_compactlySupported : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] [inst_2 : MeasurableSpace X] [BorelSpace X]
  {μ ν : MeasureTheory.Measure X} [LocallyCompactSpace X] [μ.Regular] [ν.Regular],
  (∀ (f : CompactlySupportedContinuousMap X ℝ), ∫ (x : X), f x ∂μ = ∫ (x : X), f x ∂ν) → μ = ν
-- Mathlib.FieldTheory.AbelRuffini
gal_isSolvable_tower : ∀ {F : Type u_1} [inst : Field F] (p q : Polynomial F),
  (Polynomial.map (algebraMap F q.SplittingField) p).Splits →
    Group.IsSolvable p.Gal →
      Group.IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal → Group.IsSolvable q.Gal
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- If we want to construct a CW complex of finite type, we can add the condition `finite_cell` and
relax the condition `mapsTo`.  -/
Topology.CWComplex.mkFiniteType : {X : Type u} →
  [inst : TopologicalSpace X] →
    (C : Set X) →
      (cell : ℕ → Type u) →
        (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) →
          (∀ (n : ℕ), Finite (cell n)) →
            (∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) →
              (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) →
                (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) →
                  (Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) →
                    (∀ (n : ℕ) (i : cell n),
                        Set.MapsTo (↑(map n i)) (Metric.sphere 0 1)
                          (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) →
                      (∀ A ⊆ C,
                          (∀ (n : ℕ) (j : cell n), IsClosed (A ∩ ↑(map n j) '' Metric.closedBall 0 1)) → IsClosed A) →
                        ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C → Topology.CWComplex C
-- Mathlib.Algebra.WithConv
WithConv.toEquiv_congrLinearEquiv : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : AddCommMonoid A] [inst_1 : Semiring R] [inst_2 : Module R A]
  [inst_3 : AddCommMonoid B] [inst_4 : Module R B] (f : A ≃ₗ[R] B),
  (WithConv.congrLinearEquiv f).toEquiv = WithConv.congr f.toEquiv
-- Mathlib.Algebra.Lie.Weights.Linear
/-- Given a Lie module `M` of a nilpotent Lie algebra `L` with coefficients in `R`,
if a function `χ : L → R` has a simultaneous generalized eigenvector for the action of `L`
then it has a simultaneous true eigenvector, provided `M` is Noetherian and has linear weights.  -/
LieModule.exists_forall_lie_eq_smul : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [LieModule.LinearWeights R L M] [IsNoetherian R M] (χ : LieModule.Weight R L M),
  ∃ m, m ≠ 0 ∧ ∀ (x : L), ⁅x, m⁆ = χ x • m
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mem_closure_iff_sup_sdiff : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Set α},
  IsSublattice s → ⊥ ∈ s → ⊤ ∈ s → ∀ {a : α}, a ∈ BooleanSubalgebra.closure s ↔ ∃ t, a = t.sup fun x => ↑x.1 \ ↑x.2
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Alt.default.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (code : Lean.Compiler.LCNF.Code pu),
  sizeOf (Lean.Compiler.LCNF.Alt.default code) = 1 + sizeOf code
-- Mathlib.Combinatorics.Matroid.Basic
/-- If every base of `M₁` is independent in `M₂` and vice versa, then `M₁ = M₂`.  -/
Matroid.ext_isBase_indep : ∀ {α : Type u_1} {M₁ M₂ : Matroid α},
  M₁.E = M₂.E → (∀ ⦃B : Set α⦄, M₁.IsBase B → M₂.Indep B) → (∀ ⦃B : Set α⦄, M₂.IsBase B → M₁.Indep B) → M₁ = M₂
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅}, t.minKey he ∈ t
-- Mathlib.Data.Complex.Basic
Complex.normSq_natCast : ∀ (n : ℕ), Complex.normSq ↑n = ↑n * ↑n
-- Mathlib.Topology.Order.Lattice
ContinuousWithinAt.inf : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] [inst_2 : Min L]
  [ContinuousInf L] {f g : X → L} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun a => f a ⊓ g a) s x
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.instFreeSubtypeMemSubmodule : ∀ {R : Type u_1} [inst : Semiring R] {n : ℕ}, Module.Free R ↥(Polynomial.degreeLT R n)
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, if one of `A` and `B` is flat, then for any family of
`R`-linearly independent elements `{ a_i }` of `A`, and any family of
`R`-linearly independent elements `{ b_j }` of `B`, the family `{ a_i * b_j }` in `S` is
also `R`-linearly independent.  -/
Subalgebra.LinearDisjoint.linearIndependent_mul_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    Module.Flat R ↥A ∨ Module.Flat R ↥B →
      ∀ {κ : Type u_1} {ι : Type u_2} {a : κ → ↥A} {b : ι → ↥B},
        LinearIndependent R a → LinearIndependent R b → LinearIndependent R fun i => ↑(a i.1) * ↑(b i.2)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_union_le_size_add_size : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (m₁ ∪ m₂).size ≤ m₁.size + m₂.size
-- Mathlib.Order.Comparable
AntisymmRel.incompRel_congr : ∀ {α : Type u_1} {a b c d : α} [inst : Preorder α],
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b →
    AntisymmRel (fun x1 x2 => x1 ≤ x2) c d →
      (IncompRel (fun x1 x2 => x1 ≤ x2) a c ↔ IncompRel (fun x1 x2 => x1 ≤ x2) b d)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- Implementation of `CommMon.equivLaxBraidedFunctorPUnit`.  -/
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.unitIso : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        CategoryTheory.Functor.id (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u + 1}) C) ≅
          (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C).comp
            (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C)
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.orderBot : {α : Type u_1} → [inst : LE α] → [OrderBot α] → OrderBot (Additive α)
-- Mathlib.Data.Finset.Max
Finset.le_max : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α} {s : Finset α}, a ∈ s → ↑a ≤ s.max
-- Mathlib.Data.Multiset.ZeroCons
Multiset.mem_singleton : ∀ {α : Type u_1} {a b : α}, b ∈ {a} ↔ b = a
-- Lean.Elab.DeprecatedSyntax
Lean.Linter.linter.deprecated.syntax : Lean.Option Bool
-- Plausible.Sampleable
/-- This is kept for backwards compatibility  -/
Plausible.SampleableExt.mkSelfContained : {α : Type u_1} → [Repr α] → [Plausible.Shrinkable α] → Plausible.Gen α → Plausible.SampleableExt α
-- Mathlib.Data.PSigma.Order
PSigma.Lex.preorder : {ι : Type u_1} → {α : ι → Type u_2} → [Preorder ι] → [(i : ι) → Preorder (α i)] → Preorder (Σₗ' (i : ι), α i)
-- Mathlib.RingTheory.RingHom.EssFiniteType
RingHom.EssFiniteType.isStableUnderBaseChange : RingHom.IsStableUnderBaseChange fun {R S} [CommRing R] [CommRing S] => RingHom.EssFiniteType
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint, if `A` is a flat `R`-module, then for any family of
`R`-linearly independent elements of `B`, they are also `A`-linearly independent.  -/
Subalgebra.LinearDisjoint.linearIndependent_right_of_flat : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {A B : Subalgebra R S},
  A.LinearDisjoint B →
    ∀ [Module.Flat R ↥A] {ι : Type u_1} {b : ι → ↥B}, LinearIndependent R b → LinearIndependent (↥A) (⇑B.val ∘ b)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f.op g.op).unop h
-- Mathlib.Logic.Nontrivial.Defs
/-- An injective function from a nontrivial type has an argument at
which it does not take a given value.  -/
Function.Injective.exists_ne : ∀ {α : Type u_1} {β : Type u_2} [Nontrivial α] {f : α → β}, Function.Injective f → ∀ (y : β), ∃ x, f x ≠ y
-- Mathlib.Algebra.Group.Units.Basic
Units.mul_left_inj : ∀ {α : Type u} [inst : Monoid α] (a : αˣ) {b c : α}, b * ↑a = c * ↑a ↔ b = c
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instReflBEqPoly : ReflBEq Lean.Grind.CommRing.Poly
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_comp_addSingleEquiv : ∀ {R : Type u_4} {M : Type u_5} {ι : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (i : ι)
  (c : ι → R) (h₀ : c i = 0) (v : ι → M),
  Finsupp.linearCombination R v ∘ₗ ↑(Finsupp.addSingleEquiv i c h₀) =
    Finsupp.linearCombination R (v + fun x => c x • v i)
-- Mathlib.RingTheory.Polynomial.RationalRoot
num_isRoot_scaleRoots_of_aeval_eq_zero : ∀ {A : Type u_1} {K : Type u_2} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDomain A] [inst_5 : UniqueFactorizationMonoid A] {p : Polynomial A} {x : K},
  (Polynomial.aeval x) p = 0 → (p.scaleRoots ↑(IsFractionRing.den A x)).IsRoot (IsFractionRing.num A x)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `Left.neg_nonpos_iff`.

---

Uses `left` co(ntra)variant.  -/
nonneg_of_neg_nonpos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] {a : α}, -a ≤ 0 → 0 ≤ a
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- **Alias** of `MeasureTheory.VectorMeasure.of_sdiff_of_sdiff_eq_zero`. -/
MeasureTheory.VectorMeasure.of_diff_of_diff_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A B : Set α},
  MeasurableSet A → MeasurableSet B → v (B \ A) = 0 → v (A \ B) + v B = v A
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₇_diag : ∀ (i : Fin 7), CartanMatrix.E₇ i i = 2
-- Mathlib.Analysis.Convex.Intrinsic
/-- The intrinsic interior of a nonempty convex set is nonempty.  -/
Set.Nonempty.intrinsicInterior : ∀ {V : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [FiniteDimensional ℝ V] {s : Set V},
  Convex ℝ s → s.Nonempty → (intrinsicInterior ℝ s).Nonempty
-- Mathlib.Order.Monotone.Defs
StrictAnti.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, StrictAnti g → StrictAnti f → StrictMono (g ∘ f)
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_toBitVec : ∀ (a : UInt8), { toBitVec := a.toBitVec } = a
-- Mathlib.Algebra.Colimit.Ring
Ring.instOneDirectLimit : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] → (f : (i j : ι) → i ≤ j → G i → G j) → One (Ring.DirectLimit G f)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_rpow_of_neg : ∀ {x y z : ℝ}, 0 < x → x < y → z < 0 → y ^ z < x ^ z
-- Lean.Meta.Tactic.SolveByElim
Lean.Meta.SolveByElim.SolveByElimConfig.mk.sizeOf_spec : ∀ (toApplyRulesConfig : Lean.Meta.SolveByElim.ApplyRulesConfig) (backtracking intro constructor suggestions : Bool),
  sizeOf
      { toApplyRulesConfig := toApplyRulesConfig, backtracking := backtracking, intro := intro,
        constructor := constructor, suggestions := suggestions } =
    1 + sizeOf toApplyRulesConfig + sizeOf backtracking + sizeOf intro + sizeOf constructor + sizeOf suggestions
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPushoutsAlong.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C} {X Y : C} {f : X ⟶ Y},
  (∀ {W : C} (g : X ⟶ W), P g → CategoryTheory.Limits.HasPushout g f) → P.HasPushoutsAlong f
-- Mathlib.Algebra.Free
FreeSemigroup.traverse_pure : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x : α), traverse F (pure x) = pure <$> F x
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.shift_app_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] [CategoryTheory.NatTrans.CommShift τ A] (a : A) (X : C) {Z : D}
  (h : (CategoryTheory.shiftFunctor D a).obj (F₂.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) h =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).inv.app X)
      (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₂ a).hom.app X) h))
-- Mathlib.Algebra.Order.UpperLower
LowerSet.commSemigroup : {α : Type u_1} → [inst : CommGroup α] → [inst_1 : Preorder α] → [IsOrderedMonoid α] → CommSemigroup (LowerSet α)