mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.vadd_set_subset_vadd_set_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : AddAction α β] {A B : Set β} {a : α},
  a +ᵥ A ⊆ a +ᵥ B ↔ A ⊆ B
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.un.sizeOf_spec : ∀ {w : ℕ} (op : Std.Tactic.BVDecide.BVUnOp) (operand : Std.Tactic.BVDecide.BVExpr w),
  sizeOf (Std.Tactic.BVDecide.BVExpr.un op operand) = 1 + sizeOf w + sizeOf op + sizeOf operand
-- Mathlib.Algebra.Module.FinitePresentation
Module.FinitePresentation.of_subsingleton : ∀ {R : Type u_2} (M : Type u_1) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Subsingleton M],
  Module.FinitePresentation R M
-- Lean.Declaration
Lean.instBEqTheoremVal : BEq Lean.TheoremVal
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.mem_Lp_of_ae_le : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {f : α →ₘ[μ] E} {g : ↥(MeasureTheory.Lp F p μ)},
  (∀ᵐ (x : α) ∂μ, ‖↑f x‖ ≤ ‖↑↑g x‖) → f ∈ MeasureTheory.Lp E p μ
-- Init.MethodSpecsSimp
Mul.mul_eq_hMul : ∀ {α : Type u_1} [inst : Mul α], Mul.mul = HMul.hMul
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.hole : Lean.TSyntax `Lean.binderIdent → Lean.Parser.Tactic.MRefinePat
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.snd_isEmbedding_of_left : ∀ {X Y S : TopCat} {f : X ⟶ S},
  Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    ∀ (g : Y ⟶ S), Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))
-- Lean.DocString.Extension
Lean.VersoModuleDocs.assemble : Lean.VersoModuleDocs → Except String Lean.VersoDocString
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.prod_mono : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] ⦃s₁ s₂ : Subring R⦄,
  s₁ ≤ s₂ → ∀ ⦃t₁ t₂ : Subring S⦄, t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [h : Std.TransCmp cmp] {k a : α},
  (t.insert k).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Lean.Meta.CtorRecognizer
/-- If `e` is a constructor application, return a pair containing the corresponding `ConstructorVal` and the constructor
application arguments.
 -/
Lean.Meta.constructorApp? : Lean.Expr → Lean.MetaM (Option (Lean.ConstructorVal × Array Lean.Expr))
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the largest key that is less than the given key,
returning `fallback` if no such key exists.
 -/
Std.DTreeMap.Raw.getKeyLTD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap.Raw α β cmp → α → α → α
-- Mathlib.Algebra.Polynomial.Roots
/-- The set of distinct roots of `p` in `S`.

If you have a non-separable polynomial, use `Polynomial.aroots` for the multiset
where multiple roots have the appropriate multiplicity.  -/
Polynomial.rootSet : {T : Type w} →
  [inst : CommRing T] → Polynomial T → (S : Type u_1) → [inst_1 : CommRing S] → [IsDomain S] → [Algebra T S] → Set S
-- Mathlib.Tactic.Convert
/-- Replaces the type of the local declaration `fvarId` with `typeNew`,
using `Lean.MVarId.congrN!` to prove that the old type of `fvarId` is equal to `typeNew`.
Uses `Lean.MVarId.replaceLocalDecl` to replace the type.
Returns the new goal along with the side goals generated by `congrN!`.

With `symm = true`, reverses the equality,
changing the goal to prove `typeNew` is equal to `typeOld`.
With `depth = some n`, calls `MVarId.congrN! n` instead, with `n` as the max recursion depth.
 -/
Lean.MVarId.convertLocalDecl : Lean.MVarId →
  Lean.FVarId →
    Lean.Expr →
      Bool →
        optParam (Option ℕ) none →
          optParam Congr!.Config { } →
            optParam (List (Lean.TSyntax `rintroPat)) [] → Lean.MetaM (Lean.MVarId × List Lean.MVarId)
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
/-- The horizontal composition on 2-morphisms is defined using the action on arrows of the
composition bifunctor from the enriched category structure.  -/
CategoryTheory.CatEnriched.hComp : {C : Type u_1} →
  [inst : CategoryTheory.EnrichedCategory CategoryTheory.Cat C] →
    {a b c : CategoryTheory.CatEnriched C} →
      {f f' : a ⟶ b} →
        {g g' : b ⟶ c} →
          (f ⟶ f') → (g ⟶ g') → (CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f' g')
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.birdDet.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.finset_inf'_nhds : ∀ {L : Type u_1} [inst : TopologicalSpace L] {ι : Type u_3} {α : Type u_4} {s : Finset ι} {f : ι → α → L} {l : Filter α}
  {g : ι → L} [inst_1 : SemilatticeInf L] [ContinuousInf L] (hne : s.Nonempty),
  (∀ i ∈ s, Filter.Tendsto (f i) l (nhds (g i))) → Filter.Tendsto (s.inf' hne f) l (nhds (s.inf' hne g))
-- Init.System.IO
/-- A pure-Lean abstraction of POSIX streams. These streams may represent an underlying POSIX stream or
be implemented by Lean code.

Because standard input, standard output, and standard error are all `IO.FS.Stream`s that can be
overridden, Lean code may capture and redirect input and output.
 -/
IO.FS.Stream : Type
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.ofSubsingleton.congr_simp : ∀ (R : Type uR) {ι : Type uι} (M₂ : Type v₂) (M₃ : Type v₃) [inst : Semiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : Subsingleton ι] (i i_1 : ι),
  i = i_1 → MultilinearMap.ofSubsingleton R M₂ M₃ i = MultilinearMap.ofSubsingleton R M₂ M₃ i_1
-- Mathlib.Data.Rat.Lemmas
Rat.den_div_intCast_eq_one_iff : ∀ (m n : ℤ), n ≠ 0 → ((↑m / ↑n).den = 1 ↔ n ∣ m)
-- Init.Data.Nat.Basic
/-- Compiled version of `Nat.rec` so that we can define `Nat.recAux` to be defeq to `Nat.rec`.
This is working around the fact that the compiler does not currently support recursors.  -/
Nat.recCompiled : {motive : ℕ → Sort u} → motive Nat.zero → ((n : ℕ) → motive n → motive n.succ) → (t : ℕ) → motive t
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapGrp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal],
  e.mapGrp =
    { functor := e.functor.mapGrp, inverse := e.inverse.mapGrp,
      unitIso :=
        CategoryTheory.Functor.mapGrpIdIso.symm ≪≫
          CategoryTheory.Functor.mapGrpNatIso e.unitIso ≪≫ CategoryTheory.Functor.mapGrpCompIso,
      counitIso :=
        CategoryTheory.Functor.mapGrpCompIso.symm ≪≫
          CategoryTheory.Functor.mapGrpNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapGrpIdIso,
      functor_unitIso_comp := ⋯ }
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.mapM.map.eq_1 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m β) (as : Array α) (i : ℕ) (bs : Array β),
  Array.mapM.map✝ f as i bs =
    if hlt : i < as.size then do
      let __do_lift ← f as[i]
      Array.mapM.map✝ f as (i + 1) (bs.push __do_lift)
    else pure bs
