mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.minEntry?.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Impl α β),
  x.minEntry? =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf => none
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => some ⟨k, v⟩
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      l.minEntry?
-- Mathlib.Data.Nat.Fib.Zeckendorf
Nat.zeckendorf.eq_2 : ∀ (n : ℕ), n.succ.zeckendorf = n.succ.greatestFib :: (n.succ - Nat.fib n.succ.greatestFib).zeckendorf
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- Let `f : G →* G` be a continuous surjective group endomorphism
of a compact topological group with second countable topology.
If the preimages of `1` under the iterations of `f` are dense,
then `f` is ergodic with respect to any finite inner regular left invariant measure.  -/
MonoidHom.ergodic_of_dense_iUnion_preimage_one : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [SecondCountableTopology G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] [CompactSpace G] {μ : MeasureTheory.Measure G} [μ.IsHaarMeasure]
  (f : G →* G), Dense (⋃ n, (⇑f)^[n] ⁻¹' 1) → Continuous ⇑f → Function.Surjective ⇑f → Ergodic (⇑f) μ
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.withSeminorms' : ∀ (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (n : ℕ∞) (K : TopologicalSpace.Compacts E),
  WithSeminorms (ContDiffMapSupportedIn.supSeminorm 𝕜 E F n K)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.alter.congr_simp : ∀ {α : Type u} [inst : BEq α] [inst_1 : EquivBEq α] [inst_2 : Hashable α] {β : Type v}
  (m m_1 : Std.DHashMap.Raw α fun x => β),
  m = m_1 →
    ∀ (a a_1 : α),
      a = a_1 →
        ∀ (f f_1 : Option β → Option β),
          f = f_1 → Std.DHashMap.Raw.Const.alter m a f = Std.DHashMap.Raw.Const.alter m_1 a_1 f_1
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.Γ_def : AlgebraicGeometry.LocallyRingedSpace.Γ =
  AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.op.comp AlgebraicGeometry.SheafedSpace.Γ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_a₂ : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) (S : Type s) [inst_1 : CommRing S]
  [inst_2 : Algebra R S], (W.baseChange S).a₂ = (algebraMap R S) W.a₂
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_intCast_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Ring R] [inst_1 : AddCommGroup α]
  [inst_2 : StarAddMonoid α] [inst_3 : Module R α] (c : ℤ) (M : Matrix m n α),
  (↑c • M).conjTranspose = ↑c • M.conjTranspose
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.TensorProduct.tensorQuotientEquiv_apply_tmul : ∀ {R : Type u_1} (S : Type u_2) (T : Type u_3) (A : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : CommRing A] [inst_6 : Algebra R A]
  [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A] (I : Ideal T) (a : A) (t : T),
  (Algebra.TensorProduct.tensorQuotientEquiv S T A I) (a ⊗ₜ[R] (Ideal.Quotient.mk I) t) =
    (Ideal.Quotient.mk (Ideal.map Algebra.TensorProduct.includeRight I)) (a ⊗ₜ[R] t)
-- Mathlib.AlgebraicTopology.ModelCategory.CategoryWithCofibrations
HomotopicalAlgebra.mem_trivialCofibrations_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_2 : HomotopicalAlgebra.CategoryWithWeakEquivalences C],
  HomotopicalAlgebra.trivialCofibrations C f ↔ HomotopicalAlgebra.Cofibration f ∧ HomotopicalAlgebra.WeakEquivalence f
-- Init.Grind.Config
Lean.Grind.LinarithConfig.mk.inj : ∀ {toNoopConfig toNoopConfig_1 : Lean.Grind.NoopConfig},
  { toNoopConfig := toNoopConfig } = { toNoopConfig := toNoopConfig_1 } → toNoopConfig = toNoopConfig_1
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isTrail_rotate : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} [inst : DecidableEq V] {c : G.Walk v v} (hu : u ∈ c.support),
  (c.rotate u hu).IsTrail ↔ c.IsTrail
