mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- Auxiliary result for the grid-lines lemma.  Given a nonnegative function on a finitary product
type indexed by `ι`, and a set `s` in `ι`, consider partially integrating over the variables in
`sᶜ` and performing the "grid-lines operation" (see `GridLines.T`) to the resulting function in the
variables `s`.  This theorem states that this operation decreases as the number of grid-lines taken
increases.  -/
MeasureTheory.GridLines.T_lmarginal_antitone : ∀ {ι : Type u_1} {A : ι → Type u_2} [inst : (i : ι) → MeasurableSpace (A i)] (μ : (i : ι) → MeasureTheory.Measure (A i))
  [inst_1 : DecidableEq ι] {p : ℝ} [inst_2 : Fintype ι] [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)],
  0 ≤ p →
    (↑(Fintype.card ι) - 1) * p ≤ 1 →
      ∀ {f : ((i : ι) → A i) → ENNReal},
        Measurable f → Antitone fun s => MeasureTheory.GridLines.T μ p (∫⋯∫⁻_sᶜ, f ∂μ) s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [inst : Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          ∀ {h : k' ∈ Std.ExtDTreeMap.Const.ofList l cmp},
            Std.ExtDTreeMap.Const.get (Std.ExtDTreeMap.Const.ofList l cmp) k' h = v
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValueCast? k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      (Std.Internal.List.getValueCast? k l).bind (f k)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_self_eq_one₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀}, a / a = 1 ↔ a ≠ 0
-- Mathlib.NumberTheory.Ostrowski
_private.Mathlib.NumberTheory.Ostrowski.0.list_mul_sum : ∀ {R : Type u_1} [inst : Semiring R] {T : Type u_2} (l : List T) (y x : R),
  (List.mapIdx (fun i x_1 => x * y ^ i) l).sum = x * (List.mapIdx (fun i x => y ^ i) l).sum
-- Init.Data.Option.Lemmas
Option.wellFounded_lt : ∀ {α : Type u_1} {rel : α → α → Prop}, WellFounded rel → WellFounded (Option.lt rel)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.containsKey.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a : α), Std.Internal.List.containsKey a [] = false
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_zero : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7}, ↑0 = 0
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.X_pow_card_pow_sub_X_natDegree_eq : ∀ (K' : Type u_3) [inst : Field K'] {p n : ℕ}, n ≠ 0 → 1 < p → (Polynomial.X ^ p ^ n - Polynomial.X).natDegree = p ^ n
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_image_eq_of_injOn : ∀ {α β : Type u} (f : α → β) (s : Set α), Set.InjOn f s → Cardinal.mk ↑(f '' s) = Cardinal.mk ↑s
-- Init.Data.UInt.Lemmas
BitVec.ofNat_uInt32ToNat : ∀ (n : UInt32), BitVec.ofNat 32 n.toNat = n.toBitVec
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd.eq_1 : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (s : Multiset α),
  s.gcd = Multiset.fold gcd 0 s
-- Mathlib.Order.Filter.AtTopBot.Tendsto
Filter.tendsto_atBot_atTop_of_antitone : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → (∀ (b : β), ∃ a, b ≤ f a) → Filter.Tendsto f Filter.atBot Filter.atTop
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The vector given in Euclidean space by being `a : 𝕜` at coordinate `i : ι` and `0 : 𝕜` at
all other coordinates.  -/
EuclideanSpace.single : {ι : Type u_1} → {𝕜 : Type u_3} → [RCLike 𝕜] → [DecidableEq ι] → ι → 𝕜 → EuclideanSpace 𝕜 ι
-- Mathlib.Algebra.Group.Subsemigroup.Operations
/-- Makes the identity isomorphism from a proof that two subsemigroups of a multiplicative
semigroup are equal.  -/
MulEquiv.subsemigroupCongr : {M : Type u_1} → [inst : Mul M] → {S T : Subsemigroup M} → S = T → ↥S ≃* ↥T
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
/-- Shows that the fractional parts of the stream are smaller than one.  -/
GenContFract.IntFractPair.nth_stream_fr_lt_one : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n → ifp_n.fr < 1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.comp_sub_right_iff : ∀ {ε : Type u_3} [inst : TopologicalSpace ε] [inst_1 : ENormedAddMonoid ε] {f : ℝ → ε} {a b : ℝ}
  [TopologicalSpace.PseudoMetrizableSpace ε] {c : ℝ},
  autoParam (‖f (min a b)‖ₑ ≠ ⊤) IntervalIntegrable.comp_sub_right_iff._auto_1 →
    (IntervalIntegrable (fun x => f (x - c)) MeasureTheory.volume (a + c) (b + c) ↔
      IntervalIntegrable f MeasureTheory.volume a b)
