mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Fin.SuccPred
/-- Given `i : Fin (n + 2)` and `j : Fin (n + 1)`,
there are two ways to represent the order embedding `Fin n → Fin (n + 2)`
leaving holes at `i` and `i.succAbove j`.

One is `i.succAbove ∘ j.succAbove`.
It corresponds to embedding `Fin n` to `Fin (n + 1)` leaving a hole at `j`,
then embedding the result to `Fin (n + 2)` leaving a hole at `i`.
The other one is `(i.succAbove j).succAbove ∘ (j.predAbove i).succAbove`.
It corresponds to swapping the roles of `i` and `j`.

This lemma says that these two ways are equal.
It is used in `Fin.removeNth_removeNth_eq_swap`
to show that two ways of removing 2 elements from a sequence give the same answer.
 -/
Fin.succAbove_succAbove_succAbove_predAbove : ∀ {n : ℕ} (i : Fin (n + 2)) (j : Fin (n + 1)) (k : Fin n),
  (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)
-- Mathlib.Analysis.Normed.Module.Ball.Homeomorph
OpenPartialHomeomorph.ball_subset_univBall_target : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {P : Type u_2}
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor E P] (c : P) (r : ℝ),
  Metric.ball c r ⊆ (OpenPartialHomeomorph.univBall c r).target
-- Lean.Meta.Basic
/-- `withConfig f x` executes `x` using the updated configuration object obtained by applying `f`.  -/
Lean.Meta.withConfig : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → (Lean.Meta.Config → Lean.Meta.Config) → n α → n α
-- Mathlib.Data.Finset.Union
Finset.biUnion_inter : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] (s : Finset α) (f : α → Finset β) (t : Finset β),
  s.biUnion f ∩ t = s.biUnion fun x => f x ∩ t
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Descent
RingHom.FaithfullyFlat.codescendsAlong_injective : RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] f => Function.Injective ⇑f)
  fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] [inst_10 : SizeOf 𝕜] [inst_11 : SizeOf E] [inst_12 : SizeOf F]
  [inst_13 : SizeOf G] (leftFun : E → F) (leftDeriv : E →L[𝕜] F) (rightFun : E → G) (rightDeriv : E →L[𝕜] G) (pt : E)
  (hasStrictFDerivAt_leftFun : HasStrictFDerivAt leftFun leftDeriv pt)
  (hasStrictFDerivAt_rightFun : HasStrictFDerivAt rightFun rightDeriv pt) (range_leftDeriv : (↑leftDeriv).range = ⊤)
  (range_rightDeriv : (↑rightDeriv).range = ⊤) (isCompl_ker : IsCompl (↑leftDeriv).ker (↑rightDeriv).ker),
  sizeOf
      { leftFun := leftFun, leftDeriv := leftDeriv, rightFun := rightFun, rightDeriv := rightDeriv, pt := pt,
        hasStrictFDerivAt_leftFun := hasStrictFDerivAt_leftFun,
        hasStrictFDerivAt_rightFun := hasStrictFDerivAt_rightFun, range_leftDeriv := range_leftDeriv,
        range_rightDeriv := range_rightDeriv, isCompl_ker := isCompl_ker } =
    1 + sizeOf leftDeriv + sizeOf rightDeriv + sizeOf pt + sizeOf hasStrictFDerivAt_leftFun +
            sizeOf hasStrictFDerivAt_rightFun +
          sizeOf range_leftDeriv +
        sizeOf range_rightDeriv +
      sizeOf isCompl_ker
-- Mathlib.AlgebraicTopology.ModelCategory.Basic
_private.Mathlib.AlgebraicTopology.ModelCategory.Basic.0.HomotopicalAlgebra.ModelCategory.mk'.cm3a_aux : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [(HomotopicalAlgebra.weakEquivalences C).HasTwoOutOfThreeProperty]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)]
  [(HomotopicalAlgebra.cofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.trivialFibrations C)] {A B X Y : C}
  {f : A ⟶ B} {w : X ⟶ Y} [HomotopicalAlgebra.Fibration f] [HomotopicalAlgebra.WeakEquivalence w]
  (h : CategoryTheory.RetractArrow f w), HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.lieAlgebra.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] (b : P.Base) [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι],
  RootPairing.GeckConstruction.lieAlgebra b = RootPairing.GeckConstruction.lieAlgebra b
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- If `y` is a conjugate root of a nonzero element `x`, then `y` is not zero.
 -/