-- Mathlib.Topology.MetricSpace.Algebra
TendstoLocallyUniformlyOn.mul₀ : ∀ {X : Type u_3} {M : Type u_4} {ι : Type u_5} [inst : TopologicalSpace X] [inst_1 : PseudoMetricSpace M]
  [inst_2 : Zero M] [inst_3 : Mul M] [IsBoundedSMul M M] {s : Set X} {F G : ι → X → M} {f g : X → M} {l : Filter ι},
  TendstoLocallyUniformlyOn F f l s →
    TendstoLocallyUniformlyOn G g l s →
      ContinuousOn f s → ContinuousOn g s → TendstoLocallyUniformlyOn (F * G) (f * g) l s
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.post.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasLimit (F.comp G)],
  CategoryTheory.Limits.limit.post F G =
    CategoryTheory.Limits.limit.lift (F.comp G) (G.mapCone (CategoryTheory.Limits.limit.cone F))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a fallback : α} {v : β},
  (t.insertIfNew k v).getKeyD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getKeyD a fallback
-- Mathlib.Order.Filter.Pointwise
/-- `pure` operation as a `MulHom`.  -/
Filter.pureMulHom : {α : Type u_2} → [inst : Mul α] → α →ₙ* Filter α
-- Mathlib.Analysis.Analytic.Constructions
/-- Multiplication of analytic functions (valued in a normed `𝕜`-algebra) is analytic.  -/
AnalyticWithinAt.mul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {A : Type u_7} [inst_3 : NormedRing A] [inst_4 : NormedAlgebra 𝕜 A] {f g : E → A}
  {s : Set E} {z : E}, AnalyticWithinAt 𝕜 f s z → AnalyticWithinAt 𝕜 g s z → AnalyticWithinAt 𝕜 (fun x => f x * g x) s z
-- Mathlib.Topology.Order.WithTop
WithTop.tendsto_nhds_top_iff : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι] {α : Type u_2}
  {f : Filter α} (x : α → WithTop ι), Filter.Tendsto x f (nhds ⊤) ↔ ∀ (i : ι), ∀ᶠ (a : α) in f, ↑i < x a
-- Mathlib.LinearAlgebra.Pi
LinearMap.const_apply : ∀ {R : Type u} {M₂ : Type w} {ι : Type x} [inst : Semiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  (x : M₂), LinearMap.const x = Function.const ι x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order
/-- In a unital C⋆-algebra, if `a` is strictly positive, and `a ≤ b`, then `b` is
invertible.  -/
CStarAlgebra.isUnit_of_le : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] (a : A) {b : A},
  a ≤ b → autoParam (IsStrictlyPositive a) CStarAlgebra.isUnit_of_le._auto_1 → IsUnit b
-- Init.NotationExtra
unexpandSubtype : Lean.PrettyPrinter.Unexpander
-- Init.Data.List.Control
/-- Applies the applicative action `f` to every element in the list, in order.

If `m` is also a `Monad`, then using `List.forM` can be more efficient.

`List.mapA` is a variant that collects results.
 -/
List.forA : {m : Type u → Type v} → [Applicative m] → {α : Type w} → List α → (α → m PUnit.{u + 1}) → m PUnit.{u + 1}
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- The inclusion pseudofunctor from the locally discrete bicategory on the path category into the
free bicategory.
 -/
CategoryTheory.FreeBicategory.inclusion : (B : Type u) →
  [inst : Quiver B] →
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Paths B))
      (CategoryTheory.FreeBicategory B)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- Coercing the result of `Units.instInv` is the same as coercing first and applying the