-- Mathlib.RingTheory.RootsOfUnity.Minpoly
/-- The degree of the minimal polynomial of `μ` is at least `totient n`.  -/
IsPrimitiveRoot.totient_le_degree_minpoly : ∀ {n : ℕ} {K : Type u_1} [inst : CommRing K] {μ : K},
  IsPrimitiveRoot μ n → ∀ [IsDomain K] [CharZero K], n.totient ≤ (minpoly ℤ μ).natDegree
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.mem_closure_comm : ∀ {α : Type u_1} {M : Matroid α} {e f : α}, M.IsNonloop e → M.IsNonloop f → (f ∈ M.closure {e} ↔ e ∈ M.closure {f})
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.has_limits_of_finite_and_cofiltered : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteLimits C]
  [CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w, w, v, u} C], CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
-- Mathlib.FieldTheory.Fixed
FixedPoints.isSeparable : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [Finite G],
  Algebra.IsSeparable (↥(FixedPoints.subfield G F)) F
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_rightAngleRotation_right : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E), (o.areaForm x) (o.rightAngleRotation y) = inner ℝ x y
-- Mathlib.CategoryTheory.Triangulated.TStructure.AbelianSubcategory
CategoryTheory.Triangulated.AbelianSubcategory.ιK_mor₁_assoc : ∀ {C : Type u_1} {A : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [inst_6 : CategoryTheory.Category.{v_2, u_2} A]
  {ι : CategoryTheory.Functor A C} {X₁ X₂ : A} {f₁ : X₁ ⟶ X₂} {X₃ : C} {f₂ : ι.obj X₂ ⟶ X₃}
  {f₃ : X₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj (ι.obj X₁)},
  CategoryTheory.Pretriangulated.Triangle.mk (ι.map f₁) f₂ f₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
    ∀ {K : A} (α : (CategoryTheory.shiftFunctor C 1).obj (ι.obj K) ⟶ X₃) [inst_7 : ι.Full]
      [inst_8 : CategoryTheory.Preadditive A] [ι.Faithful] {Z : A} (h : X₂ ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Triangulated.AbelianSubcategory.ιK f₃ α)
          (CategoryTheory.CategoryStruct.comp f₁ h) =
        CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Logic.Embedding.Basic
/-- Composition of `f : α ↪ β` and `g : β ↪ γ`.  -/
Function.Embedding.trans : {α : Sort u_1} → {β : Sort u_2} → {γ : Sort u_3} → (α ↪ β) → (β ↪ γ) → α ↪ γ
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresenter.mk.inj : ∀ {userName : String} {layoutKind : ProofWidgets.LayoutKind} {present : Lean.Expr → Lean.MetaM ProofWidgets.Html}
  {userName_1 : String} {layoutKind_1 : ProofWidgets.LayoutKind} {present_1 : Lean.Expr → Lean.MetaM ProofWidgets.Html},
  { userName := userName, layoutKind := layoutKind, present := present } =
      { userName := userName_1, layoutKind := layoutKind_1, present := present_1 } →
    userName = userName_1 ∧ layoutKind = layoutKind_1 ∧ present = present_1
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α}
  {b : β a}, t.WF → (t.insertIfNew a b).WF
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote.match_1.congr_eq_1 : ∀ (motive : Lean.Grind.CommRing.Mon → Sort u_1) (x : Lean.Grind.CommRing.Mon)
  (h_1 : Unit → motive Lean.Grind.CommRing.Mon.unit)
  (h_2 : (p : Lean.Grind.CommRing.Power) → (m : Lean.Grind.CommRing.Mon) → motive (Lean.Grind.CommRing.Mon.mult p m)),
  x = Lean.Grind.CommRing.Mon.unit →
    (match x with
      | Lean.Grind.CommRing.Mon.unit => h_1 ()
      | Lean.Grind.CommRing.Mon.mult p m => h_2 p m) ≍
      h_1 ()
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_map_equiv_iff : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} (e : α ≃ᵐ β) {f : β → γ},
  AEMeasurable f (MeasureTheory.Measure.map (⇑e) μ) ↔ AEMeasurable (f ∘ ⇑e) μ
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.le_def : ∀ {α : Type ua} {u₁ u₂ : UniformSpace α}, u₁ ≤ u₂ ↔ uniformity α ≤ uniformity α
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.takeEndWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.toSlice.takeEndWhile pat = s.takeEndWhile pat
-- Init.Data.Fin.Lemmas
/-- Proves a statement by cases on the underlying `Nat` value in a `Fin (n + 1)`, checking whether the
value is the greatest representable or a predecessor of some other.

