mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.liftCocone_ι_app : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {J : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J] (D : CategoryTheory.Functor J T) {X : T}
  (s : (CategoryTheory.Functor.const J).obj X ⟶ D) (c : CategoryTheory.Limits.Cocone D) (p : X ⟶ c.pt)
  (hp : ∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = p) (j : J),
  (CategoryTheory.Under.liftCocone D s c p hp).ι.app j = CategoryTheory.Under.homMk (c.ι.app j) ⋯
-- Mathlib.RingTheory.Noetherian.Basic
instIsNoetherianRingForallOfFinite : ∀ {ι : Type u_2} [Finite ι] {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsNoetherianRing (R i)],
  IsNoetherianRing ((i : ι) → R i)
-- Mathlib.CategoryTheory.Sites.PreservesLocallyBijective
CategoryTheory.Presheaf.isLocallyInjective_whisker : ∀ {C : Type u_1} {D : Type u_2} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D)
  (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor Dᵒᵖ A} (f : F ⟶ G) {FA : A → A → Type u_4}
  {CA : A → Type u_5} [inst_3 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_4 : CategoryTheory.ConcreteCategory A FA] [H.IsCocontinuous J K]
  [CategoryTheory.Presheaf.IsLocallyInjective K f], CategoryTheory.Presheaf.IsLocallyInjective J (H.op.whiskerLeft f)
-- Mathlib.Computability.RegularExpressions
RegularExpression.matchEpsilon.eq_5 : ∀ {α : Type u_1} (P Q : RegularExpression α), (P.comp Q).matchEpsilon = (P.matchEpsilon && Q.matchEpsilon)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
cbiSup_empty : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompletePartialOrderSup α] {f : β → α}, ⨆ i ∈ ∅, f i = sSup ∅
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.commute_iff_commute : ∀ {f g : CircleDeg1Lift}, Commute f g ↔ Function.Commute ⇑f ⇑g
-- Mathlib.Topology.Sets.Order
ClopenUpperSet.coe_mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LE α] (s : TopologicalSpace.Clopens α)
  (h : IsUpperSet s.carrier), ↑{ toClopens := s, upper' := h } = ↑s
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.step_takeWhile.match_3.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    {it : Std.Iter β} →
      (motive : it.Step → Sort u_2) →
        (x : it.Step) →
          ((it' : Std.Iter β) →
              (out : β) →
                (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩) →
            ((it' : Std.Iter β) →
                (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩) →
              ((h : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩) → motive x
-- Mathlib.Order.Monotone.Monovary
MonovaryOn.dual : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, MonovaryOn f g s → MonovaryOn (⇑OrderDual.toDual ∘ f) (⇑OrderDual.toDual ∘ g) s
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {outWidth : ℕ} {aig : Std.Sat.AIG α} {w len : ℕ} (iterNum : ℕ)
  (oldLayer oldLayer_1 : aig.RefVec (len * w)),
  oldLayer = oldLayer_1 →
    ∀ (newLayer newLayer_1 : aig.RefVec (iterNum * w)),
      newLayer = newLayer_1 →
        ∀ (hold : 2 * (iterNum - 1) < len) (hout : outWidth = (len + 1) / 2 * w),
          Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer newLayer hold hout =
            Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer_1 newLayer_1 hold hout
-- Mathlib.RingTheory.HahnSeries.HEval
/-- The `R`-algebra homomorphism from `R⟦X⟧` to `R⟦Γ⟧` given by sending the power series
variable `X` to a positive order element `x` and extending to infinite sums.  -/
PowerSeries.heval : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : LinearOrder Γ] →
        [inst_2 : IsOrderedCancelAddMonoid Γ] →
          [inst_3 : CommRing R] → HahnSeries Γ R → PowerSeries R →ₐ[R] HahnSeries Γ R
-- Std.Http.Protocol.H1.Error
Std.Http.Protocol.H1.Error.badMessage.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Error.badMessage = 1
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.core_hom_app_iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : CategoryTheory.Core C),
  (α.core.hom.app X).iso.hom = α.hom.app X.of
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.isLeftAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G), F.IsLeftAdjoint
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isBigOTVS_neg_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg E],
  (-f) =O[𝕜; l] g ↔ f =O[𝕜; l] g
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_const : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] (T : Set α → F →L[ℝ] F'),
  T ∅ = 0 →
    ∀ (x : F) {m : MeasurableSpace α},
      MeasureTheory.SimpleFunc.setToSimpleFunc T (MeasureTheory.SimpleFunc.const α x) = (T Set.univ) x
-- Mathlib.Analysis.Seminorm
Seminorm.instIsOrderedCancelAddMonoid : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E],
  IsOrderedCancelAddMonoid (Seminorm 𝕜 E)
-- Mathlib.Tactic.Linter.Style
/-- Linter that checks for definitions whose name contains an underscore:
such names violate the naming convention.  -/
Mathlib.Linter.Style.nameCheck.defsWithUnderscore : Batteries.Tactic.Lint.Linter
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.image_vadd_distrib : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Add α] [inst_1 : Add β] [inst_2 : FunLike F α β]
  [AddHomClass F α β] (f : F) (a : α) (s : Set α), ⇑f '' (a +ᵥ s) = f a +ᵥ ⇑f '' s
