mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_erase_eq_of_not_compare_minKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ¬compare k t.minKey! = Ordering.eq → (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey! = t.minKey!
-- Init.Data.UInt.Bitwise
UInt8.toUInt64_xor : ∀ (a b : UInt8), (a ^^^ b).toUInt64 = a.toUInt64 ^^^ b.toUInt64
-- Lean.Structure
/-- Returns the name of the structure that contains the field relative to structure `structName`.
If `structName` contains the field itself, returns that,
and otherwise recursively looks into parents that are subobjects.
 -/
Lean.findField? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_balanceR : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} (hlb : l.Balanced)
  (hrb : r.Balanced) (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond r.size l.size),
  (Std.DTreeMap.Internal.Impl.balanceR k v l r hlb hrb hlr).size = l.size + 1 + r.size
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- A shortcut to a convenient form for the negation in `LinearIndepOn.mem_span_iff`.  -/
LinearIndepOn.notMem_span_iff : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {s : Set ι} {a : ι} {f : ι → V},
  LinearIndepOn K f s → (f a ∉ Submodule.span K (f '' s) ↔ LinearIndepOn K f (insert a s) ∧ a ∉ s)
-- Mathlib.Data.Finmap
AList.toFinmap_entries : ∀ {α : Type u} {β : α → Type v} (s : AList β), s.toFinmap.entries = ↑s.entries
-- Mathlib.Topology.Spectral.Hom
SpectralMap.coe_id : ∀ (α : Type u_2) [inst : TopologicalSpace α], ⇑(SpectralMap.id α) = id
-- Mathlib.Analysis.InnerProductSpace.PiL2
Matrix.toEuclideanLin_apply_piLp_toLp : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {m : Type u_7} {n : Type u_8} [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  (M : Matrix m n 𝕜) (v : n → 𝕜), (Matrix.toEuclideanLin M) (WithLp.toLp 2 v) = WithLp.toLp 2 (M.mulVec v)
-- Mathlib.Analysis.Complex.HasPrimitives
DifferentiableOn.isConservativeOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {U : Set ℂ},
  DifferentiableOn ℂ f U → Complex.IsConservativeOn f U
-- Init.Data.Nat.Basic
Nat.add_sub_add_right : ∀ (n k m : ℕ), n + k - (m + k) = n - m
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.Internal.foldRevM.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m] (f : δ → (a : α) → β a → m δ)
  (init : δ) (b : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.Internal.foldRevM f init b =
    Array.foldrM (fun l acc => Std.DHashMap.Internal.AssocList.foldrM (fun a b d => f d a b) acc l) init b.buckets
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.Iso.inv_hom_id_app_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) {F_1 : D → D → Type uF} {carrier : D → Type w}
  {instFunLike : (X Y : D) → FunLike (F_1 X Y) (carrier X) (carrier Y)} [inst_2 : CategoryTheory.ConcreteCategory D F_1]
  (x : carrier (G.obj X)),
  (CategoryTheory.ConcreteCategory.hom (α.hom.app X)) ((CategoryTheory.ConcreteCategory.hom (α.inv.app X)) x) = x