nonsingular inverse.  -/
Matrix.coe_units_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : (Matrix n n α)ˣ),
  ↑A⁻¹ = (↑A)⁻¹
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.const_apply : ∀ (x y : SimplexCategory) (i : Fin (y.len + 1)) (a : Fin (x.len + 1)),
  (SimplexCategory.Hom.toOrderHom (x.const y i)) a = i
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.PromiseCheckedResult.mk.inj : ∀ {mainEnv asyncEnv : Lean.Environment} {checkedEnvPromise : IO.Promise Lean.Kernel.Environment}
  {mainEnv_1 asyncEnv_1 : Lean.Environment} {checkedEnvPromise_1 : IO.Promise Lean.Kernel.Environment},
  { mainEnv := mainEnv, asyncEnv := asyncEnv, checkedEnvPromise := checkedEnvPromise } =
      { mainEnv := mainEnv_1, asyncEnv := asyncEnv_1, checkedEnvPromise := checkedEnvPromise_1 } →
    mainEnv = mainEnv_1 ∧ asyncEnv = asyncEnv_1 ∧ checkedEnvPromise = checkedEnvPromise_1
-- Mathlib.Order.SuccPred.Basic
PredOrder.ofCore.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] (succ : α → α) (hn : ∀ {a : α}, ¬IsMin a → ∀ (b : α), b < a ↔ b ≤ succ a)
  (hm : ∀ (a : α), IsMin a → succ a = a),
  PredOrder.ofCore succ hn hm = { pred := succ, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }
-- Mathlib.CategoryTheory.Limits.Shapes.ConcreteCategory
CategoryTheory.Limits.Concrete.widePullback_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type (max v w)}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {B : C}
  {ι : Type w} {X : ι → C} (f : (j : ι) → X j ⟶ B) [inst_3 : CategoryTheory.Limits.HasWidePullback B X f]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.WidePullbackShape.wideCospan B X f)
      (CategoryTheory.forget C)]
  (x y : CategoryTheory.ToType (CategoryTheory.Limits.widePullback B X f)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.base f)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.base f)) y →
    (∀ (j : ι),
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) x =
          (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.WidePullback.π f j)) y) →
      x = y
-- Mathlib.RingTheory.AdicCompletion.Functoriality
/-- If `ι` is finite, `pi` is a linear equiv.  -/
AdicCompletion.piEquivOfFintype : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      {ι : Type u_6} →
        (M : ι → Type u_7) →
          [inst_1 : (i : ι) → AddCommGroup (M i)] →
            [inst_2 : (i : ι) → Module R (M i)] →
              [DecidableEq ι] →
                [Fintype ι] → AdicCompletion I ((j : ι) → M j) ≃ₗ[AdicCompletion I R] (j : ι) → AdicCompletion I (M j)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The augmented simplicial object that is deduced from a simplicial object and
a terminal object.  -/
CategoryTheory.SimplicialObject.augmentOfIsTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.SimplicialObject C →
      {T : C} → CategoryTheory.Limits.IsTerminal T → CategoryTheory.SimplicialObject.Augmented C
-- Mathlib.Tactic.DeriveEncodable
/-- The deriving handler for the `Encodable` class.
Handles non-nested non-reflexive inductive types.
They can be mutual too — in that case, there is an optimization to re-use all the generated
functions and proofs.
 -/
Mathlib.Deriving.Encodable.mkEncodableInstance : Array Lean.Name → Lean.Elab.Command.CommandElabM Bool
-- Batteries.Data.Array.Scan
Array.scanl_singleton : ∀ {β : Type u_1} {α : Type u_2} {init : β} {a : α} {f : β → α → β}, Array.scanl f init #[a] = #[init, f init a]
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.instNontriviallyNormedField : {p : ℕ} → [hp : Fact (Nat.Prime p)] → NontriviallyNormedField ℚ_[p]
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.proj_surjOn_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) [Nonempty F], Set.SurjOn proj e.source e.baseSet
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.mem_toArray_iff_get?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulBEq α],
  (↑m).WF →
    ∀ {k : α} {v : β}, (k, v) ∈ Std.DHashMap.Raw.Const.toArray ↑m ↔ Std.DHashMap.Internal.Raw₀.Const.get? m k = some v
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.refl_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.Precylinder X) {Y : C}
  (f : X ⟶ Y), (HomotopicalAlgebra.Precylinder.LeftHomotopy.refl P f).h = CategoryTheory.CategoryStruct.comp P.π f
