mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The directed cover of a scheme indexed by `X.AffineZariskiSite`.
Note the related `Scheme.directedAffineCover`, which has the same (defeq) cover but a different
category instance on the indices.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover : (X : AlgebraicGeometry.Scheme) → X.OpenCover
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.fst_decompAffineEquiv : ∀ (R : Type u_1) (S : Type u_2) (V : Type u_3) {W : Type u_4} (Q : Type u_5) [inst : Ring S] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : TopologicalSpace V] [inst_5 : IsTopologicalAddGroup V]
  [inst_6 : AddCommGroup W] [inst_7 : Module R W] [inst_8 : TopologicalSpace W] [inst_9 : Module S W]
  [inst_10 : SMulCommClass R S W] [inst_11 : ContinuousConstSMul S W] [inst_12 : AddTorsor W Q]
  [inst_13 : TopologicalSpace Q] [inst_14 : IsTopologicalAddGroup W] [inst_15 : IsTopologicalAddTorsor Q]
  (f : V →ᴬ[R] Q), ((ContinuousAffineMap.decompAffineEquiv R S V Q) f).1 = f 0
-- Mathlib.NumberTheory.NumberField.ClassNumber
/-- Let `K` be a number field such that `K/ℚ` is Galois and let `M K` be the Minkowski bound of `K`.
To show that `𝓞 K` is a PID it is enough to show that, for all (natural) primes
`p ∈ Finset.Icc 1 ⌊(M K)⌋₊`, there is an ideal `P` above `p` such that
either `⌊(M K)⌋₊ < p ^ (span ({p}).inertiaDeg P)` or `P` is principal. This is the standard
technique to prove that `𝓞 K` is principal in the Galois case, see [marcus1977number], discussion
after Theorem 37.

The way this theorem should be used is to first compute `⌊(M K)⌋₊` and then to use `fin_cases`
to deal with the finite number of primes `p` in the interval.  -/
RingOfIntegers.isPrincipalIdealRing_of_isPrincipal_of_lt_or_isPrincipal_of_mem_primesOver_of_mem_Icc : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] [IsGalois ℚ K],
  (∀
      p ∈
        Finset.Icc 1
          ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
              (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
                √|↑(NumberField.discr K)|)⌋₊,
      Nat.Prime p →
        ∃ P ∈ (Ideal.span {↑p}).primesOver (NumberField.RingOfIntegers K),
          ⌊(4 / Real.pi) ^ NumberField.InfinitePlace.nrComplexPlaces K *
                  (↑(Module.finrank ℚ K).factorial / ↑(Module.finrank ℚ K) ^ Module.finrank ℚ K *
                    √|↑(NumberField.discr K)|)⌋₊ <
              p ^ P.inertiaDeg ℤ ∨
            Submodule.IsPrincipal P) →
    IsPrincipalIdealRing (NumberField.RingOfIntegers K)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_apply_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) {x : β} {y : α},
  e.symm x = y ↔ x = e y