-- Std.Data.Iterators.Combinators.Monadic.DropWhile
/-- Internal implementation detail of the iterator library.  -/
Std.Iterators.Types.DropWhile.dropping : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} → Std.Iterators.Types.DropWhile α m β P → Bool
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.inner_single_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a : 𝕜)
  (v : EuclideanSpace 𝕜 ι), inner 𝕜 v (EuclideanSpace.single i a) = a * (starRingEnd ((fun x => 𝕜) i)) (v.ofLp i)
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instRepr : {α : Type u} → [Repr α] → Repr (WithZero α)
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_inverse_map_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) {X Y : CategoryTheory.MorphismProperty.Comma L R₂ P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).inverse.map f).right =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).right
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.mapM.map.eq_def : ∀ {α : 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.NumberTheory.ModularForms.CuspFormSubmodule
ModularForm.cuspFormSubmodule.eq_1 : ∀ (Γ : Subgroup (GL (Fin 2) ℝ)) (k : ℤ) [inst : Γ.HasDetOne],
  ModularForm.cuspFormSubmodule Γ k = CuspForm.toModularFormₗ.range
-- Lean.Data.PersistentArray
Lean.PersistentArrayNode.brecOn.eq : ∀ {α : Type u} {motive_1 : Lean.PersistentArrayNode α → Sort u_1}
  {motive_2 : Array (Lean.PersistentArrayNode α) → Sort u_1} {motive_3 : List (Lean.PersistentArrayNode α) → Sort u_1}
  (t : Lean.PersistentArrayNode α) (F_1 : (t : Lean.PersistentArrayNode α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.PersistentArrayNode α)) → Lean.PersistentArrayNode.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.PersistentArrayNode.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalars_restrictScalarsL_comp : ∀ {𝕜 : Type u_1} {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : SeminormedAddCommGroup E]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E]
  [inst_7 : SeminormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F]
  [inst_10 : IsScalarTower 𝕜 𝕜' F] [inst_11 : SeminormedAddCommGroup G] [inst_12 : NormedSpace 𝕜 G]
  [inst_13 : NormedSpace 𝕜' G] [inst_14 : IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G),
  ContinuousLinearMap.bilinearRestrictScalars 𝕜 B =
    ContinuousLinearMap.restrictScalars 𝕜 (ContinuousLinearMap.restrictScalarsL 𝕜' F G 𝕜 𝕜' ∘SL B)
-- Mathlib.RingTheory.Localization.Module
Module.Basis.ofIsLocalizedModule_apply : ∀ {R : Type u_1} (Rₛ : Type u_2) [inst : CommSemiring R] (S : Submonoid R) [inst_1 : CommSemiring Rₛ]
  [inst_2 : Algebra R Rₛ] [inst_3 : IsLocalization S Rₛ] {M : Type u_3} {Mₛ : Type u_4} [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : AddCommMonoid Mₛ] [inst_7 : Module R Mₛ] [inst_8 : Module Rₛ Mₛ]
  [inst_9 : IsScalarTower R Rₛ Mₛ] (f : M →ₗ[R] Mₛ) [inst_10 : IsLocalizedModule S f] {ι : Type u_5}
  (b : Module.Basis ι R M) (i : ι), (Module.Basis.ofIsLocalizedModule Rₛ S f b) i = f (b i)
-- Mathlib.Data.Nat.Dist
Nat.dist_tri_right' : ∀ (n m : ℕ), n ≤ m + n.dist m
-- Mathlib.Topology.ClusterPt
ClusterPt.mono : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {f g : Filter X}, ClusterPt x f → f ≤ g → ClusterPt x g
-- Mathlib.Topology.Homotopy.TopCat.Path
TopCat.pathEquiv_symm_apply_hom_hom_apply : ∀ {X : TopCat} {x y : ↑X} (p : Path x y) (a : ULift.{u, 0} ↑unitInterval),
  (TopCat.Hom.hom (TopCat.pathEquiv.symm p).hom) a = p (TopCat.I.homeomorph a)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.mapMAux : {α : Type u} →
  {β : Type v} →
    {σ : Type u} →
      {m : Type u → Type w} →
        [Monad m] → (β → m σ) → Lean.PersistentHashMap.Node α β → m (Lean.PersistentHashMap.Node α σ)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.equivProd_functor_obj : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1}))
  (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) (a : CategoryTheory.Comma L R),
  (CategoryTheory.Comma.equivProd L R).functor.obj a = (a.left, a.right)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] {k : α}
  {f : Option β → Option β} {hc : k ∈ t.alter k f}, (t.alter k f).getKey k hc = k
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_single : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] [inst_1 : DecidableEq ι] (j i : ι) (x : β i),
  (DFinsupp.erase j fun₀ | i => x) = if i = j then 0 else fun₀ | i => x
-- Mathlib.CategoryTheory.Monoidal.Center
/-- The functor lifting a braided category to its center, using the braiding as the half-braiding.
 -/