The two cases are:
 * `last`, used when the value is `Fin.last n`
 * `cast`, used when the value is of the form `(j : Fin n).succ`

The corresponding induction principle is `Fin.reverseInduction`.
 -/
Fin.lastCases : {n : ℕ} →
  {motive : Fin (n + 1) → Sort u_1} →
    motive (Fin.last n) → ((i : Fin n) → motive i.castSucc) → (i : Fin (n + 1)) → motive i
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_pi : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] {ι' : Type u_7} {M' : ι' → Type u_8} [inst_4 : (i : ι') → AddCommMonoid (M' i)]
  [inst_5 : (i : ι') → TopologicalSpace (M' i)] [inst_6 : (i : ι') → Module R (M' i)]
  (f : (i : ι') → M [⋀^ι]→L[R] M' i), ⇑(ContinuousAlternatingMap.pi f) = fun m j => (f j) m
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.polarCoordReal_source : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  (NumberField.mixedEmbedding.polarCoordReal K).source = Set.univ ×ˢ Set.univ.pi fun x => polarCoord.source
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.hom_comp : ∀ {A B C : ProfiniteGrp.{u}} (f : A ⟶ B) (g : B ⟶ C),
  ProfiniteGrp.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (ProfiniteGrp.Hom.hom g).comp (ProfiniteGrp.Hom.hom f)
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_3.eq_3 : ∀ (motive : Lean.Expr → Sort u_1) (binderName : Lean.Name) (ty body : Lean.Expr) (binderInfo : Lean.BinderInfo)
  (h_1 : (name : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const name us))
  (h_2 : (f x : Lean.Expr) → motive (f.app x))
  (h_3 :
    (binderName : Lean.Name) →
      (ty body : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName ty body binderInfo))
  (h_4 : Unit → motive (Lean.Expr.sort Lean.Level.zero)) (h_5 : (a : Lean.Level) → motive (Lean.Expr.sort a.succ))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (x : Lean.Expr) → motive x),
  (match Lean.Expr.forallE binderName ty body binderInfo with
    | Lean.Expr.const name us => h_1 name us
    | f.app x => h_2 f x
    | Lean.Expr.forallE binderName ty body binderInfo => h_3 binderName ty body binderInfo
    | Lean.Expr.sort Lean.Level.zero => h_4 ()
    | Lean.Expr.sort a.succ => h_5 a
    | Lean.Expr.sort u => h_6 u
    | x => h_7 x) =
    h_3 binderName ty body binderInfo
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.map_inf : ∀ {X Y : AlgebraicGeometry.Scheme} (I₁ I₂ : X.IdealSheafData) (f : X ⟶ Y), (I₁ ⊓ I₂).map f = I₁.map f ⊓ I₂.map f
-- Lean.Data.Lsp.Communication
Lean.IO.FS.Stream.readLspNotificationAs : IO.FS.Stream → String → (α : Type) → [Lean.FromJson α] → IO (Lean.JsonRpc.Notification α)
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.FilterMap.0.Std.IterM.forIn_filterMapWithPostcondition.match_1.eq_2 : ∀ {β₂ : Type u_1} (motive : Option β₂ → Sort u_2) (h_1 : (c : β₂) → motive (some c)) (h_2 : Unit → motive none),
  (match none with
    | some c => h_1 c
    | none => h_2 ()) =
    h_2 ()
-- Std.Time.Format.Modifier
Std.Time.OffsetX.hourMinuteSecondColon.sizeOf_spec : sizeOf Std.Time.OffsetX.hourMinuteSecondColon = 1
-- Mathlib.CategoryTheory.Sites.Localization
CategoryTheory.GrothendieckTopology.W_sheafToPresheaf_map_iff_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (J : CategoryTheory.GrothendieckTopology C)
  {A : Type u_2} [inst_1 : CategoryTheory.Category.{v_2, u_2} A] {F₁ F₂ : CategoryTheory.Sheaf J A} (φ : F₁ ⟶ F₂),
  J.W ((CategoryTheory.sheafToPresheaf J A).map φ) ↔ CategoryTheory.IsIso φ
-- Mathlib.Topology.Instances.AddCircle.Real
ZMod.toAddCircle_eq_zero : ∀ {N : ℕ} [inst : NeZero N] {j : ZMod N}, ZMod.toAddCircle j = 0 ↔ j = 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₈.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R),
  W.b₈ = W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2