-- Mathlib.Order.WellFounded
WellFounded.prop_min : ∀ {α : Type u_1} {r : α → α → Prop} (H : WellFounded r) {p : α → Prop} (h : ∃ a, p a), p (H.min {a | p a} h)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- Pushforward commutes with `SheafOfModules.forgetToSheafModuleCat`  -/
SheafOfModules.pushforwardCompForgetToSheafModuleCat : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : 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_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      (X : Cᵒᵖ) →
                        (hX : CategoryTheory.Limits.IsInitial X) →
                          (hX' : CategoryTheory.Limits.IsInitial (F.op.obj X)) →
                            (SheafOfModules.pushforward φ).comp (SheafOfModules.forgetToSheafModuleCat S X hX) ≅
                              (SheafOfModules.forgetToSheafModuleCat R (F.op.obj X) hX').comp
                                ((CategoryTheory.sheafCompose K
                                      (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X)))).comp
                                  (F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.class : Lean.Lsp.SemanticTokenType
-- Mathlib.RingTheory.Derivation.DifferentialRing
instDifferentialAlgebra : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : Differential A], DifferentialAlgebra A A
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.conjTranspose_circulant : ∀ {α : Type u_1} {n : Type u_3} [inst : Star α] [inst_1 : SubtractionMonoid n] (v : n → α),
  (Matrix.circulant v).conjTranspose = Matrix.circulant (star fun i => v (-i))
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_coe_le_of_lintegral_coe_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → NNReal} {b : NNReal},
  ∫⁻ (a : α), ↑(f a) ∂μ ≤ ↑b → ∫ (a : α), ↑(f a) ∂μ ≤ ↑b
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.eq_of_boxes_subset_iUnion_superset : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.Prepartition I},
  π₁.boxes ⊆ π₂.boxes → π₂.iUnion ⊆ π₁.iUnion → π₁ = π₂
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
ArithmeticFunction.carmichael_dvd : ∀ {a b : ℕ}, a ∣ b → ArithmeticFunction.carmichael a ∣ ArithmeticFunction.carmichael b
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.trans_map : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] {i j : 𝒰.I₀} (hij : i ⟶ j),
  CategoryTheory.CategoryStruct.comp (𝒰.trans hij) (𝒰.f j) = 𝒰.f i
-- Mathlib.Algebra.BigOperators.Intervals
/-- The two ways of summing over `(i, j)` in the range `a ≤ i ≤ j < b` are equal.  -/
Finset.sum_Ico_Ico_comm : ∀ {M : Type u_4} [inst : AddCommMonoid M] (a b : ℕ) (f : ℕ → ℕ → M),
  ∑ i ∈ Finset.Ico a b, ∑ j ∈ Finset.Ico i b, f i j = ∑ j ∈ Finset.Ico a b, ∑ i ∈ Finset.Ico a (j + 1), f i j
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative_subst : ∀ {R : Type u_1} [inst : CommRing R] {f g : PowerSeries R},
  PowerSeries.HasSubst g →
    (PowerSeries.derivative R) (PowerSeries.subst g f) =
      PowerSeries.subst g ((PowerSeries.derivative R) f) * (PowerSeries.derivative R) g
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.extendWith_single_zero : ∀ {ι : Type u} {α : Option ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : Option ι) → Zero (α i)] (i : ι)
  (x : α (some i)), (DFinsupp.extendWith 0 fun₀ | i => x) = fun₀ | some i => x