CategoryTheory.Center.ofBraided : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.Functor C (CategoryTheory.Center C)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitor_tensor_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.coe_comap : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (S : Subsemigroup N) (f : M →ₙ* N),
  ↑(Subsemigroup.comap f S) = ⇑f ⁻¹' ↑S
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeffs_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq R] (r : R),
  (MvPolynomial.C r).coeffs = if r = 0 then ∅ else {r}
-- Mathlib.Algebra.Order.Floor.Defs
Nat.ceil_int : Nat.ceil = Int.toNat
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `AddAction.isBlock_iff_vadd_eq_or_disjoint`. -/
AddAction.IsBlock.vadd_eq_or_disjoint : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B → ∀ (g : G), g +ᵥ B = B ∨ Disjoint (g +ᵥ B) B
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {k : α}, (t.erase k)[k]! = default
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_of_isLUB_of_nonneg : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α]
  [inst_3 : TopologicalSpace α] [OrderTopology α] {f : ι → α} (i : α),
  (∀ (i : ι), 0 ≤ f i) → IsLUB (Set.range fun s => ∑ i ∈ s, f i) i → HasSum f i
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Construct a right unitor from specified limit cones.  -/
CategoryTheory.Limits.BinaryFan.rightUnitor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {s : CategoryTheory.Limits.Cone (CategoryTheory.Functor.empty C)} →
        CategoryTheory.Limits.IsLimit s →
          {t : CategoryTheory.Limits.BinaryFan X s.pt} → CategoryTheory.Limits.IsLimit t → (t.pt ≅ X)
-- Mathlib.RingTheory.Localization.Ideal
/-- **Alias** of `IsLocalization.bot_lt_under_prime`. -/
IsLocalization.bot_lt_comap_prime : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [IsLocalization M S] [IsDomain R],
  M ≤ nonZeroDivisors R → ∀ (p : Ideal S) [hpp : p.IsPrime], p ≠ ⊥ → ⊥ < Ideal.under R p
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearMap.coe_toContinuousLinearMap_symm : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F' : Type x}
  [inst_5 : AddCommGroup F'] [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [inst_8 : IsTopologicalAddGroup F']
  [inst_9 : ContinuousSMul 𝕜 F'] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : FiniteDimensional 𝕜 E],
  ⇑LinearMap.toContinuousLinearMap.symm = ContinuousLinearMap.toLinearMap
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of a monoid acts commutatively on that monoid.  -/
Submonoid.center.smulCommClass_left : ∀ {M : Type u_1} [inst : Monoid M], SMulCommClass (↥(Submonoid.center M)) M M
-- Lean.Elab.Tactic.Basic
/-- Save the current tactic state for a token `stx`.
This method is a no-op if `stx` has no position information.
We use this method to save the tactic state at punctuation such as `;`
 -/
Lean.Elab.Tactic.saveTacticInfoForToken : Lean.Syntax → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.NumberTheory.LSeries.HurwitzZeta
/-- Formula for `hurwitzZeta s` as a Dirichlet series in the convergence range. We
restrict to `a ∈ Icc 0 1` to simplify the statement.  -/
HurwitzZeta.hasSum_hurwitzZeta_of_one_lt_re : ∀ {a : ℝ}, a ∈ Set.Icc 0 1 → ∀ {s : ℂ}, 1 < s.re → HasSum (fun n => 1 / (↑n + ↑a) ^ s) (HurwitzZeta.hurwitzZeta (↑a) s)
-- Mathlib.Order.Filter.Basic
Filter.hnot_principal : ∀ {α : Type u} {s : Set α}, ￢Filter.principal s = Filter.principal sᶜ
-- Mathlib.Algebra.Module.Submodule.LinearMap
Submodule.subtype_injective : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] {module_M : Module R M} (p : Submodule R M),
  Function.Injective ⇑p.subtype
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Ioc_atBot_prod_atTop : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [NoBotOrder α],
  Filter.Tendsto (fun p => Finset.Ioc p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) Filter.atTop