-- Mathlib.CategoryTheory.Sites.Plus
/-- The natural isomorphism between `P` and `P⁺` when `P` is a sheaf.  -/
CategoryTheory.GrothendieckTopology.isoToPlus : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            (P : CategoryTheory.Functor Cᵒᵖ D) →
              [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] →
                CategoryTheory.Presheaf.IsSheaf J P → (P ≅ J.plusObj P)
-- Mathlib.Data.List.Defs
List.permutationsAux.rec.eq_def : ∀ {α : Type u_1} {C : List α → List α → Sort v} (H0 : (is : List α) → C [] is)
  (H1 : (t : α) → (ts is : List α) → C ts (t :: is) → C is [] → C (t :: ts) is) (x x_1 : List α),
  List.permutationsAux.rec H0 H1 x x_1 =
    match x, x_1 with
    | [], is => H0 is
    | t :: ts, is => H1 t ts is (List.permutationsAux.rec H0 H1 ts (t :: is)) (List.permutationsAux.rec H0 H1 is [])
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- Every coefficient in a Cantor normal form is positive.  -/
Ordinal.CNF.snd_pos : ∀ {b o : Ordinal.{u}} {x : Ordinal.{u} × Ordinal.{u}}, x ∈ Ordinal.CNF b o → 0 < x.2
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of an inner regular measure under left multiplication is again inner regular.  -/
MeasureTheory.innerRegular_map_mul_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.InnerRegular] (g : G),
  (MeasureTheory.Measure.map (fun x => g * x) μ).InnerRegular