-- Mathlib.Geometry.Manifold.IntegralCurve.Transform
IsMIntegralCurveOn.comp_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {γ : ℝ → M}
  {v : (x : M) → TangentSpace I x} {s : Set ℝ},
  IsMIntegralCurveOn γ v s → ∀ (a : ℝ), IsMIntegralCurveOn (γ ∘ fun x => x * a) (a • v) {t | t * a ∈ s}
-- Mathlib.Data.Sym.Basic
Sym.equivCongr_symm_apply : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (e : α ≃ β) (x : Sym β n), (Sym.equivCongr e).symm x = Sym.map (⇑e.symm) x
-- Mathlib.GroupTheory.Goursat
/-- For `I` a subgroup of `G × H`, `I.goursatFst` is the kernel of the projection map `I → H`,
considered as a subgroup of `G`.

This is the first subgroup appearing in Goursat's lemma. See `AddSubgroup.goursat`.  -/
AddSubgroup.goursatFst : {G : Type u_1} → {H : Type u_2} → [inst : AddGroup G] → [inst_1 : AddGroup H] → AddSubgroup (G × H) → AddSubgroup G
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTGEIsoGELT_hom_app_fac' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLTGEIsoGELT a b).hom.app X)
      ((t.eTruncGE.obj a).map ((t.eTruncLTι b).app X)) =
    (t.eTruncLTι b).app ((t.eTruncGE.obj a).obj X)
-- Mathlib.Data.Sum.Order
Sum.Lex.inr_top : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] [inst_2 : OrderTop β], toLex (Sum.inr ⊤) = ⊤
-- Mathlib.Algebra.Polynomial.Derivation
Polynomial.derivative'_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (a : Polynomial R), Polynomial.derivative' a = Polynomial.derivative a
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.comp.match_1.eq_5 : ∀ {C : Type u_1}
  (motive : CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → CategoryTheory.WithInitial C → Sort u_2)
  (h_1 :
    (_X _Y _Z : C) →
      motive (CategoryTheory.WithInitial.of _X) (CategoryTheory.WithInitial.of _Y) (CategoryTheory.WithInitial.of _Z))
  (h_2 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive CategoryTheory.WithInitial.star x (CategoryTheory.WithInitial.of _X))
  (h_3 :
    (x : CategoryTheory.WithInitial C) →
      (_X : C) → motive x (CategoryTheory.WithInitial.of _X) CategoryTheory.WithInitial.star)
  (h_4 :
    (_Y : C) →
      (x : CategoryTheory.WithInitial C) → motive (CategoryTheory.WithInitial.of _Y) CategoryTheory.WithInitial.star x)
  (h_5 : Unit → motive CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.of _Z =>
      h_1 _X _Y _Z
    | CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.of _X => h_2 x _X
    | x, CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.star => h_3 x _X
    | CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.star, x => h_4 _Y x
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star => h_5 ()) =
    h_5 ()
-- Mathlib.MeasureTheory.Group.FundamentalDomain
/-- The `addCovolume` can be computed by taking the `volume` of any given additive
fundamental domain `s`.  -/
MeasureTheory.IsAddFundamentalDomain.covolume_eq_volume : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  (ν : MeasureTheory.Measure α) [Countable G] [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α ν]
  {s : Set α}, MeasureTheory.IsAddFundamentalDomain G s ν → MeasureTheory.addCovolume G α ν = ν s