-- Lean.Parser.Basic
Lean.Parser.instBEqOrElseOnAntiquotBehavior.beq : Lean.Parser.OrElseOnAntiquotBehavior → Lean.Parser.OrElseOnAntiquotBehavior → Bool
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.restrictPreimage'_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) (s : Set B)
  [inst_3 : Nonempty (↑s → F → ↑(proj ⁻¹' s))],
  (e.restrictPreimage' s).baseSet = Subtype.val ⁻¹' e.toPretrivialization.baseSet
-- Init.Data.List.Lemmas
List.getLast?_flatMap : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β},
  (List.flatMap f l).getLast? = List.findSome? (fun a => (f a).getLast?) l.reverse
-- Mathlib.Order.Bounds.Basic
bbdAbove_range_sup_iff : ∀ {ι : Sort u_4} {α : Type u_5} [inst : SemilatticeSup α] {f g : ι → α},
  BddAbove (Set.range fun x => f x ⊔ g x) ↔ BddAbove (Set.range f) ∧ BddAbove (Set.range g)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_insertMany_empty_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] [inst : BEq α] [Std.LawfulBEqOrd α] {l : List (α × β)}
  {k fallback : α},
  (List.map Prod.fst l).contains k = false →
    (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)).getKeyD k fallback = fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.insertMany!_empty_list_singleton : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {k : α} {v : β k},
  ↑(Std.DTreeMap.Internal.Impl.empty.insertMany! [⟨k, v⟩]) =
    (Std.DTreeMap.Internal.Impl.insert k v Std.DTreeMap.Internal.Impl.empty ⋯).impl
-- Init.Grind.Norm
Lean.Grind.exists_const : ∀ (α : Sort u) [i : Nonempty α] {b : Prop}, (∃ x, b) = b
-- Mathlib.Data.Real.Basic
_private.Mathlib.Data.Real.Basic.0.Real.lt_def : ∀ (x x_1 : ℝ),
  Real.lt✝ x x_1 =
    match x, x_1 with
    | { cauchy := x }, { cauchy := y } => Quotient.liftOn₂ x y (fun x1 x2 => x1 < x2) Real.definition._proof_1✝
-- Mathlib.Topology.Order.OrderClosed
Ico_mem_nhdsGT : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α] {a b : α},
  b < a → Set.Ico b a ∈ nhdsWithin b (Set.Ioi b)
-- Mathlib.Data.Finsupp.Defs
Finsupp.instCanLift : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M],
  CanLift (α → M) (α →₀ M) DFunLike.coe fun f => (Function.support f).Finite
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
/-- Define an algebra homomorphism on a directed supremum of non-unital subalgebras by defining
it on each non-unital subalgebra, and proving that it agrees on the intersection of
non-unital subalgebras.  -/
NonUnitalSubalgebra.iSupLift : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : Module R A] →
            [inst_3 : NonUnitalNonAssocSemiring B] →
              [inst_4 : Module R B] →
                [inst_5 : IsScalarTower R A A] →
                  [inst_6 : SMulCommClass R A A] →
                    {ι : Sort u_1} →
                      [Nonempty ι] →
                        (K : ι → NonUnitalSubalgebra R A) →
                          Directed (fun x1 x2 => x1 ≤ x2) K →
                            (f : (i : ι) → ↥(K i) →ₙₐ[R] B) →
                              (∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)) →
                                (T : NonUnitalSubalgebra R A) → T = iSup K → ↥T →ₙₐ[R] B
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- The operator norm satisfies the triangle inequality.  -/
ContinuousMultilinearMap.opNorm_add_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f g : ContinuousMultilinearMap 𝕜 E G), ‖f + g‖ ≤ ‖f‖ + ‖g‖
-- Batteries.Data.List.Pairwise
List.pwFilter_idem : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} [inst : DecidableRel R],
  List.pwFilter R (List.pwFilter R l) = List.pwFilter R l
