mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.instCompleteSpaceStream' : ∀ {α : Type u_1}, CompleteSpace (Stream' α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_filterMap_le_size : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Option γ}, t.WF → (Std.TreeMap.Raw.filterMap f t).size ≤ t.size
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.hom_eq_iff : ∀ {α : Type u_1} {M : Type u_4} [inst : Monoid M] {f g : FreeMonoid α →* M},
  f = g ↔ ∀ (x : α), f (FreeMonoid.of x) = g (FreeMonoid.of x)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule_eq_denote : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (m : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denoteAsIntModule ctx m = Lean.Grind.CommRing.Mon.denote ctx m
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- A finitely strongly measurable function is measurable.  -/
MeasureTheory.FinStronglyMeasurable.measurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
  [inst_1 : TopologicalSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β] [BorelSpace β],
  MeasureTheory.FinStronglyMeasurable f μ → Measurable f
-- Mathlib.Data.Sum.Order
WithTop.orderIsoSumLexPUnit_top : ∀ {α : Type u_1} [inst : LE α], WithTop.orderIsoSumLexPUnit ⊤ = toLex (Sum.inr PUnit.unit)
-- Mathlib.Analysis.VonNeumannAlgebra.Basic
/-- The centralizer of a `VonNeumannAlgebra`, as a `VonNeumannAlgebra`.  -/
VonNeumannAlgebra.commutant : {H : Type u} →
  [inst : NormedAddCommGroup H] →
    [inst_1 : InnerProductSpace ℂ H] → [inst_2 : CompleteSpace H] → VonNeumannAlgebra H → VonNeumannAlgebra H
-- Aesop.RuleSet
Aesop.LocalRuleSet.contains : Aesop.LocalRuleSet → Aesop.RuleName → Bool
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.State.mk : Lean.Meta.Sym.State →
  Lean.Meta.Grind.State → List Lean.Meta.Grind.Goal → Lean.Elab.Tactic.Grind.Cache → Lean.Elab.Tactic.Grind.State
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b_relation_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.b₈ = W.b₂ * W.b₆ - W.b₄ ^ 2
-- Batteries.Data.String.Lemmas
/-- A substring is represented by three lists `l m r`, where `m` is the middle section
(the actual substring) and `l ++ m ++ r` is the underlying string.  -/
Substring.Raw.ValidFor : List Char → List Char → List Char → Substring.Raw → Prop
-- Mathlib.Algebra.CharP.Defs
ringChar.ringChar_subsingleton : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [Subsingleton R], ringChar R = 1
-- Init.Data.Float.Float
/-- Computes the exponential `e^x` of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`exp`.
 -/
Float.exp : Float → Float
-- Init.Data.Int.Gcd
Int.lcm_mul_gcd : ∀ (m n : ℤ), m.lcm n * m.gcd n = m.natAbs * n.natAbs
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.eq_top_iff : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → (l = ⊤ ↔ ∀ (i : ι), p i → s i = Set.univ)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_add_swap : ∀ {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} (f : M [⋀^ι]→ₗ[R] N) (v : ι → M)
  [inst_5 : DecidableEq ι] {i j : ι}, i ≠ j → f v + f (v ∘ ⇑(Equiv.swap i j)) = 0
-- Mathlib.Combinatorics.SimpleGraph.Circulant
SimpleGraph.circulantGraph_eq_symm : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), SimpleGraph.circulantGraph s = SimpleGraph.circulantGraph (s ∪ -s)
-- Batteries.Data.Char.AsciiCasing
/-- Case folding for ASCII characters only.

Alphabetic ASCII characters are mapped to their lowercase form, all other characters are left
unchanged. This agrees with the Unicode case folding algorithm for ASCII characters.

```
#eval caseFoldAsciiOnly 'A' == 'a'
#eval caseFoldAsciiOnly 'a' == 'a'
#eval caseFoldAsciiOnly 'À' == 'À'
#eval caseFoldAsciiOnly 'à' == 'à'
#eval caseFoldAsciiOnly '$' == '$'
```
 -/