-- Init.System.IO
IO.Process.Output.mk.sizeOf_spec : ∀ (exitCode : UInt32) (stdout stderr : String),
  sizeOf { exitCode := exitCode, stdout := stdout, stderr := stderr } =
    1 + sizeOf exitCode + sizeOf stdout + sizeOf stderr
-- Lean.Level
Lean.Level.data : Lean.Level → Lean.Level.Data
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_singleL : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l : Std.DTreeMap.Internal.Impl α β} {rk : α} {rv : β rk}
  {rl rr : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.singleL k v l rk rv rl rr).toListModel =
    l.toListModel ++ ⟨k, v⟩ :: (rl.toListModel ++ ⟨rk, rv⟩ :: rr.toListModel)
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  (AlgebraicTopology.AlternatingFaceMapComplex.obj X).d (n + 1) n = ∑ i, (-1) ^ ↑i • X.δ i
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMapZero
ContinuousMapZero.aeStronglyMeasurable_restrict_mkD_restrict_of_uncurry : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] {s : Set X} {t : Set Y} [CompactSpace ↑t] [inst_4 : Zero ↑t]
  [inst_5 : TopologicalSpace X] [OpensMeasurableSpace X] [SecondCountableTopologyEither X C(↑t, E)],
  MeasurableSet s →
    ∀ (f : X → Y → E) (g : ContinuousMapZero (↑t) E),
      ContinuousOn (Function.uncurry f) (s ×ˢ t) →
        (∀ᵐ (x : X) ∂μ.restrict s, f x ↑0 = 0) →
          MeasureTheory.AEStronglyMeasurable (fun x => ContinuousMapZero.mkD (t.domRestrict (f x)) g) (μ.restrict s)
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.isLeftCancelAdd : ∀ {α : Type u} [inst : Mul α] [IsLeftCancelMul α], IsLeftCancelAdd (Additive α)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instEmptyCollectionTextEditBatch : EmptyCollection Lean.Lsp.TextEditBatch
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
SheafOfModules.instIsRightAdjointPushforwardCompSheafRingCatMapSheafPushforwardContinuous : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {D' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat}
  {R : CategoryTheory.Sheaf K RingCat} [inst_3 : F.IsContinuous J K]
  (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) [(SheafOfModules.pushforward φ).IsRightAdjoint]
  {K' : CategoryTheory.GrothendieckTopology D'} {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat}
  [inst_5 : G.IsContinuous K K'] [inst_6 : (F.comp G).IsContinuous J K']
  (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') [(SheafOfModules.pushforward ψ).IsRightAdjoint],
  (SheafOfModules.pushforward
      (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ))).IsRightAdjoint
-- Mathlib.LinearAlgebra.Dimension.Free
Module.finrank_div_finrank_cancel_right : ∀ (F : Type u) (K : Type v) (A : Type w) [inst : Semiring F] [inst_1 : Semiring K] [inst_2 : AddCommMonoid A]
  [inst_3 : Module F K] [inst_4 : Module K A] [inst_5 : Module F A] [IsScalarTower F K A] [StrongRankCondition F]
  [StrongRankCondition K] [Module.Free F K] [Module.Free K A],
  Module.finrank K A ≠ 0 → Module.finrank F A / Module.finrank K A = Module.finrank F K
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_mono_nnnorm_ae : ∀ {α : Type u_1} {F : Type u_5} {G : Type u_6} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup F] [inst_1 : NormedAddCommGroup G] {f : α → F} {g : α → G},
  (∀ᵐ (x : α) ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) → MeasureTheory.eLpNormEssSup f μ ≤ MeasureTheory.eLpNormEssSup g μ