-- Lean.Setup
Lean.Plugin.mk : System.FilePath → Option String → Lean.Plugin
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
PreAbstractSimplicialComplex.instPartialOrder : (ι : Type u_1) → PartialOrder (PreAbstractSimplicialComplex ι)
-- Mathlib.Data.Num.Basic
instDecidableEqPosNum : DecidableEq PosNum
-- Lean.Elab.InfoTree.Main
Lean.Elab.ContextInfo.ppSyntax : Lean.Elab.ContextInfo → Lean.LocalContext → Lean.Syntax → IO Std.Format
-- Mathlib.Topology.Constructions
nhds_subtype_eq_comap_nhdsWithin : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X) (x : { x // x ∈ s }),
  nhds x = Filter.comap Subtype.val (nhdsWithin (↑x) s)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.decompositionMonoid_iff : ∀ {M : Type u_1} [inst : CommMonoid M], DecompositionMonoid (Associates M) ↔ DecompositionMonoid M
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence_unitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max w v))),
  (CategoryTheory.CategoryOfElements.costructuredArrowULiftYonedaEquivalence F).unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        (CategoryTheory.CategoryOfElements.isoMk
            (F.elementsMk
              (Opposite.op
                ({
                        obj := fun x =>
                          CategoryTheory.CostructuredArrow.mk
                            (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd),
                        map := fun {X Y} f => CategoryTheory.CostructuredArrow.homMk (↑(Opposite.unop f)).unop ⋯,
                        map_id := ⋯, map_comp := ⋯ }.obj
                    x).left)
              (CategoryTheory.uliftYonedaEquiv
                ({
                        obj := fun x =>
                          CategoryTheory.CostructuredArrow.mk
                            (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd),
                        map := fun {X Y} f => CategoryTheory.CostructuredArrow.homMk (↑(Opposite.unop f)).unop ⋯,
                        map_id := ⋯, map_comp := ⋯ }.obj
                    x).hom))
            (Opposite.unop x)
            (CategoryTheory.Iso.refl
              (F.elementsMk
                  (Opposite.op
                    ({
                            obj := fun x =>
                              CategoryTheory.CostructuredArrow.mk
                                (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd),
                            map := fun {X Y} f => CategoryTheory.CostructuredArrow.homMk (↑(Opposite.unop f)).unop ⋯,
                            map_id := ⋯, map_comp := ⋯ }.obj
                        x).left)
                  (CategoryTheory.uliftYonedaEquiv
                    ({
                            obj := fun x =>
                              CategoryTheory.CostructuredArrow.mk
                                (CategoryTheory.uliftYonedaEquiv.symm (Opposite.unop x).snd),
                            map := fun {X Y} f => CategoryTheory.CostructuredArrow.homMk (↑(Opposite.unop f)).unop ⋯,
                            map_id := ⋯, map_comp := ⋯ }.obj
                        x).hom)).fst)
            ⋯).op)
      ⋯
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Cell.get?.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) →
        (x = none → motive none) → ((p : (a : α) × β a) → x = some p → motive (some p)) → motive x
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_insertListConst_le : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)},
  (Std.Internal.List.insertListConst l toInsert).length ≤ l.length + toInsert.length
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.cyclesFunctor_linear : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.Limits.HasKernels C] [inst_5 : CategoryTheory.Limits.HasCokernels C],
  CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.cyclesFunctor C)
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.IsPrincipal.add_eq_right_of_le : ∀ {a b c : Ordinal.{u}}, Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) b → a < b → b ≤ c → a + c = c
-- Mathlib.RepresentationTheory.Basic
Representation.ofModule_asAlgebraHom_apply_apply : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Monoid G] (M : Type u_4) [inst_2 : AddCommMonoid M]
  [inst_3 : Module (MonoidAlgebra k G) M] (r : MonoidAlgebra k G) (m : RestrictScalars k (MonoidAlgebra k G) M),
  ((Representation.ofModule M).asAlgebraHom r) m =
    (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)
-- Mathlib.Algebra.Module.Submodule.Range
Submodule.map_comap_eq : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective τ₁₂] (f : M →ₛₗ[τ₁₂] M₂) (q : Submodule R₂ M₂),
  Submodule.map f (Submodule.comap f q) = f.range ⊓ q
-- Mathlib.Algebra.IsPrimePow
isPrimePow_def : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] (n : R), IsPrimePow n ↔ ∃ p k, Prime p ∧ 0 < k ∧ p ^ k = n
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
/-- A choice of splitting for a short exact short complex `S` in a balanced category
such that `S.X₃` is projective.  -/
CategoryTheory.ShortComplex.ShortExact.splittingOfProjective : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        S.ShortExact → [CategoryTheory.Projective S.X₃] → [CategoryTheory.Balanced C] → S.Splitting
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → Option γ} {k : α},
  (Std.TreeMap.filterMap f t).getKey! k = ((t.getKey? k).pfilter fun x h' => (f x t[x]).isSome).get!
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDerivWithin_comp_eq_sum_orderedFinpartition : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g f : 𝕜 → 𝕜} {s t : Set 𝕜} {x : 𝕜} {n : WithTop ℕ∞} {i : ℕ},
  ContDiffWithinAt 𝕜 n g t (f x) →
    ContDiffWithinAt 𝕜 n f s x →
      UniqueDiffOn 𝕜 t →
        UniqueDiffOn 𝕜 s →
          x ∈ s →
            Set.MapsTo f s t →
              ↑i ≤ n →
                iteratedDerivWithin i (g ∘ f) s x =
                  ∑ c, iteratedDerivWithin c.length g t (f x) * ∏ j, iteratedDerivWithin (c.partSize j) f s x