Char.caseFoldAsciiOnly : Char → Char
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
ChartedSpace.LiftPropOn.eq_1 : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] (P : (H → H') → Set H → H → Prop) (f : M → M')
  (s : Set M), ChartedSpace.LiftPropOn P f s = ∀ x ∈ s, ChartedSpace.LiftPropWithinAt P f s x
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.sum_sq : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} (I : Finset ι) (a : ι → R), IsSumSq (∑ i ∈ I, a i ^ 2)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
Summable.const_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : AddCommMonoid α]
  [inst_2 : DistribSMul γ α] [ContinuousConstSMul γ α] {f : β → α} {L : SummationFilter β} (b : γ),
  Summable f L → Summable (fun i => b • f i) L
-- Mathlib.RingTheory.Artinian.Module
/-- A version of `isArtinian_pi` for non-dependent functions. We need this instance because
sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
prove that `ι → ℝ` is finite dimensional over `ℝ`).  -/
isArtinian_pi' : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
  [Finite ι] [IsArtinian R M], IsArtinian R (ι → M)
-- Init.Sym.Lemmas
Lean.Sym.Fin.le_eq_false : ∀ {n : ℕ} (a b : Fin n), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.Geometry.Euclidean.Triangle
/-- **Law of sines** (sine rule), angle-at-point form.  -/
EuclideanGeometry.sin_angle_mul_dist_eq_sin_angle_mul_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ p₃ : P),
  Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) * dist p₂ p₃ = Real.sin (EuclideanGeometry.angle p₃ p₁ p₂) * dist p₃ p₁
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.rangeRestrict_injective_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N},
  Function.Injective ⇑f.rangeRestrict ↔ Function.Injective ⇑f
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoDiv_sub : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIcoDiv hp a (b - p) = toIcoDiv hp a b - 1
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.one_lt_lift_iff : ∀ {a : Cardinal.{u}}, 1 < Cardinal.lift.{v, u} a ↔ 1 < a
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_ne_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]}, ↑x ≠ 0 ↔ x ≠ 0
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_eq_some_getD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α}
  {fallback : β}, a ∈ t → t[a]? = some (t.getD a fallback)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.Λ.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (s : ℂ),
  P.Λ s = P.Λ₀ s - (1 / s) • P.f₀ - (P.ε / (↑P.k - s)) • P.g₀
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.centralizer_toSubsemiring : ∀ {R : Type u_1} [inst : Ring R] (s : Set R), (Subring.centralizer s).toSubsemiring = Subsemiring.centralizer s
-- Mathlib.Topology.Order.LiminfLimsup
/-- Ad hoc typeclass stating that neighborhoods are eventually bounded below.  -/
BoundedGENhdsClass : (α : Type u_7) → [Preorder α] → [TopologicalSpace α] → Prop
-- Lean.Meta.Basic
/-- Similar to `approxDefEq`, but uses all available approximations.
We don't use `constApprox` by default at `approxDefEq` because it often produces undesirable solution for monadic code.
For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[Pure ?m]`.
Now, assume the expected type is `IO Bool`. Then, the unification constraint `?m Prop =?= IO Bool` could be solved
as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to
solve `[Pure (fun _ => IO Bool)]`  -/
Lean.Meta.fullApproxDefEq : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → n α → n α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.ε_pullback_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X R : C}
  {f : R ⟶ X},
  CategoryTheory.Over.Hom.left (CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Over.pullback f)) =
    CategoryTheory.inv (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.id X) f)
-- Mathlib.NumberTheory.SumFourSquares
Int.exists_sq_add_sq_add_one_eq_mul : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.mk.injEq : ∀ (toMatcherInfo : Lean.Meta.MatcherInfo) (matcherName : Lean.Name) (matcherLevels : Array Lean.Level)
  (params : Array Lean.Expr) (motive : Lean.Expr) (discrs alts remaining : Array Lean.Expr)
  (toMatcherInfo_1 : Lean.Meta.MatcherInfo) (matcherName_1 : Lean.Name) (matcherLevels_1 : Array Lean.Level)
  (params_1 : Array Lean.Expr) (motive_1 : Lean.Expr) (discrs_1 alts_1 remaining_1 : Array Lean.Expr),
  ({ toMatcherInfo := toMatcherInfo, matcherName := matcherName, matcherLevels := matcherLevels, params := params,
        motive := motive, discrs := discrs, alts := alts, remaining := remaining } =
      { toMatcherInfo := toMatcherInfo_1, matcherName := matcherName_1, matcherLevels := matcherLevels_1,
        params := params_1, motive := motive_1, discrs := discrs_1, alts := alts_1, remaining := remaining_1 }) =
    (toMatcherInfo = toMatcherInfo_1 ∧
      matcherName = matcherName_1 ∧
        matcherLevels = matcherLevels_1 ∧
          params = params_1 ∧ motive = motive_1 ∧ discrs = discrs_1 ∧ alts = alts_1 ∧ remaining = remaining_1)
-- Mathlib.Data.Nat.Squarefree
Nat.squarefree_iff_factorization_le_one : ∀ {n : ℕ}, n ≠ 0 → (Squarefree n ↔ ∀ (p : ℕ), n.factorization p ≤ 1)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instMonoid.eq_1 : ∀ {α : Type u_1} [inst : Monoid α],
  OrderDual.instMonoid =
    { toSemigroup := OrderDual.instSemigroup, toOne := OrderDual.instOne, one_mul := ⋯, mul_one := ⋯,
      toNPow := NPow.ofPow, npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- Lawfulness of `convolutionUnitApp`.  -/
CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp_eq : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} (V : Type u₂) {inst_1 : CategoryTheory.Category.{v₂, u₂} V}
  {inst_2 : CategoryTheory.MonoidalCategory C} {inst_3 : CategoryTheory.MonoidalCategory V} {D : Type u₃}
  {inst_4 : CategoryTheory.Category.{v₃, u₃} D}
  [self : CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] (d d' : D)
  (x y : C),
  CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutionUnitApp V d d' x y =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.MonoidalCategory.DayConvolution.unit
            ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).obj d)
            ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι C V D).obj
              d')).app
        (x, y))
      ((CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorObjIsoConvolution C
              V d d').inv.app
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbit_vadd : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] (g : G) (a : α),
  AddAction.orbit G (g +ᵥ a) = AddAction.orbit G a
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.instSDiff : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → SDiff (Std.TreeMap.Raw α β cmp)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDivisionMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : DivisionMonoid Mᵐᵒᵖ], DomMulAct.instDivisionMonoidOfMulOpposite = inst
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey?_eq_some_getKey! : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], (↑m).WF → ∀ {a : α}, m.contains a = true → m.getKey? a = some (m.getKey! a)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_gcd_of_dvd : ∀ (d a x p : ℤ), d ∣ a * x + p → Int.Internal.Linear.gcd✝ d a ∣ p
-- Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
AlgebraicGeometry.isClosedMap_isZariskiLocalAtTarget : AlgebraicGeometry.IsZariskiLocalAtTarget
  (AlgebraicGeometry.topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] => IsClosedMap)
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofBitVec : ∀ {a : BitVec 16}, { toBitVec := a }.toNat = a.toNat
-- Mathlib.Topology.Sheaves.Presheaf
/-- The restriction of a section along an inclusion of open sets.
For `x : F.obj (op V)`, we provide the notation `x |_ U`, where the proof `U ≤ V` is inferred by
the tactic `Top.presheaf.restrict_tac'`  -/
TopCat.Presheaf.restrictOpen : {X : TopCat} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {FC : C → C → Type u_1} →
        {CC : C → Type u_2} →
          [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] →
            [inst_2 : CategoryTheory.ConcreteCategory C FC] →
              {F : TopCat.Presheaf C X} →
                {V : TopologicalSpace.Opens ↑X} →
                  CategoryTheory.ToType (F.obj (Opposite.op V)) →
                    (U : TopologicalSpace.Opens ↑X) →
                      autoParam (U ≤ V) TopCat.Presheaf.restrictOpen._auto_1 →
                        CategoryTheory.ToType (F.obj (Opposite.op U))
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.mk.sizeOf_spec : ∀ (symm : Bool) (proof type : Lean.Expr) (index : Lean.HeadIndex × ℕ)
  (mvarIds : Array (Lean.MVarId × Array Lean.LocalDecl)),
  sizeOf { symm := symm, proof := proof, type := type, index := index, mvarIds := mvarIds } =
    1 + sizeOf symm + sizeOf proof + sizeOf type + sizeOf index + sizeOf mvarIds
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectOutput.below : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    {motive : (a : Std.Iter β) → (a_1 : β) → a.IsPlausibleIndirectOutput a_1 → Prop} →
      {a : Std.Iter β} → {a_1 : β} → a.IsPlausibleIndirectOutput a_1 → Prop