-- Mathlib.NumberTheory.Primorial
primorial_pos : ∀ (n : ℕ), 0 < primorial n
-- Mathlib.Data.Int.Star
Int.addSubmonoid_closure_range_mul_self : AddSubmonoid.closure (Set.range fun x => x * x) = AddSubmonoid.nonneg ℤ
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.biprod_inr_desc_f_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {M : HomologicalComplex C c}
  (α : K ⟶ M) (β : L ⟶ M) (i : ι) {Z : C} (h : M.X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.biprod.desc α β).f i) h) =
    CategoryTheory.CategoryStruct.comp (β.f i) h
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.monotone_or_antitone_iff_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : α → β},
  Monotone f ∨ Antitone f ↔ ∀ (a b c : α), c ∈ Set.uIcc a b → f c ∈ Set.uIcc (f a) (f b)
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- **Alias** of `Stirling.log_stirlingSeq_sdiff_le_geo_sum`.

---

We have a bound for successive elements in the sequence `log (stirlingSeq k)`.  -/
Stirling.log_stirlingSeq_diff_le_geo_sum : ∀ (n : ℕ),
  Real.log (Stirling.stirlingSeq (n + 1)) - Real.log (Stirling.stirlingSeq (n + 2)) ≤
    (1 / (2 * ↑(n + 1) + 1)) ^ 2 / (1 - (1 / (2 * ↑(n + 1) + 1)) ^ 2)
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.mem_sInf : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R] {S : Set (TwoSidedIdeal R)} {x : R}, x ∈ sInf S ↔ ∀ I ∈ S, x ∈ I
-- Mathlib.Data.Set.Image
/-- If the preimage of a set under an injective map is nontrivial, the set is nontrivial.  -/
Set.nontrivial_of_preimage : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Injective f → ∀ (s : Set β), (f ⁻¹' s).Nontrivial → s.Nontrivial
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgResult.ext : (ext₁? : Option Lean.Meta.SimpExtension) →
  (ext₂? : Option Lean.Meta.Simp.SimprocExtension) →
    (ext₁?.isSome || ext₂?.isSome) = true → Lean.Elab.Tactic.ElabSimpArgResult
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
_private.Lean.Meta.Tactic.Simp.Arith.Int.Basic.0.Int.Internal.Linear.Poly.toExpr.go : Option Int.Internal.Linear.Expr → Int.Internal.Linear.Poly → Int.Internal.Linear.Expr
-- Mathlib.Order.Lattice
SemilatticeSup.ext : ∀ {α : Type u_1} {A B : SemilatticeSup α}, (∀ (x y : α), x ≤ y ↔ x ≤ y) → A = B
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.orderMonoidIso.congr_simp : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedCommGroupWithZero Γ₀]
  [inst_1 : LinearOrderedCommGroupWithZero Γ'₀] [inst_2 : Ring R] {v : Valuation R Γ₀} {w : Valuation R Γ'₀}
  (h : v.IsEquiv w), h.orderMonoidIso = h.orderMonoidIso
-- Mathlib.Logic.Function.FiberPartition
/-- Any `a : Fiber f` is of the form `f ⁻¹' {x}` for some `x` in the image of `f`. We define `a.image`
as an arbitrary such `x`.
 -/
Function.Fiber.image : {Y : Type u_2} → {Z : Type u_3} → (f : Y → Z) → Function.Fiber f → Z
-- Mathlib.Topology.Connected.PathConnected
/-- If `h : X → Y` is a homeomorphism, `h(s)` is path-connected iff `s` is.  -/
Homeomorph.isPathConnected_image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set X} (h : X ≃ₜ Y),
  IsPathConnected (⇑h '' s) ↔ IsPathConnected s
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.isStableUnderBaseChange : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), F.relativelyRepresentable.IsStableUnderBaseChange
-- Mathlib.Combinatorics.SimpleGraph.Extremal.TuranDensity
/-- The edge density of `H`-free simple graphs on `turanDensityConst H ε` vertices
is at most `turanDensity H + ε`.

Contrapositively, `turanDensity H + ε` is the density at which `H` is always contained in simple
graphs on `turanDensityConst H ε` vertices.

Note that this value is only defined for positive `ε` and `turanDensityConst H ε = 0` for non
positive `ε`.  -/
SimpleGraph.turanDensityConst : {W : Type u_1} → SimpleGraph W → ℝ → ℕ
-- Mathlib.MeasureTheory.Function.AEEqFun
ContinuousMap.coeFn_toAEEqFun : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [inst_1 : TopologicalSpace α]
  [inst_2 : BorelSpace α] [inst_3 : TopologicalSpace β] [inst_4 : SecondCountableTopologyEither α β]
  [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] (f : C(α, β)), ↑(ContinuousMap.toAEEqFun μ f) =ᵐ[μ] ⇑f