-- Init.Data.Int.Lemmas
Int.sub_mul : ∀ (a b c : ℤ), (a - b) * c = a * c - b * c
-- Mathlib.RingTheory.Ideal.IsAugmentation
/-- An ideal `I` of an `R`-algebra `A` is an augmentation ideal
if its underlying module is a complement to `1 : Submodule R A`.  -/
Ideal.IsAugmentation : (R : Type u_1) → [inst : CommSemiring R] → {A : Type u_2} → [inst_1 : Semiring A] → [Algebra R A] → Ideal A → Prop
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.infer.sizeOf_spec : sizeOf Lean.Meta.Grind.AttrKind.infer = 1
-- Mathlib.Algebra.Order.Hom.Basic
/-- The argument is one if its image under the map is zero.  -/
GroupNormClass.eq_one_of_map_eq_zero : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Group α} {inst_1 : AddCommMonoid β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : GroupNormClass F α β] (f : F) {a : α}, f a = 0 → a = 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval_extract : ∀ {assign : Std.Tactic.BVDecide.BVExpr.Assignment} {start len a : ℕ} {expr : Std.Tactic.BVDecide.BVExpr a},
  Std.Tactic.BVDecide.BVExpr.eval assign (Std.Tactic.BVDecide.BVExpr.extract start len expr) =
    BitVec.extractLsb' start len (Std.Tactic.BVDecide.BVExpr.eval assign expr)
-- Mathlib.Analysis.Convex.Quasiconvex
/-- A function is quasiconvex if all its sublevels are convex.
This means that, for all `r`, `{x ∈ s | f x ≤ r}` is `𝕜`-convex.  -/
QuasiconvexOn : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {β : Type u_3} → [Semiring 𝕜] → [PartialOrder 𝕜] → [AddCommMonoid E] → [LE β] → [SMul 𝕜 E] → Set E → (E → β) → Prop
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.AreEqualizedByLocalization.map_eq : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C} {f g : X ⟶ Y},
  CategoryTheory.AreEqualizedByLocalization W f g →
    ∀ (L : CategoryTheory.Functor C D) [L.IsLocalization W], L.map f = L.map g
-- Mathlib.Data.Finset.Lattice.Basic
Finset.union_subset_right : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, s ∪ t ⊆ u → t ⊆ u
-- Std.Time.DateTime.PlainDateTime
/-- Converts a `WallTime` to a `PlainDate`.
 -/
Std.Time.PlainDate.ofWallTime : Std.Time.WallTime → Std.Time.PlainDate
-- Mathlib.RingTheory.Morita.Basic
MoritaEquivalence.mk.sizeOf_spec : ∀ {R : Type u₀} [inst : CommSemiring R] {A : Type u₁} [inst_1 : Ring A] [inst_2 : Algebra R A] {B : Type u₂}
  [inst_3 : Ring B] [inst_4 : Algebra R B] [inst_5 : SizeOf R] [inst_6 : SizeOf A] [inst_7 : SizeOf B]
  (eqv : ModuleCat A ≌ ModuleCat B)
  (linear : autoParam (CategoryTheory.Functor.Linear R eqv.functor) MoritaEquivalence.linear._autoParam),
  sizeOf { eqv := eqv, linear := linear } = 1 + sizeOf eqv + sizeOf linear
-- Mathlib.RingTheory.Smooth.Local
/-- The **Jacobian criterion** for smoothness of local algebras.
Suppose `S` is a local `R`-algebra, and `0 → I → P → S → 0` is a presentation such that
`P` is formally-smooth over `R`, `Ω[P⁄R]` is finite free over `P`,
(typically satisfied when `P` is the localization of a polynomial ring of finite type)
and `I` is finitely generated.
Then `S` is formally smooth iff `k ⊗ₛ I → k ⊗ₚ Ω[P/R]` is injective,
where `k` any field extension of the residue field of `S`.
 -/