-- Init.Data.List.Sublist
List.cons_subset_cons : ∀ {α : Type u_1} {l₁ l₂ : List α} (a : α), l₁ ⊆ l₂ → a :: l₁ ⊆ a :: l₂
-- Init.Data.Rat.Lemmas
Rat.natCast_le_natCast : ∀ {a b : ℕ}, ↑a ≤ ↑b ↔ a ≤ b
-- Mathlib.Data.List.Basic
List.insert_pos : ∀ {α : Type u} [inst : DecidableEq α] {x : α} {l : List α}, x ∈ l → insert x l = l
-- Mathlib.Order.LatticeIntervals
Set.Ici.distribLattice : {α : Type u_1} → [inst : DistribLattice α] → {a : α} → DistribLattice ↑(Set.Ici a)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify
PresheafOfModules.Sheafify.instUniqueSMulCandidate : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} →
        {R : CategoryTheory.Sheaf J RingCat} →
          (α : R₀ ⟶ R.obj) →
            [CategoryTheory.Presheaf.IsLocallyInjective J α] →
              [CategoryTheory.Presheaf.IsLocallySurjective J α] →
                {M₀ : PresheafOfModules R₀} →
                  {A : CategoryTheory.Sheaf J AddCommGrpCat} →
                    (φ : M₀.presheaf ⟶ A.obj) →
                      [CategoryTheory.Presheaf.IsLocallyInjective J φ] →
                        [CategoryTheory.Presheaf.IsLocallySurjective J φ] →
                          {X : Cᵒᵖ} →
                            (r : ↑(R.obj.obj X)) →
                              (m : ↑(A.obj.obj X)) → Unique (PresheafOfModules.Sheafify.SMulCandidate α φ r m)
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.link2.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3)
  (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (h_1 :
    (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (szr : ℕ) →
      (k'' : α) →
        (v'' : β k'') →
          (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) →
              Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' →
                motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') hr),
  (match hr' : Std.DTreeMap.Internal.Impl.leaf, hr with
    | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr hr'
    | Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'', hr => h_2 szr k'' v'' l'' r'' hr hr') =
    h_1 hr ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
/-- The Weierstrass curve in projective coordinates mapped over a ring homomorphism `f : R →+* S`.
 -/
WeierstrassCurve.Projective.map : {R : Type r} →
  [inst : CommRing R] →
    WeierstrassCurve.Projective R → {S : Type s} → [inst_1 : CommRing S] → (R →+* S) → WeierstrassCurve.Projective S
-- Lean.Message
Lean.BaseMessage.pos : {α : Type u} → Lean.BaseMessage α → Lean.Position
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.AttributeEntry.isBuiltin : {γ : Type} → Lean.KeyedDeclsAttribute.AttributeEntry γ → Bool
-- Mathlib.RingTheory.Localization.Defs
/-- Given a localization map `f : R →+* S` for a submonoid `M ⊆ R` and a map of `CommSemiring`s
`g : R →* P` such that `g y` is invertible for all `y : M`, the homomorphism induced from
`S` to `P` maps `f x * (f y)⁻¹` to `g x * (g y)⁻¹` for all `x : R, y ∈ M`.  -/
IsLocalization.lift_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] {P : Type u_3} [inst_3 : CommSemiring P] [inst_4 : IsLocalization M S] {g : R →+* P}
  (hg : ∀ (y : ↥M), IsUnit (g ↑y)) (x : R) (y : ↥M),
  (IsLocalization.lift hg) (IsLocalization.mk' S x y) = g x * ↑((IsUnit.liftRight ((↑g).domRestrict M) hg) y)⁻¹
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_div : ∀ {a b : UInt32}, (a / b).toBitVec = a.toBitVec / b.toBitVec
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_span_le_ncard_of_finite : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  s.Finite → (Submodule.span R s).spanFinrank ≤ s.ncard
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.length_alternatingWord : ∀ {B : Type u_1} (i i' : B) (m : ℕ), (CoxeterSystem.alternatingWord i i' m).length = m
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} {fallback : β a}, m.contains a = false → m.getD a fallback = fallback
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.instMulAction : {ι : Type v} →
  {M₁ : ι → Type w₁} →
    {M₂ : Type w₂} →
      [inst : (i : ι) → AddCommMonoid (M₁ i)] →
        [inst_1 : AddCommMonoid M₂] →
          [inst_2 : (i : ι) → TopologicalSpace (M₁ i)] →
            [inst_3 : TopologicalSpace M₂] →
              {R' : Type u_1} →
                {A : Type u_2} →
                  [inst_4 : Monoid R'] →
                    [inst_5 : Semiring A] →
                      [inst_6 : (i : ι) → Module A (M₁ i)] →
                        [inst_7 : Module A M₂] →
                          [inst_8 : DistribMulAction R' M₂] →
                            [ContinuousConstSMul R' M₂] →
                              [SMulCommClass A R' M₂] → MulAction R' (ContinuousMultilinearMap A M₁ M₂)
-- Mathlib.Data.PEquiv
PEquiv.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (toFun : α → Option β) (invFun : β → Option α)
  (inv : ∀ (a : α) (b : β), invFun b = some a ↔ toFun a = some b),
  sizeOf { toFun := toFun, invFun := invFun, inv := inv } = 1
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap`.

---

The induced order-preserving function from a linear ordered field to a conditionally complete
linear ordered field, defined by taking the Sup in the codomain of all the rationals less than the
input.  -/
LinearOrderedField.inducedMap : (α : Type u_2) → (β : Type u_3) → [Field α] → [LinearOrder α] → [Field β] → [ConditionallyCompleteLinearOrder β] → α → β
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The sum over the values of a nontrivial additive character vanishes if the target ring
is a domain.  -/
AddChar.sum_eq_zero_of_ne_one : ∀ {R : Type u_1} [inst : AddGroup R] [inst_1 : Fintype R] {R' : Type u_2} [inst_2 : CommRing R'] [IsDomain R']
  {ψ : AddChar R R'}, ψ ≠ 1 → ∑ a, ψ a = 0
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_const_of_zero : ∀ {n : SimplexCategory} (f : { len := 0 } ⟶ n), f = { len := 0 }.const n ((SimplexCategory.Hom.toOrderHom f) 0)
-- Mathlib.Algebra.Group.TypeTags.Basic
instDecidableEqMultiplicative : {α : Type u} → [h : DecidableEq α] → DecidableEq (Multiplicative α)
-- Init.Grind.Norm
Lean.Grind.not_and : ∀ (p q : Prop), (¬(p ∧ q)) = (¬p ∨ ¬q)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.le_sup'_of_le : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (f : β → α) {a : α} {b : β} (hb : b ∈ s),
  a ≤ f b → a ≤ s.sup' ⋯ f
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField : ∀ {K : Type u_1} {Γ₀ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [inst_2 : Valued K Γ₀]
  [Valued.v.RankOne],
  CompactSpace ↥(Valued.integer K) ↔
    CompleteSpace ↥(Valued.integer K) ∧ IsDiscreteValuationRing ↥(Valued.integer K) ∧ Finite (Valued.ResidueField K)
-- Init.Data.Vector.Lemmas
Vector.anyM_congr : ∀ {m : Type → Type u_1} {α : Type u_2} {n : ℕ} [inst : Monad m] {xs ys : Vector α n},
  xs = ys → ∀ {p q : α → m Bool}, (∀ (a : α), p a = q a) → Vector.anyM p xs = Vector.anyM q ys
-- Init.Data.List.Lemmas
List.eraseDups_cons : ∀ {α : Type u_1} [inst : BEq α] {a : α} {as : List α},
  (a :: as).eraseDups = a :: (List.filter (fun b => !b == a) as).eraseDups
-- Init.Data.String.Defs
_private.Init.Data.String.Defs.0.String.push.match_1.splitter : (motive : String → Char → Sort u_1) →
  (x : String) →
    (x_1 : Char) →
      ((b : ByteArray) → (h : b.IsValidUTF8) → (c : Char) → motive { toByteArray := b, isValidUTF8 := h } c) →
        motive x x_1
-- Mathlib.RingTheory.Coalgebra.Hom
Coalgebra.counitCoalgHom_apply : ∀ (R : Type u) (A : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (x : A), (Coalgebra.counitCoalgHom R A) x = CoalgebraStruct.counit x
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.disjWithin_mono : ∀ {a b c d : ℝ},
  Set.uIcc c d ⊆ Set.uIcc a b →
    AbsolutelyContinuousOnInterval.disjWithin c d ⊆ AbsolutelyContinuousOnInterval.disjWithin a b
-- Std.Time.Date.Unit.Day
Std.Time.Day.Ordinal.instTransOrdOfYear : ∀ {leap : Bool}, Std.TransOrd (Std.Time.Day.Ordinal.OfYear leap)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.exists_eq_pow_mul_of_is_compact_of_quasi_separated_space_aux_aux : ∀ {X : TopCat} (F : TopCat.Presheaf CommRingCat X) {U₁ U₂ U₃ U₄ U₅ U₆ U₇ : TopologicalSpace.Opens ↑X} {n₁ n₂ : ℕ}
  {y₁ : ↑(F.obj (Opposite.op U₁))} {y₂ : ↑(F.obj (Opposite.op U₂))} {f : ↑(F.obj (Opposite.op (U₁ ⊔ U₂)))}
  {x : ↑(F.obj (Opposite.op U₃))} (h₄₁ : U₄ ≤ U₁) (h₄₂ : U₄ ≤ U₂) (h₅₁ : U₅ ≤ U₁) (h₅₃ : U₅ ≤ U₃) (h₆₂ : U₆ ≤ U₂)
  (h₆₃ : U₆ ≤ U₃) (h₇₄ : U₇ ≤ U₄),
  U₇ ≤ U₅ →
    U₇ ≤ U₆ →
      TopCat.Presheaf.restrictOpen y₁ U₅ h₅₁ =
          TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯) U₅ h₅₁ ^ n₁ *
            TopCat.Presheaf.restrictOpen x U₅ h₅₃ →
        TopCat.Presheaf.restrictOpen y₂ U₆ h₆₂ =
            TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯) U₆ h₆₂ ^ n₂ *
              TopCat.Presheaf.restrictOpen x U₆ h₆₃ →
          TopCat.Presheaf.restrictOpen
              (TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₁ ⋯ ^ n₂ * y₁) U₄ h₄₁) U₇ h₇₄ =
            TopCat.Presheaf.restrictOpen
              (TopCat.Presheaf.restrictOpen (TopCat.Presheaf.restrictOpen f U₂ ⋯ ^ n₁ * y₂) U₄ h₄₂) U₇ h₇₄
-- Aesop.RuleSet
/-- The rule set used by an Aesop tactic call. A local rule set is produced by
combining several global rule sets and possibly adding or erasing some
individual rules.
 -/
Aesop.LocalRuleSet : Type
-- Lean.Meta.Match.MatchEqsExt
Lean.Meta.Match.getEquationsFor : Lean.Name → Lean.MetaM Lean.Meta.Match.MatchEqns
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_restr : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : SeminormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] {k n : ℕ}
  (f : G [×n]→L[𝕜] G') (s : Finset (Fin n)) (hk : s.card = k) (z : G), ‖f.restr s hk z‖ ≤ ‖f‖ * ‖z‖ ^ (n - k)
-- Mathlib.Data.Finsupp.Fin
Finsupp.cons_zero : ∀ {n : ℕ} {M : Type u_1} [inst : Zero M] (y : M) (s : Fin n →₀ M), (Finsupp.cons y s) 0 = y
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- If the extended distance between consecutive points of a sequence is estimated
by a summable series of `NNReal`s, then the original sequence is a Cauchy sequence.  -/
cauchySeq_of_edist_le_of_summable : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {f : ℕ → α} (d : ℕ → NNReal),
  (∀ (n : ℕ), edist (f n) (f n.succ) ≤ ↑(d n)) → Summable d → CauchySeq f
-- Mathlib.RingTheory.Perfection
/-- `Perfection R p` as a semiring of `ℕ → R`.  -/
Perfection.subring : (R : Type u_1) → [inst : CommRing R] → (p : ℕ) → [hp : Fact (Nat.Prime p)] → [CharP R p] → Subring (ℕ → R)
-- Mathlib.Topology.LocallyConstant.Basic
/-- As a shorthand, `LocallyConstant.toContinuousMap` is available as a coercion  -/
LocallyConstant.instCoeContinuousMap : {X : Type u_1} →
  {Y : Type u_2} → [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → Coe (LocallyConstant X Y) C(X, Y)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, (t₁ ∪ t₂).contains k = (t₁.contains k || t₂.contains k)
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Nat.Subtype.right_inverse_aux : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s] (n : ℕ),
  Nat.Subtype.toFunAux✝ (Nat.Subtype.ofNat s n) = n
-- Mathlib.GroupTheory.Focal
/-- The transfer homomorphism `V : G → H/H*` from `G` the abelian quotient `H/H*`.  -/
Subgroup.transferFocal : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → [H.FiniteIndex] → G →* ↥H ⧸ H.focalSubgroupOf
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.H1Cotangent.val_add : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x y : P.H1Cotangent), ↑(x + y) = ↑x + ↑y
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.Perm.prod_eq : ∀ {M : Type u_4} [inst : CommMonoid M] {l₁ l₂ : List M}, l₁.Perm l₂ → l₁.prod = l₂.prod
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.targetAffineLocally.eq_1 : ∀ (P : AlgebraicGeometry.AffineTargetMorphismProperty) {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.targetAffineLocally P f = ∀ (U : ↑Y.affineOpens), P (f ∣_ ↑U)
-- Mathlib.Algebra.Notation.Indicator
Set.mulSupport_mulIndicator : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M},
  Function.mulSupport (s.mulIndicator f) = s ∩ Function.mulSupport f
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instSMulCommClassForall_2 : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} {N : Type u_4} [inst : SMul M α] [inst_1 : SMul N α]
  [SMulCommClass M N α], SMulCommClass Mᵈᵐᵃ Nᵈᵐᵃ (α → β)
-- Mathlib.CategoryTheory.Sites.Closed
/-- The presheaf of `J`-closed sieves is a `J`-sheaf.
The proof of this is adapted from [MM92], Chapter III, Section 7, Lemma 1.
 -/
CategoryTheory.classifier_isSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C),
  CategoryTheory.Presieve.IsSheaf J₁ (CategoryTheory.Functor.closedSieves J₁).toFunctor
-- Init.Data.Nat.Lemmas
Nat.succ_add_eq_add_succ : ∀ (a b : ℕ), a.succ + b = a + b.succ
-- Mathlib.Combinatorics.SetFamily.Compression.UV
UV.le_of_mem_compression_of_notMem : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α], a ∈ UV.compression u v s → a ∉ s → u ≤ a
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.div_iInter₂_subset : ∀ {α : Type u_2} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : Div α] (s : Set α) (t : (i : ι) → κ i → Set α),
  s / ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s / t i j
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instAddCommGroup : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddCommGroup Y] → AddCommGroup (Function.locallyFinsuppWithin U Y)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
eventually_enorm_mfderiv_extChartAt_lt : ∀ {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]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] (x : M),
  ∃ C > 0, ∀ᶠ (y : M) in nhds x, ‖mfderiv% ↑(extChartAt I x) y‖ₑ < ↑C
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.HoldsForLocalization.holdsForLocalizationAway : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.HoldsForLocalization fun {R S} [CommRing R] [CommRing S] => P) →
    RingHom.HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.Topology.Compactness.CompactlyCoherentSpace
/-- For a map `f : X → Y` of topological spaces, `CompactCoherentification.map f` is the
corresponding map between the compact coherentifications of `X` and `Y`.  -/
CompactCoherentification.map : {X : Type u_1} → {Y : Type u_2} → (X → Y) → CompactCoherentification X → CompactCoherentification Y
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of a magma is isomorphic to the center of its opposite.  -/
Subsemigroup.centerToMulOpposite : {M : Type u_2} → [inst : Mul M] → ↥(Subsemigroup.center M) ≃* ↥(Subsemigroup.center Mᵐᵒᵖ)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- For every nonzero ideal `I` of `v`, there are finitely many maximal ideals `v` such that
`v^-(val_v(I))` is not the unit ideal.  -/
Ideal.hasFiniteMulSupport_inv : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDedekindDomain R] {I : Ideal R},
  I ≠ 0 →
    Function.HasFiniteMulSupport fun v => ↑v.asIdeal ^ (-↑((Associates.mk v.asIdeal).count (Associates.mk I).factors))
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivWithinAt.clm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {x : 𝕜} {s : Set 𝕜} {G : Type u_2} [inst_3 : NormedAddCommGroup G]
  [inst_4 : NormedSpace 𝕜 G] {c : 𝕜 → F →L[𝕜] G} {c' : F →L[𝕜] G} {u : 𝕜 → F} {u' : F},
  HasDerivWithinAt c c' s x →
    HasDerivWithinAt u u' s x → HasDerivWithinAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') s x
-- Mathlib.Order.BooleanAlgebra.Set
Set.inter_sdiff_self : ∀ {α : Type u_1} (a b : Set α), a ∩ (b \ a) = ∅
-- Mathlib.Analysis.RCLike.Basic
RCLike.normSq_pos : ∀ {K : Type u_1} [inst : RCLike K] {z : K}, 0 < RCLike.normSq z ↔ z ≠ 0
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.lowerBoundP?_eq_findP? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBSet α cmp} {cut : α → Ordering},
  t.findP? cut = some x → t.lowerBoundP? cut = some x
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- Typeclass for purely inseparable field extensions: an algebraic extension `E / F` is purely
inseparable if and only if the minimal polynomial of every element of `E ∖ F` is not separable.

We define this for general (commutative) rings and only assume `F` and `E` are fields
if this is needed for a proof.  -/
IsPurelyInseparable : (F : Type u_1) → (E : Type u_2) → [inst : CommRing F] → [inst_1 : Ring E] → [Algebra F E] → Prop
-- Init.CbvSimproc
Lean.Parser.cbvSimprocPattern : Lean.ParserDescr
-- Plausible.Random
/-- A monad to generate random objects using the generator type `StdGen`.  -/
Plausible.Rand : Type u_1 → Type u_1
-- Std.Data.TreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.Raw.get? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → Option β
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.shortComplexOfDistTriangle_X₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles),
  (CategoryTheory.Pretriangulated.shortComplexOfDistTriangle T hT).X₃ = T.obj₃
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionIdentifier.fvar : Lean.FVarId → Lean.Lsp.CompletionIdentifier
-- Mathlib.CategoryTheory.Whiskering
/-- The "postcomposition" with a functor `E ⥤ E'` gives a functor
`(E ⥤ E') ⥤ (C₁ ⥤ C₂ ⥤ C₃ ⥤ E) ⥤ C₁ ⥤ C₂ ⥤ C₃ ⥤ E'`.  -/
CategoryTheory.Functor.postcompose₃ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
            {E : Type u_7} →
              [inst_3 : CategoryTheory.Category.{v_7, u_7} E] →
                {E' : Type u_8} →
                  [inst_4 : CategoryTheory.Category.{v_8, u_8} E'] →
                    CategoryTheory.Functor (CategoryTheory.Functor E E')
                      (CategoryTheory.Functor
                        (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E)))
                        (CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E'))))
-- Mathlib.Data.Set.Function
Set.injOn_of_subsingleton : ∀ {α : Type u_1} {β : Type u_2} [Subsingleton α] (f : α → β) (s : Set α), Set.InjOn f s
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.splitFirstHypothesisS?.tacticBuilder : Lean.MVarId → Array Lean.MVarId × Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_of_isPrincipal_mul`. -/
Ordinal.principal_add_of_principal_mul : ∀ {o : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) o → o ≠ 2 → Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) o
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitUpper.eq_1 : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (i : ι) (x : ℝ),
  I.splitUpper i x = BoxIntegral.Box.mk' (Function.update I.lower i (max x (I.lower i))) I.upper