IsConjRoot.ne_zero : ∀ {K : Type u_2} {S : Type u_4} [inst : CommRing S] [inst_1 : Field K] [inst_2 : Algebra K S] [IsDomain S] {x y : S},
  x ≠ 0 → IsConjRoot K x y → y ≠ 0
-- Init.Data.Nat.Lemmas
Nat.pos_of_lt_mul_right : ∀ {a b c : ℕ}, a < b * c → 0 < b
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Pull back a cover along a morphism.  -/
CategoryTheory.GrothendieckTopology.pullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (J : CategoryTheory.GrothendieckTopology C) → (Y ⟶ X) → CategoryTheory.Functor (J.Cover X) (J.Cover Y)
-- Aesop.Script.TacticState
Aesop.Script.TacticState.focus : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Aesop.Script.TacticState → Lean.MVarId → m Aesop.Script.TacticState
-- Mathlib.Topology.Separation.Regular
/-- In a regular space, if a compact set and a closed set are disjoint, then they have disjoint
neighborhoods.  -/
SeparatedNhds.of_isCompact_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] {s t : Set X},
  IsCompact s → IsClosed t → Disjoint s t → SeparatedNhds s t
-- Mathlib.Data.Nat.Init
/-- Given `P : ℕ → ℕ → Sort*`, if for all `m n : ℕ` we can extend `P` from the rectangle
strictly below `(m, n)` to `P m n`, then we have `P n m` for all `n m : ℕ`.
Note that for non-`Prop` output it is preferable to use the equation compiler directly if possible,
since this produces equation lemmas.  -/
Nat.strongSubRecursion : {P : ℕ → ℕ → Sort u_1} → ((m n : ℕ) → ((x y : ℕ) → x < m → y < n → P x y) → P m n) → (n m : ℕ) → P n m
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity`.

---

The bijection `normalizedFactorsEquivSpanNormalizedFactors` between the set of prime
factors of `r` and the set of prime factors of the ideal `⟨r⟩` preserves multiplicities. See
`count_normalizedFactorsSpan_eq_count` for the version stated in terms of multisets `count`.  -/
emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] {r d : R} (hr : r ≠ 0) (hd : d ∈ UniqueFactorizationMonoid.normalizedFactors r),
  emultiplicity d r = emultiplicity (↑((Ideal.normalizedFactorsEquivSpanNormalizedFactors hr) ⟨d, hd⟩)) (Ideal.span {r})
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.entryAtIdx.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2}
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Balanced → (x_2 : ℕ) → x_2 < x.size → Sort u_3) (size : ℕ)
  (k : α) (v : β) (l' r' : Std.DTreeMap.Internal.Impl α fun x => β)
  (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) (n : ℕ)
  (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size)
  (h_1 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l' r' : Std.DTreeMap.Internal.Impl α fun x => β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner size k v l' r').Balanced) →
              (n : ℕ) →
                (h : n < (Std.DTreeMap.Internal.Impl.inner size k v l' r').size) →
                  motive (Std.DTreeMap.Internal.Impl.inner size k v l' r') hl n h),
  (match Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h with
    | Std.DTreeMap.Internal.Impl.inner size k v l' r', hl, n, h => h_1 size k v l' r' hl n h) =
    h_1 size k v l' r' hl n h
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.IndepFun.neg_left : ∀ {α : 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 β'} [inst : Neg β] [MeasurableNeg β],
  ProbabilityTheory.Kernel.IndepFun f g κ μ → ProbabilityTheory.Kernel.IndepFun (-f) g κ μ
-- Mathlib.Data.Multiset.Bind
Multiset.rel_join : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset (Multiset α)} {t : Multiset (Multiset β)},
  Multiset.Rel (Multiset.Rel r) s t → Multiset.Rel r s.join t.join
-- Mathlib.LinearAlgebra.TensorPower.Basic
/-- Homogeneous tensor powers $M^{\otimes n}$. `⨂[R]^n M` is a shorthand for
`⨂[R] (i : Fin n), M`.  -/
TensorProduct.«term⨂[_]^_» : Lean.ParserDescr
-- Mathlib.Algebra.Group.TypeTags.Basic
Additive.toMul_symm_eq : ∀ {α : Type u}, Additive.toMul.symm = Additive.ofMul
-- Mathlib.Tactic.Monotonicity.Attr
/-- A lemma stating the monotonicity of some function, with respect to appropriate relations on its
domain and range, and possibly with side conditions.  -/
Mathlib.Tactic.Monotonicity.Attr.ext : Lean.LabelExtension
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.centralizer_le_normalizer : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.centralizer s ≤ Subgroup.normalizer s
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.expand_zero : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R],
  MvPolynomial.expand 0 = (Algebra.ofId R (MvPolynomial σ R)).comp (MvPolynomial.aeval 1)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.anyM.eq_2 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type v} (p : α → m Bool) (a : α) (as : List α),
  List.anyM p (a :: as) = do
    let __do_lift ← p a
    match __do_lift with
      | true => pure true
      | false => List.anyM p as
-- Mathlib.CategoryTheory.Sites.ConstantSheaf
CategoryTheory.constantPresheafAdj_counit_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {T : C} (hT : CategoryTheory.Limits.IsTerminal T)
  (F : CategoryTheory.Functor Cᵒᵖ D) (x : Cᵒᵖ),
  ((CategoryTheory.constantPresheafAdj D hT).counit.app F).app x = F.map (hT.from (Opposite.unop x)).op
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} {l : List α} {k : α},
  Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l) k = ()
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.HasDifferentials.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {φ : S ⟶ F.op.comp R},
  (∃ M d, Nonempty d.Universal) → PresheafOfModules.HasDifferentials φ
-- Init.Data.Vector.Lemmas
Vector.sum_push : ∀ {α : Type u_1} {n : ℕ} [inst : Add α] [inst_1 : Zero α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {xs : Vector α n} {x : α}, (xs.push x).sum = xs.sum + x
-- Mathlib.Analysis.Normed.Group.Subgroup
Subgroup.seminormedGroup.eq_1 : ∀ {E : Type u_1} [inst : SeminormedGroup E] {s : Subgroup E},
  Subgroup.seminormedGroup =
    { norm := fun a => ‖s.subtype a‖, toGroup := s.toGroup, toPseudoMetricSpace := Subtype.pseudoMetricSpace,
      dist_eq := ⋯ }
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.exists_eventually_const_mul_le_r : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r), ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)
-- Lean.Parser.Term
/-- Predicate for what `explicitUniv` can follow. It is only meant to be used on an identifier
that becomes the head constant of an application.  -/
Lean.Parser.Term.isIdentOrDotIdentOrProj : Lean.Syntax → Bool
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.map_add : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω'] {f : Ω → Ω'},
  Measurable f → ∀ (ν₁ ν₂ : MeasureTheory.FiniteMeasure Ω), (ν₁ + ν₂).map f = ν₁.map f + ν₂.map f
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.subsemigroup.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  (s : UpperSet (ArchimedeanClass M)),
  ArchimedeanClass.subsemigroup s = { carrier := ArchimedeanClass.mk ⁻¹' ↑s, add_mem' := ⋯ }
-- Mathlib.Order.Circular
/-- Syntax typeclass for a strict betweenness relation.  -/
SBtw : Type u_1 → Type u_1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A B : CategoryTheory.CostructuredArrow S T} (f g : A ⟶ B),
  f.left = g.left → f = g
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_sub_of_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree g) < m.toSyn (m.degree f) → m.degree (f - g) = m.degree f
-- Mathlib.Analysis.Normed.Group.Continuity
continuous_nnnorm : ∀ {E : Type u_4} [inst : SeminormedAddGroup E], Continuous fun a => ‖a‖₊
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.Iso.map_hom_inv_id_eval_app_assoc : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [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} E]
  {X Y : CategoryTheory.GradedObject J C} (e : X ≅ Y) (F : CategoryTheory.Functor C (CategoryTheory.Functor D E))
  (j : J) (Y_1 : D) {Z : E} (h : (F.obj (X j)).obj Y_1 ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.map (e.hom j)).app Y_1)
      (CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y_1) h) =
    h
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionParams.toJson : Lean.Lsp.CodeActionParams → Lean.Json
-- Lean.Util.ReplaceLevel
_private.Lean.Util.ReplaceLevel.0.Lean.Expr.ReplaceLevelImpl.notAnExpr : Unit × Unit
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coe_coordChangeL' : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e]
  [inst_9 : Bundle.Trivialization.IsLinear R e'] {b : B} (hb : b ∈ e.baseSet ∩ e'.baseSet),
  ↑(Bundle.Trivialization.coordChangeL R e e' b) =
    (Bundle.Trivialization.linearEquivAt R e b ⋯).symm ≪≫ₗ Bundle.Trivialization.linearEquivAt R e' b ⋯
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.ofNatCode.eq_def : ∀ (x : ℕ),
  Nat.Partrec.Code.ofNatCode x =
    match x with
    | 0 => Nat.Partrec.Code.zero
    | 1 => Nat.Partrec.Code.succ
    | 2 => Nat.Partrec.Code.left
    | 3 => Nat.Partrec.Code.right
    | n.succ.succ.succ.succ =>
      let m := n.div2.div2;
      have hm := ⋯;
      have _m1 := ⋯;
      have _m2 := ⋯;
      match n.bodd, n.div2.bodd with
      | false, false => (Nat.Partrec.Code.ofNatCode (Nat.unpair m).1).pair (Nat.Partrec.Code.ofNatCode (Nat.unpair m).2)
      | false, true => (Nat.Partrec.Code.ofNatCode (Nat.unpair m).1).comp (Nat.Partrec.Code.ofNatCode (Nat.unpair m).2)
      | true, false => (Nat.Partrec.Code.ofNatCode (Nat.unpair m).1).prec (Nat.Partrec.Code.ofNatCode (Nat.unpair m).2)
      | true, true => (Nat.Partrec.Code.ofNatCode m).rfind'
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.sub_mul_right_right_iff : ∀ {R : Type u} [inst : CommRing R] {x y z : R}, IsCoprime x (y - z * x) ↔ IsCoprime x y
-- Mathlib.Order.Interval.Set.ProjIcc
Set.strictMonoOn_projIic : ∀ {α : Type u_1} [inst : LinearOrder α] {b : α}, StrictMonoOn (Set.projIic b) (Set.Iic b)
-- Mathlib.Topology.Order.Monotone
/-- A monotone continuous function is left-continuous in the order-theoretic sense.  -/
Continuous.leftOrdContinuous : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] {f : α → β} [inst_4 : TopologicalSpace β] [OrderTopology β],
  Continuous f → Monotone f → LeftOrdContinuous f
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- If an extension has finite separable degree one, then it is purely inseparable.  -/
isPurelyInseparable_of_finSepDegree_eq_one : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Field.finSepDegree F E = 1 → IsPurelyInseparable F E
-- Std.Internal.Do.Assertion
Std.Internal.Do.Assertion.mk : {α : Type w} → [toCompleteLattice : Lean.Order.CompleteLattice α] → Std.Internal.Do.Assertion α
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
constFormalMultilinearSeries_apply_succ : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E] [inst_4 : NormedSpace 𝕜 F] {c : F} {n : ℕ},
  constFormalMultilinearSeries 𝕜 E c (n + 1) = 0
-- Mathlib.Algebra.Module.Injective
Module.Baer.congr : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] (e : Q ≃ₗ[R] M), Module.Baer R Q ↔ Module.Baer R M
-- Init.Omega.Constraint
Lean.Omega.Constraint.trivial.eq_1 : Lean.Omega.Constraint.trivial = { lowerBound := none, upperBound := none }
-- Init.Data.UInt.Bitwise
UInt32.toUInt8_not : ∀ (a : UInt32), (~~~a).toUInt8 = ~~~a.toUInt8
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.IsSelfAdjoint.realToRCLike_rclikeToReal : ∀ {X : Type u_1} {𝕜 : Type u_2} [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] {f : C(X, 𝕜)},
  IsSelfAdjoint f → ContinuousMap.realToRCLike 𝕜 f.rclikeToReal = f
-- Aesop.Tree.Tracing
Aesop.Goal.withHeadlineTraceNode : {α : Type} →
  Aesop.Goal →
    Aesop.TraceOption →
      Lean.MetaM α → optParam Bool true → optParam (Lean.MessageData → Lean.MetaM Lean.MessageData) pure → Lean.MetaM α
-- Mathlib.Data.Set.Finite.Basic
Set.Infinite.exists_notMem_finset : ∀ {α : Type u} {s : Set α}, s.Infinite → ∀ (t : Finset α), ∃ a ∈ s, a ∉ t
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The proposition that the function preserves multiplication  -/
NonUnitalAlgHom.map_mul' : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] (self : A →ₛₙₐ[φ] B) (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.units_smul_resolvent_self : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : Rˣ} {a : A},
  r • resolvent a ↑r = resolvent (r⁻¹ • a) 1
-- Mathlib.Data.List.Infix
List.mem_of_mem_dropLast : ∀ {α : Type u_1} {l : List α} {a : α}, a ∈ l.dropLast → a ∈ l
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RccSliceData : (α : Type u) → [Ord α] → Type u
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.source_restr : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : Equidecomp X G) {A : Set X},
  A ⊆ f.source → (f.restr A).source = A
-- Init.Data.Option.Lemmas
Option.min_le_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Min α], (∀ (x y : α), x ⊓ y ≤ x) → ∀ {a b : Option α}, a ⊓ b ≤ a
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.add_single_apply_of_not_exists_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] (r : R) {g g' : M} (x : AddMonoidAlgebra R M),
  (¬∃ d, g' = d + g) → (x * AddMonoidAlgebra.single g r).coeff g' = 0
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.AdditiveFunctor.ofRightExact_obj_fst : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : CategoryTheory.Limits.HasZeroObject D]
  [inst_6 : CategoryTheory.Limits.HasBinaryBiproducts C] (F : C ⥤ᵣ D),
  ((CategoryTheory.AdditiveFunctor.ofRightExact C D).obj F).obj = F.obj
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instAddCommSemigroup : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → AddCommSemigroup (ContIntertwiningMap π₁ π₂)
-- Mathlib.RingTheory.Polynomial.Pochhammer
/-- The Pochhammer polynomial of degree `n` has roots at `0`, `-1`, ..., `-(n - 1)`.  -/
ascPochhammer_eval_neg_coe_nat_of_lt : ∀ {R : Type u} [inst : Ring R] {n k : ℕ}, k < n → Polynomial.eval (-↑k) (ascPochhammer R n) = 0
-- Init.Data.String.Basic
String.Pos.lt_ofToSlice_iff : ∀ {s : String} {p : s.Pos} {q : s.toSlice.Pos}, p < String.Pos.ofToSlice q ↔ p.toSlice < q
-- Mathlib.Data.Finset.Filter
/-- Elaborate set builder notation for `Finset`.

`{x ∈ s | p x}` is elaborated as `Finset.filter (fun x ↦ p x) s` if either the expected type is
`Finset ?α` or the expected type is not `Set ?α` and `s` has expected type `Finset ?α`.

See also
* `Data.Set.Defs` for the `Set` builder notation elaborator that this elaborator partly overrides.
* `Data.Fintype.Basic` for the `Finset` builder notation elaborator handling syntax of the form
  `{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.
* `Order.LocallyFinite.Basic` for the `Finset` builder notation elaborator handling syntax of the
  form `{x ≤ a | p x}`, `{x ≥ a | p x}`, `{x < a | p x}`, `{x > a | p x}`.

TODO: Write a delaborator
 -/
Mathlib.Meta.elabFinsetBuilderSep : Lean.Elab.Term.TermElab
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.exactFunctor_comp_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] {E : Type u''} [inst_4 : CategoryTheory.Category.{v'', u''} E] [CategoryTheory.Abelian E]
  [L.IsLocalization P.isoModSerre] [inst_7 : CategoryTheory.Preadditive D] [L.Additive]
  (G : CategoryTheory.Functor D E), CategoryTheory.exactFunctor C E (L.comp G) ↔ CategoryTheory.exactFunctor D E G
-- Mathlib.Topology.Order.LeftRightNhds
nhdsGT_basis_Ioc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α]
  [NoMaxOrder α] (a : α), (nhdsWithin a (Set.Ioi a)).HasBasis (fun x => a < x) (Set.Ioc a)