-- Mathlib.RingTheory.Localization.AtPrime.Extension
IsLocalization.AtPrime.equivQuotientMapOfIsMaximal.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p p_1 : Ideal R)
  (e_p : p = p_1) [inst_3 : p.IsPrime] (Sₚ : Type u_4) [inst_4 : CommRing Sₚ] [inst_5 : Algebra S Sₚ]
  [inst_6 : IsLocalization (Algebra.algebraMapSubmonoid S p.primeCompl) Sₚ] (P : Ideal S) [hPp : P.LiesOver p]
  [inst_7 : P.IsMaximal],
  IsLocalization.AtPrime.equivQuotientMapOfIsMaximal p Sₚ P =
    IsLocalization.AtPrime.equivQuotientMapOfIsMaximal p_1 Sₚ P
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- Lift a quasi-compact cover of a `u`-scheme in an arbitrary universe to `u`. The indexing
type is constructed by choosing finitely many compact opens above every affine open.
This cover is again quasi-compact.
 -/
AlgebraicGeometry.QuasiCompactCover.ulift : {S : AlgebraicGeometry.Scheme} →
  (𝒰 : CategoryTheory.PreZeroHypercover S) →
    [AlgebraicGeometry.QuasiCompactCover 𝒰] → CategoryTheory.PreZeroHypercover S
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_injective : ∀ {α : Type u_1} [inst : LinearOrder α], Function.Injective Set.Ioi
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.Context.mk : ℕ → ℕ → Lean.Meta.SynthInstance.Context
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.currySum_apply' : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : Type u_2} [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  (f : MultilinearMap R (fun x => N) M₂) (u : ι → N) (v : ι' → N), (f.currySum u) v = f (Sum.elim u v)
-- Mathlib.Data.Ordmap.Ordset
Ordnode.map.eq_def : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (x : Ordnode α),
  Ordnode.map f x =
    match x with
    | Ordnode.nil => Ordnode.nil
    | Ordnode.node s l x r => Ordnode.node s (Ordnode.map f l) (f x) (Ordnode.map f r)
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.findMax'.match_1.eq_2 : ∀ {α : Type u_1} (motive : α → Ordnode α → Sort u_2) (x : α) (size : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α)
  (h_1 : (x : α) → motive x Ordnode.nil)
  (h_2 : (x : α) → (size : ℕ) → (l : Ordnode α) → (x_2 : α) → (r : Ordnode α) → motive x (Ordnode.node size l x_2 r)),
  (match x, Ordnode.node size l x_1 r with
    | x, Ordnode.nil => h_1 x
    | x, Ordnode.node size l x_2 r => h_2 x size l x_2 r) =
    h_2 x size l x_1 r
-- Mathlib.Topology.WithTopology
WithTopology.instMin : {X : Type u_1} → (t : TopologicalSpace X) → [Min X] → Min (WithTopology X t)
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.indepFun_iff_measure_inter_preimage_eq_mul`. -/
ProbabilityTheory.Kernel.IndepFun.measure_inter_preimage_eq_mul : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'} {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'},
  ProbabilityTheory.Kernel.IndepFun f g κ μ →
    ∀ (s : Set β) (t : Set β'),
      MeasurableSet s → MeasurableSet t → ∀ᵐ (a : α) ∂μ, (κ a) (f ⁻¹' s ∩ g ⁻¹' t) = (κ a) (f ⁻¹' s) * (κ a) (g ⁻¹' t)
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeOmitMax : Lean.Options → Bool
-- Mathlib.Order.Monotone.MonovaryOrder
instIsStrictTotalOrderMonovaryOrder : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] (f : ι → α) (g : ι → β),
  IsStrictTotalOrder ι (MonovaryOrder f g)
-- Mathlib.Data.Nat.Prime.Basic
Nat.not_prime_iff_exists_mul_eq : ∀ {n : ℕ}, 2 ≤ n → (¬Nat.Prime n ↔ ∃ a b, a < n ∧ b < n ∧ a * b = n)