-- Init.Data.Array.Erase
Array.eraseIdx_eq_take_drop_succ : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.size), xs.eraseIdx i h = xs.take i ++ xs.drop (i + 1)
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.isMonicOfDegree_one_iff : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R] {f : Polynomial R},
  f.IsMonicOfDegree 1 ↔ ∃ r, f = Polynomial.X + Polynomial.C r
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
/-- If `X` is an integral scheme that is universally closed and of finite type over `Spec K`,
then `Γ(X, ⊤)` is a finite field extension over `K`.  -/
AlgebraicGeometry.finite_appTop_of_universallyClosed : ∀ {X : AlgebraicGeometry.Scheme} (K : Type u) [inst : Field K] (f : X ⟶ AlgebraicGeometry.Spec (CommRingCat.of K))
  [AlgebraicGeometry.IsIntegral X] [AlgebraicGeometry.UniversallyClosed f] [AlgebraicGeometry.LocallyOfFiniteType f],
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).Finite
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.NonemptyCompacts.instPreconnectedSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [PreconnectedSpace α],
  PreconnectedSpace (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Topology.Instances.Nat
Nat.preimage_closedBall : ∀ (x : ℕ) (r : ℝ), Nat.cast ⁻¹' Metric.closedBall (↑x) r = Metric.closedBall x r
-- Init.Data.Fin.Lemmas
Fin.ofNat_sub : ∀ {n : ℕ} [inst : NeZero n] (x : ℕ) (y : Fin n), Fin.ofNat n x - y = Fin.ofNat n (n - ↑y + x)
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.intCast_ofNat : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (n : ℕ),
  Lean.Grind.Ring.OfSemiring.intCast (OfNat.ofNat n) = Lean.Grind.Ring.OfSemiring.natCast n
-- Lean.Parser.Term
Lean.Parser.Term.depArrow : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.inverse_obj_V : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G]
  (F : CategoryTheory.Functor (CategoryTheory.SingleObj G) V),
  (Action.FunctorCategoryEquivalence.inverse.obj F).V = F.obj PUnit.unit