-- Lean.Compiler.IR.Basic
/-- Store `y : ty` at Position `sizeof(void*)*i + offset` in `x`. `x` must be a Constructor object and `RC(x)` must be 1.
`ty` must not be `object`, `tobject`, `erased` nor `Usize`.  -/
Lean.IR.FnBody.sset : Lean.IR.VarId → ℕ → ℕ → Lean.IR.VarId → Lean.IR.IRType → Lean.IR.FnBody → Lean.IR.FnBody
-- Init.Data.SInt.Basic
instDecidableEqInt64 : DecidableEq Int64
-- Mathlib.CategoryTheory.Localization.HomEquiv
CategoryTheory.Localization.homEquiv.congr_simp : ∀ {C : Type u_1} {D₁ : Type u_5} {D₂ : Type u_6} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_5, u_5} D₁] [inst_2 : CategoryTheory.Category.{v_6, u_6} D₂]
  (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1) (L₁ : CategoryTheory.Functor C D₁)
  [inst_3 : L₁.IsLocalization W] (L₂ : CategoryTheory.Functor C D₂) [inst_4 : L₂.IsLocalization W] {X Y : C},
  CategoryTheory.Localization.homEquiv W L₁ L₂ = CategoryTheory.Localization.homEquiv W_1 L₁ L₂
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork_φK : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0)
  (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hg₂ : S₂.g = 0)
  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) (hc₂ : CategoryTheory.Limits.IsColimit c₂) (f : c₁.pt ⟶ c₂.pt)
  (comm :
    CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f),
  (CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork φ hg₁ c₁ hc₁ hg₂ c₂ hc₂ f comm).φK = φ.τ₂
-- Mathlib.RingTheory.Algebraic.Basic
IsAlgebraic.of_aeval_of_transcendental : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {r : A} {f : Polynomial R},
  IsAlgebraic R ((Polynomial.aeval r) f) → Transcendental R f → IsAlgebraic R r
-- Lean.Elab.Do.Legacy
/-- Extend the set of updated variables. It assumes `ws` is a super set of `c.uvars`.
We **cannot** simply update the field `c.uvars`, because `c` may have shadowed some variable in `ws`.
See discussion at `pullExitPoints`.
 -/
Lean.Elab.Term.Do.extendUpdatedVars : Lean.Elab.Term.Do.CodeBlock → Lean.Elab.Term.Do.VarSet → Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Every multifork is isomorphic to one of the form `Multifork.ofι`.  -/
CategoryTheory.Limits.Multifork.isoOfι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      {I : CategoryTheory.Limits.MulticospanIndex J C} →
        (t : CategoryTheory.Limits.Multifork I) → t ≅ CategoryTheory.Limits.Multifork.ofι I t.pt t.ι ⋯
-- Mathlib.MeasureTheory.Measure.Restrict
MeasurableSet.map_coe_volume : ∀ {α : Type u_2} [inst : MeasureTheory.MeasureSpace α] {s : Set α},
  MeasurableSet s → MeasureTheory.Measure.map Subtype.val MeasureTheory.volume = MeasureTheory.volume.restrict s