-- Mathlib.RingTheory.Ideal.Defs
Ideal.mul_mem_right : ∀ {α : Type u_1} {a : α} (b : α) [inst : Semiring α] (I : Ideal α) [I.IsTwoSided], a ∈ I → a * b ∈ I
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isEmpty_unitOfList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.DHashMap.Raw.Const.unitOfList l).isEmpty = l.isEmpty
-- Mathlib.LinearAlgebra.Dimension.LinearMap
/-- `rank f` is the rank of a `LinearMap` `f`, defined as the dimension of `f.range`.  -/
LinearMap.rank : {K : Type u} →
  {V : Type v} →
    {V' : Type v'} →
      [inst : Semiring K] →
        [inst_1 : AddCommMonoid V] →
          [inst_2 : Module K V] → [inst_3 : AddCommMonoid V'] → [inst_4 : Module K V'] → (V →ₗ[K] V') → Cardinal.{v'}
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.Iff.symm : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ : L.BoundedFormula α n}, T.Iff φ ψ → T.Iff ψ φ
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- `weightedVSubOfPoint` gives equal results for two families of weights and two families of
points that are equal on `s`.  -/
Finset.weightedVSubOfPoint_congr : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) {w₁ w₂ : ι → k},
  (∀ i ∈ s, w₁ i = w₂ i) →
    ∀ {p₁ p₂ : ι → P},
      (∀ i ∈ s, p₁ i = p₂ i) → ∀ (b : P), (s.weightedVSubOfPoint p₁ b) w₁ = (s.weightedVSubOfPoint p₂ b) w₂
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.reverse.eq_1 : ∀ {T : Type u_1} {N : Type u_2} (r : ContextFreeRule T N), r.reverse = { input := r.input, output := r.output.reverse }
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.of_formallyUnramified_of_flat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Flat f] [AlgebraicGeometry.FormallyUnramified f]
  [AlgebraicGeometry.LocallyOfFinitePresentation f], AlgebraicGeometry.Etale f
-- Init.Data.UInt.Bitwise
UInt64.toUInt32_not : ∀ (a : UInt64), (~~~a).toUInt32 = ~~~a.toUInt32
-- Lean.Elab.InfoTree.Types
Lean.Elab.CustomInfo.value : Lean.Elab.CustomInfo → Dynamic
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_mul_of_nonneg : ∀ {x y z : ℤ}, 0 ≤ y → x / (y * z) = x / y / z
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.mulSingle_div : ∀ {I : Type u} {f : I → Type v} [inst : DecidableEq I] [inst_1 : (i : I) → Group (f i)] (i : I) (x y : f i),
  Pi.mulSingle i (x / y) = Pi.mulSingle i x / Pi.mulSingle i y
