mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtHashMap.Lemmas
/-- Variant of `getElem_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.ExtHashMap.getElem_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtHashMap.map f m},
  (Std.ExtHashMap.map f m)[k] = f (m.getKey k ⋯) m[k]
-- Init.Data.ByteArray.Basic
ByteArray.instInhabitedIterator.default : ByteArray.Iterator
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_mul_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s₁ s₂ t : Finset α}, s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.responseError : Lean.JsonRpc.MessageKind
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of `Set.Infinite.inter_of_finite_sdiff`. -/
Set.Infinite.inter_of_finite_diff : ∀ {α : Type u_1} {s t : Set α}, s.Infinite → (s \ t).Finite → (s ∩ t).Infinite
-- Mathlib.Topology.Algebra.ConstMulAction
IsUnit.continuous_const_smul_iff : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Monoid M] [inst_1 : TopologicalSpace α] [inst_2 : MulAction M α]
  [ContinuousConstSMul M α] [inst_4 : TopologicalSpace β] {f : β → α} {c : M},
  IsUnit c → ((Continuous fun x => c • f x) ↔ Continuous f)
-- Mathlib.Analysis.Calculus.Deriv.Pi
hasDerivAt_single : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : NontriviallyNormedField 𝕜] (i : ι) (y : 𝕜),
  HasDerivAt (Pi.single i) (Pi.single i 1) y
-- Mathlib.Topology.Closure
closure_minimal : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ t → IsClosed t → closure s ⊆ t
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isTrail_def : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.IsTrail ↔ p.edges.Nodup
-- Mathlib.Order.Filter.IsBounded
Filter.IsCobounded.mono : ∀ {α : Type u_1} {r : α → α → Prop} {f g : Filter α}, f ≤ g → Filter.IsCobounded r f → Filter.IsCobounded r g
-- Mathlib.Tactic.CancelDenoms.Core
Mathlib.Tactic.CancelDenoms.pow_subst : ∀ {α : Type u_1} [inst : CommRing α] {n e1 t1 k l : α} {e2 : ℕ},
  n * e1 = t1 → l * n ^ e2 = k → k * e1 ^ e2 = l * t1 ^ e2
-- Mathlib.Computability.RegularExpressions
RegularExpression.map.eq_6 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (P : RegularExpression α),
  RegularExpression.map f P.star = (RegularExpression.map f P).star
-- Mathlib.Topology.Order.MonotoneConvergence
instInfConvergenceClassProd : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [InfConvergenceClass α] [InfConvergenceClass β], InfConvergenceClass (α × β)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.mem_range_gamma : ∀ {o : Ordinal.{u}}, o ∈ Set.range Ordinal.gamma ↔ Ordinal.veblen o 0 = o
-- Mathlib.CategoryTheory.Sums.Basic
/-- `inr_` is the functor `X ↦ inr X`.  -/
CategoryTheory.Sum.inr_ : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor D (C ⊕ D)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.isStarProjection_iff_isSymmetricProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E], IsStarProjection T ↔ (↑T).IsSymmetricProjection
-- Mathlib.Topology.Connected.Clopen
/-- The setoid of connected components of a topological space  -/
connectedComponentSetoid : (α : Type u_3) → [TopologicalSpace α] → Setoid α
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_filter_le_size : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : α → β → Bool}, (Std.HashMap.filter f m).size ≤ m.size
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.noZeroDivisors : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) [NoZeroDivisors R], NoZeroDivisors ↥s
-- Lean.Data.Lsp.Basic
/-- Arguments that the command handler should be invoked with.  -/
Lean.Lsp.Command.arguments? : Lean.Lsp.Command → Option (Array Lean.Json)
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.content_X : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R], Polynomial.X.content = 1
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The type of probability measures is a measurable space when equipped with the Giry monad.  -/
MeasureTheory.ProbabilityMeasure.instMeasurableSpace : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → MeasurableSpace (MeasureTheory.ProbabilityMeasure Ω)
-- Mathlib.Data.Nat.Find
Nat.findGreatest_mono_left : ∀ {P Q : ℕ → Prop} [inst : DecidablePred P] [inst_1 : DecidablePred Q],
  (∀ (n : ℕ), P n → Q n) → ∀ (n : ℕ), Nat.findGreatest P n ≤ Nat.findGreatest Q n
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
returning `fallback` if no such key exists.
 -/
Std.ExtDTreeMap.getKeyGTD : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtDTreeMap α β cmp → α → α → α
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.mk'.congr_simp : ∀ {R : Type u} [inst : NonAssocRing R] (s s_1 : Set R) (e_s : s = s_1) (sm sm_1 : Submonoid R) (e_sm : sm = sm_1)
  (sa sa_1 : AddSubgroup R) (e_sa : sa = sa_1) (hm : ↑sm = s) (ha : ↑sa = s),
  Subring.mk' s sm sa hm ha = Subring.mk' s_1 sm_1 sa_1 ⋯ ⋯
-- Mathlib.Algebra.Quandle
/-- The fixing property of a Quandle  -/
Quandle.fix : ∀ {α : Type u_1} [self : Quandle α] {x : α}, Shelf.act x x = x
-- Mathlib.Data.Finset.Max
Finset.min_le : ∀ {α : Type u_2} [inst : LinearOrder α] {a : α} {s : Finset α}, a ∈ s → s.min ≤ ↑a
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.ext_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} {K K' : CategoryTheory.Limits.Multicofork I} (e : K.pt ≅ K'.pt)
  (h :
    autoParam (∀ (i : J.R), CategoryTheory.CategoryStruct.comp (K.π i) e.hom = K'.π i)
      CategoryTheory.Limits.Multicofork.ext._auto_1),
  (CategoryTheory.Limits.Multicofork.ext e h).hom.hom = e.hom
-- Mathlib.Algebra.Notation.Prod
Prod.instInv.eq_1 : ∀ {G : Type u_8} {H : Type u_9} [inst : Inv G] [inst_1 : Inv H], Prod.instInv = { inv := fun p => (p.1⁻¹, p.2⁻¹) }
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator.mk.inj : ∀ {α : Type u} {β : α → Type v} {inst : Ord α} {iter : Std.DTreeMap.Internal.Zipper α β} {upper : α}
  {iter_1 : Std.DTreeMap.Internal.Zipper α β} {upper_1 : α},
  { iter := iter, upper := upper } = { iter := iter_1, upper := upper_1 } → iter = iter_1 ∧ upper = upper_1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instCompleteLattice : {X : AlgebraicGeometry.Scheme} → CompleteLattice X.IdealSheafData
-- Init.Data.Array.Perm
Array.Perm.rfl : ∀ {α : Type u_1} {xs : Array α}, xs.Perm xs
-- Std.Http.Data.Extensions
/-- An empty extensions map with no data.
 -/
Std.Http.Extensions.empty : Std.Http.Extensions
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_le_pi_div_two_iff : ∀ {z : ℂ}, z.arg ≤ Real.pi / 2 ↔ 0 ≤ z.re ∨ z.im < 0
-- Mathlib.LinearAlgebra.Contraction
/-- When `M` is a finite free module, the map `rTensorHomToHomRTensor` is an equivalence. Note
that `rTensorHomEquivHomRTensor` is not defined directly in terms of
`rTensorHomToHomRTensor`, but the equivalence between the two is given by
`rTensorHomEquivHomRTensor_toLinearMap` and `rTensorHomEquivHomRTensor_apply`.  -/
rTensorHomEquivHomRTensor : (R : Type u_2) →
  (M : Type u_3) →
    (P : Type u_5) →
      (Q : Type u_6) →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid P] →
              [inst_3 : AddCommMonoid Q] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R P] →
                    [inst_6 : Module R Q] →
                      [Module.Projective R M] →
                        [Module.Finite R M] → TensorProduct R (M →ₗ[R] P) Q ≃ₗ[R] M →ₗ[R] TensorProduct R P Q
-- Mathlib.Geometry.Euclidean.Angle.Incenter
/-- The incenter of a triangle bisects the angle at a vertex.  -/
Affine.Triangle.oangle_incenter_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  (t : Affine.Triangle ℝ P) {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ →
    i₁ ≠ i₃ →
      i₂ ≠ i₃ →
        EuclideanGeometry.oangle (t.points i₂) (t.points i₁) (Affine.Simplex.incenter t) =
          EuclideanGeometry.oangle (Affine.Simplex.incenter t) (t.points i₁) (t.points i₃)
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_emod_of_nonneg : ∀ {a : ℤ}, 0 ≤ a → ∀ (b : ℤ), (a % b).natAbs = a.natAbs % b.natAbs
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} (m m_1 : Std.DHashMap α β) (e_m : m = m_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ m), m.getKey a h = m_1.getKey a_1 ⋯
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.SpaceResult.mk.inj : ∀ {foundLine foundFlattenedHardLine : Bool} {space : ℕ} {foundLine_1 foundFlattenedHardLine_1 : Bool} {space_1 : ℕ},
  { foundLine := foundLine, foundFlattenedHardLine := foundFlattenedHardLine, space := space } =
      { foundLine := foundLine_1, foundFlattenedHardLine := foundFlattenedHardLine_1, space := space_1 } →
    foundLine = foundLine_1 ∧ foundFlattenedHardLine = foundFlattenedHardLine_1 ∧ space = space_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_insertMany_list : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k : α},
  (t.insertMany l)[k]? =
    (List.findSomeRev?
          (fun x =>
            match x with
            | (a, b) => if cmp a k = Ordering.eq then some b else none)
          l).or
      t[k]?
-- Mathlib.CategoryTheory.Countable
/-- The opposite of a countable category is countable.  -/
CategoryTheory.countableCategoryOpposite : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.CountableCategory J],
  CategoryTheory.CountableCategory Jᵒᵖ
-- Mathlib.Order.Filter.Pointwise
Filter.frequently_inv : ∀ {α : Type u_2} [inst : Inv α] {f : Filter α} {p : α → Prop}, (∃ᶠ (x : α) in f⁻¹, p x) ↔ ∃ᶠ (x : α) in f, p x⁻¹
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_neg_eq_arg_sub_pi_of_im_pos : ∀ {x : ℂ}, 0 < x.im → (-x).arg = x.arg - Real.pi
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.toFunctor : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Comonad C → CategoryTheory.Functor C C
-- Lean.Parser.Term
Lean.Parser.Term.withAnonymousAntiquot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.CompleteLattice.Basic
iInf_exists : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : Exists p → α},
  ⨅ (x : Exists p), f x = ⨅ i, ⨅ (h : p i), f ⋯
-- Mathlib.Order.Hom.Basic
/-- `>` is preserved by order embeddings of preorders.  -/
OrderEmbedding.gtEmbedding : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α ↪o β → (fun x1 x2 => x2 < x1) ↪r fun x1 x2 => x2 < x1
-- Mathlib.RingTheory.OrderOfVanishing.Basic
Ring.ordFrac_eq_ord : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsNoetherianRing R] [inst_2 : Ring.KrullDimLE 1 R] {K : Type u_3}
  [inst_3 : Field K] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K] [inst_6 : Nontrivial R] {x : R},
  x ≠ 0 → (Ring.ordFrac R) ((algebraMap R K) x) = (Ring.ordMonoidWithZeroHom R) x
-- Mathlib.Tactic.FBinop
_private.Mathlib.Tactic.FBinop.0.FBinopElab.analyze.go : FBinopElab.Tree✝ → StateRefT' IO.RealWorld FBinopElab.AnalyzeResult✝ Lean.Elab.TermElabM Unit
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.pred : Nat.Primrec Nat.pred
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instNonUnitalCommSemiring : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] → [NonUnitalCommSemiring β] → NonUnitalCommSemiring (MeasureTheory.SimpleFunc α β)
-- Mathlib.Geometry.Manifold.ContMDiffMFDeriv
/-- The function that sends `x` to the `y`-derivative of `f(x,y)` at `g(x)` applied to `g₂(x)` is
`C^n` at `x₀`, where the derivative is taken as a continuous linear map.
We have to assume that `f` is `C^(n+1)` at `(x₀, g(x₀))` and `g` is `C^n` at `x₀`.
We have to insert a coordinate change from `x₀` to `g₁(x)` to make the derivative sensible.

This is similar to `ContMDiffWithinAt.mfderivWithin`, but where the continuous linear map is
applied to a (variable) vector.
 -/
ContMDiffWithinAt.mfderivWithin_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {m n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {F : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  [Js : IsManifold J 1 N] {F' : Type u_11} [inst_16 : NormedAddCommGroup F'] [inst_17 : NormedSpace 𝕜 F']
  {G' : Type u_12} [inst_18 : TopologicalSpace G'] {J' : ModelWithCorners 𝕜 F' G'} {N' : Type u_13}
  [inst_19 : TopologicalSpace N'] [inst_20 : ChartedSpace G' N'] [Is : IsManifold I 1 M] [I's : IsManifold I' 1 M']
  {x₀ : N'} {f : N → M → M'} {g : N → M} {g₁ : N' → N} {g₂ : N' → E} {t : Set N} {u : Set M} {v : Set N'}, ⋯ → ⋯
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousLinearEquiv.isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [CompleteSpace E], IsOpen (Set.range ContinuousLinearEquiv.toContinuousLinearMap)
-- Init.Data.List.ControlImpl
_private.Init.Data.List.ControlImpl.0.List.flatMapM.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List (List β) → Sort u_3) (bs : List (List β))
  (h_1 : (bs : List (List β)) → motive [] bs)
  (h_2 : (a : α) → (as : List α) → (bs : List (List β)) → motive (a :: as) bs),
  (match [], bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_1 bs
-- Lean.Parser.Extension
Lean.Parser.ParserResolution.parser.sizeOf_spec : ∀ (decl : Lean.Name) (isDescr : Bool),
  sizeOf (Lean.Parser.ParserResolution.parser decl isDescr) = 1 + sizeOf decl + sizeOf isDescr
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.double_d_eq_zero₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} (f : X₀ ⟶ X₁) {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} (hi₀₁ : c.Rel i₀ i₁) (a b : ι), b ≠ i₁ → (HomologicalComplex.double f hi₀₁).d a b = 0
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.coe_neg_interval : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedAddMonoid α]
  (s : NonemptyInterval α), ↑(-s) = -↑s
-- Init.Data.SInt.Lemmas
Int64.toInt32_toISize : ∀ (n : Int64), n.toISize.toInt32 = n.toInt32
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat
CategoryTheory.Pseudofunctor.mapId'_hom_naturality : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ : B}
  {X Y : ↑(F.obj b₀)} (f : b₀ ⟶ b₀) (hf : f = CategoryTheory.CategoryStruct.id b₀) (a : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map a) ((F.mapId' f hf).hom.toNatTrans.app Y) =
    CategoryTheory.CategoryStruct.comp ((F.mapId' f hf).hom.toNatTrans.app X) a
-- Lean.Util.Trace
Lean.addTrace : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadTrace m] → [Lean.MonadRef m] → [Lean.AddMessageContext m] → Lean.Name → Lean.MessageData → m Unit
-- Mathlib.Algebra.CubicDiscriminant
Cubic.monic_of_a_eq_one' : ∀ {R : Type u_1} {b c d : R} [inst : Semiring R], { a := 1, b := b, c := c, d := d }.toPoly.Monic
-- Init.Data.UInt.Lemmas
UInt8.not_lt_zero : ∀ {a : UInt8}, ¬a < 0
-- Mathlib.FieldTheory.KummerExtension
/-- Also see `Polynomial.separable_X_pow_sub_C_unit`  -/
Polynomial.separable_X_pow_sub_C_of_irreducible : ∀ {K : Type u} [inst : Field K] {n : ℕ},
  (primitiveRoots n K).Nonempty →
    ∀ (a : K), Irreducible (Polynomial.X ^ n - Polynomial.C a) → (Polynomial.X ^ n - Polynomial.C a).Separable
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.inclusion_injective : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] {S T : NonUnitalStarSubalgebra R A} (h : S ≤ T),
  Function.Injective ⇑(NonUnitalStarSubalgebra.inclusion h)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendScalars.smul_tmul : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {M : ModuleCat R} (s s' : S)
  (m : ↑M), s • s' ⊗ₜ[R] m = (s * s') ⊗ₜ[R] m
-- Lean.Parser.Command
Lean.Parser.Command.openOnly.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Data.Set.Finite.Lattice
Set.Infinite.biUnion : ∀ {α : Type u} {ι : Type u_1} {s : ι → Set α} {a : Set ι}, a.Infinite → Set.InjOn s a → (⋃ i ∈ a, s i).Infinite
-- Init.SimpLemmas
and_iff_right_of_imp : ∀ {b a : Prop}, (b → a) → (a ∧ b ↔ b)
-- Init.PropLemmas
ite_iff_right_iff : ∀ {p : Prop} [inst : Decidable p] {x y : Prop}, ((if p then x else y) ↔ y) ↔ p → x = y
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.ULift.upFunctor_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.ULift.upFunctor.map f = f
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.instIsStableUnderBaseChangeAlongR : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  [Wₗ.IsStableUnderBaseChangeAgainst Wᵣ] (S₁ : CategoryTheory.Span Wₗ Wᵣ c c'), Wₗ.IsStableUnderBaseChangeAlong S₁.r
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
/-- The category of comonoid objects in a Cartesian monoidal category is equivalent
to the category itself, via the forgetful functor.
 -/
CategoryTheory.comonEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → CategoryTheory.Comon C ≌ C
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapAddMonIdIso_hom_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.AddMon C),
  (CategoryTheory.Functor.mapAddMonIdIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `ne_one_of_lt`. -/
LT.lt.ne_one : ∀ {α : Type u_1} {a b : α} [inst : Preorder α] [inst_1 : One α] [IsBotOneClass α], a < b → b ≠ 1
-- Mathlib.FieldTheory.IntermediateField.Basic
IsScalarTower.toAlgHom_fieldRange : ∀ (K : Type u_1) (L : Type u_2) (L' : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] [inst_5 : Algebra L L'] [inst_6 : IsScalarTower K L L'],
  ↑(IsScalarTower.toAlgHom K L L').fieldRange = Set.range ⇑(algebraMap L L')
-- Std.Do.WP.SimpLemmas
Std.Do.WP.modifyGet_MonadState : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ α : Type u} {Q : Std.Do.PostCond α ps} [inst : Std.Do.WP m ps]
  [inst_1 : MonadStateOf σ m] (f : σ → α × σ),
  (Std.Do.wp (modifyGet f)).apply Q = (Std.Do.wp (MonadStateOf.modifyGet f)).apply Q
-- Mathlib.Data.List.Basic
List.head!_nil : ∀ {α : Type u} [inst : Inhabited α], [].head! = default
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.div'`. -/
MeasureTheory.ProgMeasurable.div' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] {u v : ι → Ω → β} [inst_2 : MeasurableSpace ι] [inst_3 : Group β]
  [ContinuousDiv β],
  MeasureTheory.IsStronglyProgressive f u →
    MeasureTheory.IsStronglyProgressive f v → MeasureTheory.IsStronglyProgressive f fun i ω => u i ω / v i ω