-- Init.Data.Vector.Lemmas
/-- Two vectors of constant length vectors are equal iff their flattens coincide.  -/
Vector.eq_iff_flatten_eq : ∀ {α : Type u_1} {n m : ℕ} {xss xss' : Vector (Vector α n) m}, xss = xss' ↔ xss.flatten = xss'.flatten
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_set_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s t : Set β} {a : α}, s ⊆ t → a • s ⊆ a • t
-- Mathlib.Algebra.Ring.Units
Units.divp_sub_divp : ∀ {α : Type u} [inst : CommRing α] (a b : α) (u₁ u₂ : αˣ), a /ₚ u₁ - b /ₚ u₂ = (a * ↑u₂ - ↑u₁ * b) /ₚ (u₁ * u₂)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → k ∉ m₁ \ m₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonTypeDefinitionParams : Lean.ToJson Lean.Lsp.TypeDefinitionParams
-- Mathlib.Topology.Inseparable
stableUnderGeneralization_empty : ∀ {X : Type u_1} [inst : TopologicalSpace X], StableUnderGeneralization ∅
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncOptions.mk.injEq : ∀ (openClose : Bool) (change : Lean.Lsp.TextDocumentSyncKind) (willSave willSaveWaitUntil : Bool)
  (save? : Option Lean.Lsp.SaveOptions) (openClose_1 : Bool) (change_1 : Lean.Lsp.TextDocumentSyncKind)
  (willSave_1 willSaveWaitUntil_1 : Bool) (save?_1 : Option Lean.Lsp.SaveOptions),
  ({ openClose := openClose, change := change, willSave := willSave, willSaveWaitUntil := willSaveWaitUntil,
        save? := save? } =
      { openClose := openClose_1, change := change_1, willSave := willSave_1, willSaveWaitUntil := willSaveWaitUntil_1,
        save? := save?_1 }) =
    (openClose = openClose_1 ∧
      change = change_1 ∧ willSave = willSave_1 ∧ willSaveWaitUntil = willSaveWaitUntil_1 ∧ save? = save?_1)
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.toFun_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N), f.toFun = ⇑f
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₂_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X : C},
  CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F (CategoryTheory.CategoryStruct.id X) = id
-- Mathlib.Data.Seq.Basic
Stream'.Seq.zip_nil_right : ∀ {α : Type u} {s : Stream'.Seq α}, s.zip Stream'.Seq.nil = Stream'.Seq.nil
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.lex_le_iff : ∀ {σ : Type u_1} [inst : LinearOrder σ] [inst_1 : WellFoundedGT σ] {c d : σ →₀ ℕ},
  MonomialOrder.lex.toSyn c ≤ MonomialOrder.lex.toSyn d ↔ toLex c ≤ toLex d
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.mul_of_commute : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f g : Module.End K M}
  [FiniteDimensional K M] [PerfectField K], Commute f g → f.IsSemisimple → g.IsSemisimple → (f * g).IsSemisimple
-- Mathlib.Algebra.Algebra.Prod
AlgHom.snd_prod : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] B) (g : A →ₐ[R] C), (AlgHom.snd R B C).comp (f.prod g) = g
-- Init.Data.List.Erase
List.length_eraseP_le : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, (List.eraseP p l).length ≤ l.length
-- Std.Internal.Do.Triple.Gadget
Std.Internal.Do.assertGadget.eq_1 : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] (name : Lean.Name)
  (as : Pred), Std.Internal.Do.assertGadget name as = pure PUnit.unit
-- Mathlib.Order.Filter.Defs
Filter.filter_eq : ∀ {α : Type u_1} {f g : Filter α}, f.sets = g.sets → f = g
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_eq_of_dvd_sub : ∀ {α : Type u_2} {β : Type u_3} [inst : CommRing α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β} {f g : β → α}
  {a : α}, (∀ x ∈ s, a ∣ f x - g x) → gcd a (s.gcd f) = gcd a (s.gcd g)
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.FunctorsInverting.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {W : CategoryTheory.MorphismProperty C} {F₁ F₂ : W.FunctorsInverting D} {α β : F₁ ⟶ F₂}, α.hom.app = β.hom.app → α = β
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListIfNew.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l toInsert : List ((a : α) × β a)),
  Std.Internal.List.insertListIfNew l toInsert =
    match toInsert with
    | [] => l
    | ⟨k, v⟩ :: tl => Std.Internal.List.insertListIfNew (Std.Internal.List.insertEntryIfNew k v l) tl
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_iff_lowerBound? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBSet α cmp} [Std.TransCmp cmp],
  x ∈ t ↔ ∃ y, t.lowerBound? x = some y ∧ cmp x y = Ordering.eq
-- Mathlib.Data.TypeVec
TypeVec.splitFun_inj : ∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} {f f' : α.drop.Arrow α'.drop}
  {g g' : α.last → α'.last}, TypeVec.splitFun f g = TypeVec.splitFun f' g' → f = f' ∧ g = g'