Algebra.FormallySmooth.iff_injective_cotangentComplexBaseChange : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : IsLocalRing S]
  [inst_3 : Algebra R S] (P : Type u_3) (K : Type u_4) [inst_4 : Field K] [inst_5 : CommRing P] [inst_6 : Algebra R P]
  [inst_7 : Algebra P S] [IsScalarTower R P S] [inst_9 : Algebra S K] [inst_10 : Algebra P K]
  [inst_11 : IsScalarTower P S K] [Algebra.FormallySmooth R P] [Module.Free P Ω[P⁄R]] [Module.Finite P Ω[P⁄R]],
  Function.Surjective ⇑(algebraMap P S) →
    (RingHom.ker (algebraMap P S)).FG →
      IsLocalRing.maximalIdeal S ≤ RingHom.ker (algebraMap S K) →
        (Algebra.FormallySmooth R S ↔ Function.Injective ⇑(KaehlerDifferential.cotangentComplexBaseChange R S P K))
-- Mathlib.Analysis.Normed.Operator.Banach
/-- The **closed graph theorem** : a linear map between two Banach spaces whose graph is closed
is continuous.  -/
LinearMap.continuous_of_isClosed_graph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [CompleteSpace F] (g : E →ₗ[𝕜] F), IsClosed ↑g.graph → Continuous ⇑g
-- Mathlib.Analysis.Normed.Field.WithAbs
WithAbs.instIsSeparable_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Field R] {T : Type u_3}
  [inst_3 : Field T] (v : AbsoluteValue R S) [inst_4 : Algebra T R] [Algebra.IsSeparable T R],
  Algebra.IsSeparable T (WithAbs v)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sub_lt : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R} {g : Γ₀}, v x < g → v y < g → v (x - y) < g
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)} (I : Type v)
  [ℐ : CategoryTheory.SmallCategory I] [hI : CategoryTheory.IsFiltered I] (F : CategoryTheory.Functor I C)
  (ι : F.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A)
  (isColimit : CategoryTheory.Limits.IsColimit { pt := A, ι := ι }) (I_1 : Type v)
  (ℐ_1 : CategoryTheory.SmallCategory I_1) (hI_1 : CategoryTheory.IsFiltered I_1) (F_1 : CategoryTheory.Functor I_1 C)
  (ι_1 : F_1.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I_1).obj A)
  (isColimit_1 : CategoryTheory.Limits.IsColimit { pt := A, ι := ι_1 }),
  ({ I := I, ℐ := ℐ, hI := hI, F := F, ι := ι, isColimit := isColimit } =
      { I := I_1, ℐ := ℐ_1, hI := hI_1, F := F_1, ι := ι_1, isColimit := isColimit_1 }) =
    (I = I_1 ∧ ℐ ≍ ℐ_1 ∧ F ≍ F_1 ∧ ι ≍ ι_1 ∧ isColimit ≍ isColimit_1)
-- Mathlib.Data.Num.Prime
PosNum.minFac.eq_3 : ∀ (n : PosNum), n.bit1.minFac = n.bit1.minFacAux (↑n) 1
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_lt_of_lt_mul : ∀ {a b c : ℤ}, 0 < c → a < b * c → a / c < b
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.submatrix_id_id : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (A : Matrix m n α), A.submatrix id id = A
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.instDecidableEqCode.decEq : (x x_1 : Turing.ToPartrec.Code) → Decidable (x = x_1)
-- Mathlib.Topology.Sets.CompactOpenCovered
IsCompactOpenCovered.of_finite_of_isSpectralMap : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  [Finite ι] [inst_2 : TopologicalSpace S],
  (∀ (i : ι), IsSpectralMap (f i)) →
    ∀ {U : Set S}, (∀ x ∈ U, ∃ i, x ∈ Set.range (f i)) → IsOpen U → IsCompact U → IsCompactOpenCovered f U
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.NormalExpr.zero.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Mathlib.Tactic.Abel.NormalExpr.zero e) = 1 + sizeOf e