-- Mathlib.Order.OrderDual
/-- **Alias** of the reverse direction of `OrderDual.toDual_le_toDual`. -/
LE.le.dual : ∀ {α : Type u_1} [inst : LE α] {a b : α}, b ≤ a → OrderDual.toDual a ≤ OrderDual.toDual b
-- Init.Data.Stream
Std.Stream : Type u → outParam (Type v) → Type (max u v)
-- Mathlib.Topology.Algebra.Order.Group
ContinuousWithinAt.mabs : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : CommGroup G] [inst_2 : LinearOrder G] [IsOrderedMonoid G]
  [OrderTopology G] {X : Type u_2} [inst_5 : TopologicalSpace X] {f : X → G} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun x => |f x|ₘ) s x
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
/-- The Weierstrass curve `Y² = X³ + X`. It is of j-invariant 1728 if it is an elliptic curve.  -/
WeierstrassCurve.ofJ1728 : (R : Type u_1) → [CommRing R] → WeierstrassCurve R
-- Mathlib.Data.Nat.Choose.Sum
/-- The sum of `(n+1).choose i * f i (n+1-i)` can be split into two sums at rank `n`,
respectively of `n.choose i * f i (n+1-i)` and `n.choose i * f (i+1) (n-i)`.  -/
Finset.sum_choose_succ_mul : ∀ {R : Type u_1} [inst : NonAssocSemiring R] (f : ℕ → ℕ → R) (n : ℕ),
  ∑ i ∈ Finset.range (n + 2), ↑((n + 1).choose i) * f i (n + 1 - i) =
    ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * f i (n + 1 - i) +
      ∑ i ∈ Finset.range (n + 1), ↑(n.choose i) * f (i + 1) (n - i)
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.SmallCofilteredIntermediate.instIsCofilteredOrEmpty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] (F : CategoryTheory.Functor D C),
  CategoryTheory.IsCofilteredOrEmpty (CategoryTheory.IsCofiltered.SmallCofilteredIntermediate F)
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.forget₂_map_ofHom : ∀ {X Y : Type u} [inst : AddGroup X] [inst_1 : AddGroup Y] (f : X →+ Y),
  (CategoryTheory.forget₂ AddGrpCat AddMonCat).map (AddGrpCat.ofHom f) = AddMonCat.ofHom f
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.single_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r₁ r₂ : R),
  MonoidAlgebra.single m (r₁ + r₂) = MonoidAlgebra.single m r₁ + MonoidAlgebra.single m r₂
-- Mathlib.Analysis.Complex.Polynomial.Basic
/-- An irreducible polynomial of prime degree with two non-real roots has full Galois group.  -/
Polynomial.Gal.galActionHom_bijective_of_prime_degree : ∀ {p : Polynomial ℚ},
  Irreducible p →
    Nat.Prime p.natDegree →
      Fintype.card ↑(p.rootSet ℂ) = Fintype.card ↑(p.rootSet ℝ) + 2 →
        Function.Bijective ⇑(Polynomial.Gal.galActionHom p ℂ)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.replaceIndFVars : ℕ → Array Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Constructs a generalized continued fraction without fractional part.  -/
GenContFract.ofInteger : {α : Type u_1} → α → GenContFract α
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.struct : {J : Type w} → CategoryTheory.CategoryStruct.{w, w} (CategoryTheory.Limits.WidePushoutShape J)
-- Mathlib.Algebra.Algebra.Subalgebra.Operations
AlgHom.ker_rangeRestrict : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B), RingHom.ker f.rangeRestrict = RingHom.ker f