-- Mathlib.Order.DirectedInverseSystem
/-- It is a natural family of bijections.  -/
InverseSystem.PEquivOn.nat : ∀ {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [inst : LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i}
  [inst_1 : SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι}
  (self : InverseSystem.PEquivOn f equivSucc s), InverseSystem.IsNatEquiv f self.equiv
-- Lean.Meta.Tactic.Grind.Arith.ModelUtil
_private.Lean.Meta.Tactic.Grind.Arith.ModelUtil.0.Lean.Meta.Grind.Arith.satisfyDiseqs.checkDiseq : Std.HashMap Lean.Expr ℚ → ℤ → Lean.Expr → Bool
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.instIsStandardEtale : ∀ {R : Type u_1} [inst : CommRing R], Algebra.IsStandardEtale R R
-- Std.Data.TreeMap.Basic
/-- Returns a map that contains all mappings of `t₁` and `t₂`. In case that both maps contain the
same key `k` with respect to `cmp`, the provided function is used to determine the new value from
the respective values in `t₁` and `t₂`.

This function ensures that `t₁` is used linearly. It also uses the individual values in `t₁`
linearly if the merge function uses the second argument (i.e. the first of type `β a`) linearly.
Hence, as long as `t₁` is unshared, the performance characteristics follow the following imperative
description: Iterate over all mappings in `t₂`, inserting them into `t₁` if `t₁` does not contain a
conflicting mapping yet. If `t₁` does contain a conflicting mapping, use the given merge function to
merge the mapping in `t₂` into the mapping in `t₁`. Then return `t₁`.

Hence, the runtime of this method scales logarithmically in the size of `t₁` and linearly in the size of
`t₂` as long as `t₁` is unshared.
 -/
Std.TreeMap.mergeWith : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} → (α → β → β → β) → Std.TreeMap α β cmp → Std.TreeMap α β cmp → Std.TreeMap α β cmp
-- Mathlib.Order.OmegaCompletePartialOrder
/-- `Part.bind` as a continuous function.  -/
OmegaCompletePartialOrder.ContinuousHom.bind : {α : Type u_2} → [inst : OmegaCompletePartialOrder α] → {β γ : Type v} → (α →𝒄 Part β) → (α →𝒄 β → Part γ) → α →𝒄 Part γ
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor'_map_τ₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Arrow (CategoryTheory.Arrow C)}
  (φ : X ⟶ Y),
  (CategoryTheory.Square.fromArrowArrowFunctor'.map φ).τ₂ =
    CategoryTheory.Arrow.Hom.right (CategoryTheory.Arrow.Hom.left φ)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- Algebra homomorphism `F⟮α⟯ →ₐ[F] K` are in bijection with the set of roots
of `minpoly α` in `K`.  -/
IntermediateField.algHomAdjoinIntegralEquiv : (F : Type u_1) →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {α : E} →
            {K : Type u} →
              [inst_3 : Field K] →
                [inst_4 : Algebra F K] → IsIntegral F α → (↥F⟮α⟯ →ₐ[F] K) ≃ { x // x ∈ (minpoly F α).aroots K }
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.coe_of : ∀ {L : FirstOrder.Language} (T : L.Theory) (M : Type w) [inst : L.Structure M] [inst_1 : M ⊨ T] [inst_2 : Nonempty M],
  ↑(FirstOrder.Language.Theory.ModelType.of T M) = M
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Polynomial.Irreducible.natDegree_dvd_finrank : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {f : Polynomial K},
  Irreducible f → (Polynomial.map (algebraMap K L) f).Splits → f.natDegree ∣ Module.finrank K L
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.widePushoutShapeOp_map : ∀ (J : Type w) {X Y : CategoryTheory.Limits.WidePushoutShape J} (a : X ⟶ Y),
  (CategoryTheory.Limits.widePushoutShapeOp J).map a = CategoryTheory.Limits.widePushoutShapeOpMap J X Y a
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.Nat.smul_eq_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {n n' : ℕ} {r : R}, ↑n = r → n' = n → ∀ (a : R), n' • a = r * a
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_insertListIfNewₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {l : List ((a : α) × β a)},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(m.insertListIfNewₘ l)).buckets).Perm
      (Std.Internal.List.insertListIfNew (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Init.Data.Ord.Basic
List.compareLex.eq_1 : ∀ {α : Type u_1} (cmp : α → α → Ordering), List.compareLex cmp [] [] = Ordering.eq
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting.0.CategoryTheory.Limits.termI₂_1 : Lean.ParserDescr
-- Lean.Meta.CongrTheorems
/-- The lemma contains three parameters for this kind of argument `a_i`, `b_i` and `eq_i : a_i = b_i`.
`a_i` and `b_i` represent the left and right hand sides, and `eq_i` is a proof for their equality.  -/
Lean.Meta.CongrArgKind.eq : Lean.Meta.CongrArgKind
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- The Frobenius automorphism of `k`, as a linear map  -/
Isocrystal.«term_→ᶠˡ[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.ZMod.Basic
ZMod.cast_pow' : ∀ {n : ℕ} {R : Type u_1} [inst : Ring R] [CharP R n] (a : ZMod n) (k : ℕ), (a ^ k).cast = a.cast ^ k
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.RespectsIso],
  (∀ {X Y : C} {f : X ⟶ Y} {R : CategoryTheory.Presieve X},
      R ∈ K.coverings X → (P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryTheory.CategoryStruct.comp g f))) →
    P.IsLocalAtSource K
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.Valid.remainingToString : ∀ {l r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l r it → it.remainingToString = String.ofList r
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.instEmptyCollectionTheorems : {α : Type} → EmptyCollection (Lean.Meta.Grind.Theorems α)
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.fst_surjective : ∀ {G₀ : Type u_1} {H₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀],
  Function.Surjective ⇑(MonoidWithZeroHom.fst G₀ H₀)
-- Aesop.RuleTac.Basic
Aesop.instInhabitedRuleTacInput.default : Aesop.RuleTacInput
-- Mathlib.Topology.Order.PartialSups
ContinuousWithinAt.partialSups : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : ℕ → X → L} {n : ℕ} {s : Set X} {x : X},
  (∀ k ≤ n, ContinuousWithinAt (f k) s x) → ContinuousWithinAt ((partialSups f) n) s x
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instAddCommGroup : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → AddCommGroup (AdicCompletion I M)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.singularPart_eq_self : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ.singularPart ν = μ ↔ μ.MutuallySingular ν
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.instUniqueHomOfPUnit : (X : CommRingCat) → Unique (X ⟶ CommRingCat.of PUnit.{u + 1})
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.mem_saturation_of_mul_mem_left : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid} {x y : S},
  x * y ∈ s.saturation M H → x ∈ M → y ∈ s.saturation M H
-- Mathlib.CategoryTheory.Elements
/-- The functor `(F ⋙ G).Elements ⥤ G.Elements`.  -/
CategoryTheory.Functor.Elements.precomp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{u_2, u_1} D] →
        (F : CategoryTheory.Functor C D) →
          (G : CategoryTheory.Functor D (Type w)) → CategoryTheory.Functor (F.comp G).Elements G.Elements
-- Mathlib.Data.EReal.Operations
EReal.top_mul_top : ⊤ * ⊤ = ⊤
-- Mathlib.Order.Defs.LinearOrder
min_le_right : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), min a b ≤ b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Affine F} [inst_1 : DecidableEq F] {x₁ x₂ y₁ y₂ : F},
  W.Equation x₁ y₁ →
    W.Equation x₂ y₂ →
      ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂) →
        WeierstrassCurve.Affine.CoordinateRing.XIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) *
            (WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₁ (Polynomial.C y₁) *
              WeierstrassCurve.Affine.CoordinateRing.XYIdeal W x₂ (Polynomial.C y₂)) =
          WeierstrassCurve.Affine.CoordinateRing.YIdeal W
              (WeierstrassCurve.Affine.linePolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂)) *
            WeierstrassCurve.Affine.CoordinateRing.XYIdeal W (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))
              (Polynomial.C (W.addY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂)))