-- Mathlib.Analysis.Normed.Field.Basic
/-- TODO: merge with `_root_.exists_enorm_lt`.  -/
NormedField.exists_enorm_lt : ∀ (α : Type u_2) [inst : NontriviallyNormedField α] {r : ENNReal}, 0 < r → ∃ x, 0 < ‖x‖ₑ ∧ ‖x‖ₑ < r
-- Mathlib.Data.ENat.Basic
ENat.addLECancellable_natCast : ∀ (a : ℕ), AddLECancellable ↑a
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.leftRegularHomEquiv_symm_single : ∀ {k : Type u} {G : Type v} [inst : CommRing k] [inst_1 : Monoid G] {A : Rep.{max u v, u, v} k G} (x : ↑A) (g : G),
  (Rep.Hom.hom (A.leftRegularHomEquiv.symm x)) (MonoidAlgebra.single g 1) = (A.ρ g) x
-- Mathlib.Data.DFinsupp.Defs
/-- The underlying function of a dependent function with finite support (aka `DFinsupp`).  -/
DFinsupp.toFun : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → Zero (β i)] → DFinsupp β → (i : ι) → β i
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.instIsIsoCommRingCatAppObjOpensOpensFunctor : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.app f ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U))
-- Mathlib.Topology.UnitInterval
unitInterval.symmHomeomorph_symm_apply : ∀ (a : ↑unitInterval), unitInterval.symmHomeomorph.symm a = unitInterval.symm a
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.size_toArray_rio : ∀ {b : ℕ}, (*...b).toArray.size = b
-- Mathlib.Algebra.Group.Indicator
/-- **Alias** of `Set.mulIndicator_sdiff`. -/
Set.mulIndicator_diff : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] {s t : Set α},
  s ⊆ t → ∀ (f : α → G), (t \ s).mulIndicator f = t.mulIndicator f * (s.mulIndicator f)⁻¹
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.toColon.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ Ψ : CategoryTheory.Abelian.Preradical C), Φ.toColon Ψ = CategoryTheory.MonoOver.homMk (⋯.lift Φ.ι 0 ⋯) ⋯
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_ite_mem_eq : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Fintype ι] (s : Finset ι) (f : ι → M)
  [inst_2 : DecidablePred fun x => x ∈ s], (∑ i, if i ∈ s then f i else 0) = ∑ i ∈ s, f i
-- Lean.Data.Lsp.Internal
Lean.Lsp.instInhabitedLeanQueryModuleResponse : Inhabited Lean.Lsp.LeanQueryModuleResponse
-- Mathlib.Algebra.Group.Action.Basic
invOf_smul_smul : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : MulAction α β] (c : α) (x : β) [inst_2 : Invertible c],
  ⅟c • c • x = x
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.IsFredholm.isClosed_range : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F}, u.IsFredholm → IsClosed ↑(↑u).range
-- Mathlib.Data.TwoPointing
TwoPointing.swap_swap : ∀ {α : Type u_1} (p : TwoPointing α), p.swap.swap = p
-- Mathlib.Topology.Algebra.GroupWithZero
/-- Eta-expanded form of `ContinuousAt.inv₀` -/
ContinuousAt.fun_inv₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : Zero G₀] [inst_1 : Inv G₀] [inst_2 : TopologicalSpace G₀] [ContinuousInv₀ G₀]
  {f : α → G₀} {a : α} [inst_4 : TopologicalSpace α], ContinuousAt f a → f a ≠ 0 → ContinuousAt (fun i => (f i)⁻¹) a
-- Mathlib.Data.ZMod.Basic
ZMod.charP : ∀ (n : ℕ), CharP (ZMod n) n
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
/-- `x ^ k = o(exp(b * x))` as `x → ∞` for any natural `k` and positive `b`.  -/
isLittleO_pow_exp_pos_mul_atTop : ∀ (k : ℕ) {b : ℝ}, 0 < b → (fun x => x ^ k) =o[Filter.atTop] fun x => Real.exp (b * x)
-- Mathlib.Topology.UniformSpace.Cauchy
cauchy_nhds : ∀ {α : Type u} [uniformSpace : UniformSpace α] {a : α}, Cauchy (nhds a)