-- Mathlib.RingTheory.Etale.QuasiFinite
/-- A less universe polymorphic version of
`exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq`. Use that instead.  -/
_private.Mathlib.RingTheory.Etale.QuasiFinite.0.Algebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq' : ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Finite R S]
  (p : Ideal R) [inst_4 : p.IsPrime],
  ∃ R' x x_1,
    ∃ (_ : Algebra.Etale R R'),
      ∃ P,
        ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p),
          ∃ n e,
            ∃ (_ : CompleteOrthogonalIdempotents e),
              ∃ P',
                ∃ (_ : ∀ (i : Fin n), (P' i).IsPrime) (_ : ∀ (i : Fin n), (P' i).LiesOver P),
                  Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (Algebra.ofId R R') ⋯) ∧
                    (∀ (i : Fin n), e i.castSucc ∉ P' i) ∧
                      ∀ (P'' : Ideal (TensorProduct R R' S)),
                        P''.IsPrime →
                          P''.LiesOver P → e (Fin.last n) ∈ P'' ∧ ∀ (i : Fin n), e i.castSucc ∉ P'' → P'' = P' i
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.toAddCommMonoid : {M : Type u} → [self : Lean.Grind.AddCommGroup M] → Lean.Grind.AddCommMonoid M
-- Std.Data.ExtDHashMap.Basic
/-- Internal implementation detail of the hash map.  -/
Std.ExtDHashMap.lift₂ : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        {γ : Sort w} →
          (f : Std.DHashMap α β → Std.DHashMap α β → γ) →
            (∀ (a b c d : Std.DHashMap α β), a.Equiv c → b.Equiv d → f a b = f c d) →
              Std.ExtDHashMap α β → Std.ExtDHashMap α β → γ
-- Std.Do.PostCond
Std.Do.PostCond.entails.refl : ∀ {α : Type u_1} {ps : Std.Do.PostShape} (Q : Std.Do.PostCond α ps), Q.entails Q
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.unit_rightAdjointUniq_hom_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 : CategoryTheory.Functor C D} {G G' : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F ⊣ G') (x : C) {Z : C} (h : G'.obj (F.obj x) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj1.unit.app x)
      (CategoryTheory.CategoryStruct.comp ((adj1.rightAdjointUniq adj2).hom.app (F.obj x)) h) =
    CategoryTheory.CategoryStruct.comp (adj2.unit.app x) h
-- Init.Data.Array.Lemmas
Array.eq_empty_iff_size_eq_zero : ∀ {α : Type u_1} {xs : Array α}, xs = #[] ↔ xs.size = 0
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.lt_iff_of_unique : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : Unique α] [inst_2 : LT N] [inst_3 : Preorder α]
  {x y : Colex (α →₀ N)}, x < y ↔ (ofColex x) default < (ofColex y) default
-- Mathlib.Topology.SeparatedMap
isLocallyInjective_iff_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y},
  IsLocallyInjective f ↔ ∀ (x : X), ∃ U ∈ nhds x, Set.InjOn f U
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedRUsage.default : Std.Internal.UV.System.RUsage
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensRangeParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier) (range : Lean.Lsp.Range),
  sizeOf { textDocument := textDocument, range := range } = 1 + sizeOf textDocument + sizeOf range
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Projective
/-- Projective general linear group $PGL(n, R)$
defined as the quotient of the general linear group by its center.  -/
MatrixGroups.«termPGL(_,_)_1» : Lean.ParserDescr
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.eq_of_embedding_eq_conjugate : ∀ (K : Type u_1) [inst : Field K] {v₁ v₂ : NumberField.InfinitePlace K},
  v₁.embedding = NumberField.ComplexEmbedding.conjugate v₂.embedding → v₁ = v₂
-- Lean.Attributes
Lean.AttributeImplCore.mk.sizeOf_spec : ∀ (ref : autoParam Lean.Name Lean.AttributeImplCore.ref._autoParam) (name : Lean.Name) (descr : String)
  (applicationTime : Lean.AttributeApplicationTime),
  sizeOf { ref := ref, name := name, descr := descr, applicationTime := applicationTime } =
    1 + sizeOf ref + sizeOf name + sizeOf descr + sizeOf applicationTime
-- Mathlib.Algebra.Ring.GeomSum
Nat.pow_sub_one_dvd_pow_sub_one : ∀ {m k : ℕ} (x : ℕ), m ∣ k → x ^ m - 1 ∣ x ^ k - 1
-- Mathlib.AlgebraicGeometry.Cover.Sigma
AlgebraicGeometry.Scheme.Cover.instUniqueI₀Sigma : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  {S : AlgebraicGeometry.Scheme} →
    [inst : AlgebraicGeometry.IsZariskiLocalAtSource P] →
      [inst_1 : UnivLE.{v, u}] →
        (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) S) → Unique 𝒰.sigma.I₀
-- Mathlib.Order.Hom.Basic
OrderIso.orderEmbeddingCongr_symm_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : LE α] [inst_1 : LE β] [inst_2 : LE γ]
  [inst_3 : LE δ] (f : α ≃o γ) (g : β ≃o δ) (h : γ ↪o δ),
  (f.orderEmbeddingCongr g).symm h = ((RelIso.toRelEmbedding f).trans h).trans (RelIso.toRelEmbedding g.symm)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.isScalarTower_right : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] (f : Polynomial R) [inst_1 : DistribSMul S R]
  [inst_2 : IsScalarTower S R R], IsScalarTower S (AdjoinRoot f) (AdjoinRoot f)
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
Commute.pow_dvd_sub_pow_of_pow_eq_zero_left : ∀ {R : Type u_1} {x y : R} {n m p : ℕ} [inst : Ring R], n + m ≤ p + 1 → Commute x y → x ^ n = 0 → y ^ m ∣ (x - y) ^ p