mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.apply_smulCommClass : ∀ {R : Type u_1} {S : Type u_4} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : SMul S R] [inst_4 : SMul S M] [IsScalarTower S R M], SMulCommClass S (M ≃ₗ[R] M) M
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.instPreservesColimitsOfShapeSheafedSpaceCommRingCatDiscreteForgetToSheafedSpace : ∀ {ι : Type v} [Small.{u, v} ι],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete ι)
    AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntry!.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Inhabited ((a : α) × β a)] (k : α),
  Std.DTreeMap.Internal.Impl.leaf.getEntry! k =
    panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.getEntry!" 147 13
      "Key is not present in map"
-- Mathlib.Topology.Bornology.BoundedOperation
BoundedMul.mk : ∀ {R : Type u_1} [inst : Bornology R] [inst_1 : Mul R],
  (∀ {s t : Set R}, Bornology.IsBounded s → Bornology.IsBounded t → Bornology.IsBounded (s * t)) → BoundedMul R
-- Batteries.Data.Vector.Lemmas
Vector.scanlM.loop.congr_simp : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {n : ℕ} [inst : Monad m] (f f_1 : β → α → m β),
  f = f_1 →
    ∀ (as as_1 : Vector α n),
      as = as_1 →
        ∀ (cur cur_1 : β),
          cur = cur_1 →
            ∀ (i : ℕ) (hi : i ≤ n) (acc acc_1 : Vector β i),
              acc = acc_1 → Vector.scanlM.loop f as cur i hi acc = Vector.scanlM.loop f_1 as_1 cur_1 i hi acc_1
-- Mathlib.Data.Finset.MulAntidiagonal
Finset.antidiagonal_min_add_min : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedCancelAddMonoid α] {s t : Set α}
  (hs : s.IsWF) (ht : t.IsWF) (hns : s.Nonempty) (hnt : t.Nonempty),
  Finset.antidiagonal ⋯ ⋯ (hs.min hns + ht.min hnt) = {(hs.min hns, ht.min hnt)}
-- Mathlib.Analysis.InnerProductSpace.Basic
norm_inner_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖inner 𝕜 x y‖ = ‖inner 𝕜 y x‖
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.getIndicesPos : Lean.Name → Array Lean.Expr → ℕ → ℕ → Array Lean.Expr → Lean.MetaM (List ℕ)
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.of_shrink : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Small.{w, v} M]
  [Module.IsStablyFree R (Shrink.{w, v} M)], Module.IsStablyFree R M
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_two_pow_self : ∀ {n : ℕ}, (2 ^ n).testBit n = true
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toArray_toList : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β}, m.toList.toArray = m.toArray
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_iSup : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {ι : Sort u_7} (f : G →* N) (s : ι → Subgroup G),
  Subgroup.map f (iSup s) = ⨆ i, Subgroup.map f (s i)
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.pow_smul_mem_adjoin_smul : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (r : R)
  (s : Set A) {x : A}, x ∈ Algebra.adjoin R s → ∃ n₀, ∀ n ≥ n₀, r ^ n • x ∈ Algebra.adjoin R (r • s)
-- Mathlib.NumberTheory.Modular
ModularGroup.ρ_mem_fd : UpperHalfPlane.ρ ∈ ModularGroup.fd
-- Init.Prelude
/-- First macro scope available for our frontend  -/
Lean.firstFrontendMacroScope : ℕ
-- Mathlib.RingTheory.WittVector.Compare
/-- `toZModPow` is a family of compatible ring homs. We get this family by composing
`TruncatedWittVector.zmodEquivTrunc` (in right-to-left direction) with `WittVector.truncate`.  -/
WittVector.toZModPow : (p : ℕ) → [hp : Fact (Nat.Prime p)] → (k : ℕ) → WittVector p (ZMod p) →+* ZMod (p ^ k)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- Coefficients of a section `s` of `V` w.r.t. the local frame `b.localFrame e i`.

If x is outside of `e.baseSet`, this returns the junk value 0.  -/
Bundle.Trivialization.localFrameCoeff : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {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] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : FiberBundle F V] →
                                        [inst_13 : VectorBundle 𝕜 F V] →
                                          {ι : Type u_7} →
                                            (e : Bundle.Trivialization F Bundle.TotalSpace.proj) →
                                              [MemTrivializationAtlas e] →
                                                Module.Basis ι 𝕜 F →
                                                  [ContMDiffVectorBundle 1 F V I] → ι → (x : M) → V x →ₗ[𝕜] 𝕜
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.mk : {α : Type u_1} →
  (E : Set α) →
    (IsBase Indep : Set α → Prop) →
      (∀ ⦃I : Set α⦄, Indep I ↔ ∃ B, IsBase B ∧ I ⊆ B) →
        (∃ B, IsBase B) →
          Matroid.ExchangeProperty IsBase →
            (∀ X ⊆ E, Matroid.ExistsMaximalSubsetProperty Indep X) → (∀ (B : Set α), IsBase B → B ⊆ E) → Matroid α
-- Init.Data.Int.Gcd
Int.lcm_neg : ∀ {a b : ℤ}, a.lcm (-b) = a.lcm b
-- Mathlib.Data.List.Destutter
_private.Mathlib.Data.List.Destutter.0.List.destutter.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → ((h : α) → (l : List α) → motive (h :: l)) → (Unit → motive []) → motive x
-- Mathlib.Order.BooleanAlgebra.Basic
_private.Mathlib.Order.BooleanAlgebra.Basic.0.sdiff_sup_self' : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], y \ x ⊔ x = y ⊔ x
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.instRepr : {α : Type u_1} → {cmp : α → α → Ordering} → [Repr α] → Repr (RBTree.RBSet α cmp)
-- Mathlib.Algebra.Group.Equiv.Defs
EmbeddingLike.map_ne_zero_iff : ∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [EmbeddingLike F M N] [ZeroHomClass F M N] {f : F} {x : M}, f x ≠ 0 ↔ x ≠ 0
-- Lean.DocString.Types
/-- The term being described.  -/
Lean.Doc.DescItem.term : {α : Type u} → {β : Type v} → Lean.Doc.DescItem α β → Array α
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_of_empty : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrderBot α] [IsEmpty ι] (f : ι → α), ⨆ i, f i = ⊥
-- Mathlib.Data.Fin.Tuple.Basic
Fin.find_eq_zero : ∀ {n : ℕ} {p : Fin (n + 1) → Prop} [inst : DecidablePred p] (h : ∃ k, p k), Fin.find p h = 0 ↔ p 0
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_comm : ∀ {α : Type u_1} {β : Type u_2} {f : α → β → ENNReal}, ∑' (a : α) (b : β), f a b = ∑' (b : β) (a : α), f a b
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.lTensor_comp_rTensor : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} {Q : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q] (f : M →ₗ[R] P)
  (g : N →ₗ[R] Q), LinearMap.lTensor P g ∘ₗ LinearMap.rTensor N f = TensorProduct.map f g
-- Init.Data.Array.Lex.Lemmas
Array.instDecidableLEOfDecidableEqOfDecidableLT : {α : Type u_1} → [DecidableEq α] → [inst : LT α] → [DecidableLT α] → DecidableLE (Array α)
-- Batteries.Data.UInt
instLawfulOrdUInt64 : Std.LawfulOrd UInt64
-- Mathlib.NumberTheory.Height.NumberField
/-- This is the familiar definition of the multiplicative height on a number field.  -/
NumberField.mulHeight₁_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K),
  Height.mulHeight₁ x = (∏ v, max (v x) 1 ^ v.mult) * ∏ᶠ (v : NumberField.FinitePlace K), max (v x) 1
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_mapIso_inv : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b ≅ g b) (b : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g b) (CategoryTheory.Limits.Sigma.mapIso p).inv =
    CategoryTheory.CategoryStruct.comp (p b).inv (CategoryTheory.Limits.Sigma.ι f b)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
CategoryTheory.NormalEpi.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {f : X ⟶ Y} →
          (W : C) →
            (g : W ⟶ X) →
              (w : CategoryTheory.CategoryStruct.comp g f = 0) →
                CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ f w) →
                  CategoryTheory.NormalEpi f
-- Std.Http.Internal.ChunkedBuffer
/-- Checks whether the buffer is empty.
 -/
Std.Http.Internal.ChunkedBuffer.isEmpty : Std.Http.Internal.ChunkedBuffer → Bool
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- `χ₈'` takes values in `{0, 1, -1}`  -/
ZMod.isQuadratic_χ₈' : ZMod.χ₈'.IsQuadratic
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.getKeyGT : {α : Type u} →
  {β : α → Type v} →
    [inst : Ord α] →
      [Std.TransOrd α] →
        (k : α) → (t : Std.DTreeMap.Internal.Impl α β) → t.Ordered → (∃ a ∈ t, compare a k = Ordering.gt) → α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- **Alias** of `AffineMap.map_vectorSpan`.

---

The affine version of `LinearMap.map_span`.  -/
AffineMap.vectorSpan_image_eq_submodule_map : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : AddCommGroup V₂]
  [inst_5 : Module k V₂] [inst_6 : AddTorsor V₂ P₂] (f : P₁ →ᵃ[k] P₂) {s : Set P₁},
  Submodule.map f.linear (vectorSpan k s) = vectorSpan k (⇑f '' s)
-- Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed
minpoly.IsIntegrallyClosed.isIntegral_iff_leadingCoeff_dvd : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain R] [inst_3 : Algebra R S]
  [IsIntegrallyClosed R] [IsDomain S] [Module.IsTorsionFree R S] {s : S} {p : Polynomial R},
  (Polynomial.aeval s) p = 0 →
    p ≠ 0 →
      (∀ (q : Polynomial R), q.Monic → (Polynomial.aeval s) q = 0 → p.degree ≤ q.degree) →
        (IsIntegral R s ↔ Polynomial.C p.leadingCoeff ∣ p)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.ofTwoCocycle.mk : {R : Type u_5} →
  {L : Type u_6} →
    {M : Type u_7} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    {c : ↥(LieModule.Cohomology.twoCocycle R L M)} → L × M → LieAlgebra.ofTwoCocycle c
-- Mathlib.Algebra.Lie.Ideal
/-- A morphism of Lie algebras `f : L → L'` pushes forward Lie ideals of `L` to Lie ideals of `L'`.

Note that unlike `LieSubmodule.map`, we must take the `lieSpan` of the image. Mathematically
this is because although `f` makes `L'` into a Lie module over `L`, in general the `L` submodules of
`L'` are not the same as the ideals of `L'`.  -/
LieIdeal.map : {R : Type u} →
  {L : Type v} →
    {L' : Type w₂} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieRing L'] →
            [inst_3 : LieAlgebra R L'] → [inst_4 : LieAlgebra R L] → (L →ₗ⁅R⁆ L') → LieIdeal R L → LieIdeal R L'
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ext_getElem?_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] {m₁ m₂ : Std.ExtHashMap α β},
  m₁ = m₂ ↔ ∀ (k : α), m₁[k]? = m₂[k]?
-- Mathlib.Topology.Inseparable
_private.Mathlib.Topology.Inseparable.0.«term_~ᵢ_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.direction_prod_eq : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] {s : AffineSubspace k P} {t : AffineSubspace k Q},
  s ≠ ⊥ → t ≠ ⊥ → (s.prod t).direction = s.direction.prod t.direction
-- Init.Data.Rat.Lemmas
Rat.add_assoc : ∀ (a b c : ℚ), a + b + c = a + (b + c)
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.ext : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} {w₁ w₂ : Monoid.PushoutI.NormalWord d},
  w₁.head = w₂.head → w₁.toList = w₂.toList → w₁ = w₂
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vecMulVec_cons : ∀ {α : Type u} {n : ℕ} {m' : Type uₘ} [inst : NonUnitalNonAssocSemiring α] (v : m' → α) (x : α) (w : Fin n → α),
  Matrix.vecMulVec v (Matrix.vecCons x w) = Matrix.of fun i => v i • Matrix.vecCons x w
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insertWith.eq_def : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (f : α → α) (x : α) (x_1 : Ordnode α),
  Ordnode.insertWith f x x_1 =
    match x_1 with
    | Ordnode.nil => Ordnode.singleton x
    | Ordnode.node sz l y r =>
      match cmpLE x y with
      | Ordering.lt => (Ordnode.insertWith f x l).balanceL y r
      | Ordering.eq => Ordnode.node sz l (f y) r
      | Ordering.gt => l.balanceR y (Ordnode.insertWith f x r)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanIndex_snd : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A] {X : C}
  (data : F.PreOneHypercoverDenseData X) (P : CategoryTheory.Functor C₀ᵒᵖ A) (j : data.multicospanShape.R),
  (data.multicospanIndex P).snd j = P.map (data.p₂ j.snd).op
-- Init.System.IO
/-- Creates a new task that waits for `t` to complete, runs the `IO` action `f` on its result, and then
continues as the resulting task. This new task has priority `prio`.

Running the resulting `BaseIO` action causes this new task to be started eagerly. Unlike pure tasks
created by `Task.spawn`, tasks created by this function will run even if the last reference to the
task is dropped. The `act` should explicitly check for cancellation via `IO.checkCanceled` if it
should be terminated or otherwise react to the last reference being dropped. Because `IO` actions
may throw an exception of type `IO.Error`, the result of the task is an `Except IO.Error α`.
 -/
IO.bindTask : {α : Type u_1} →
  {β : Type} →
    Task α →
      (α → IO (Task (Except IO.Error β))) →
        optParam Task.Priority Task.Priority.default → optParam Bool false → BaseIO (Task (Except IO.Error β))
-- Batteries.Data.List.Interleave
List.reverse_interleave_of_length_eq_length_add_one : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.length = l₂.length + 1 → (l₁.interleave l₂).reverse = l₁.reverse.interleave l₂.reverse
-- Mathlib.Order.Fin.Basic
Fin.strictMono_castAdd : ∀ {n : ℕ} (m : ℕ), StrictMono (Fin.castAdd m)
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The pullback of a finite measure under a map.
If `f` is injective and sends each measurable set to a null-measurable set, then for each
measurable set `s` we have `comap f μ s = μ (f '' s)`.
Otherwise, the pullback is defined to be zero.  -/
MeasureTheory.FiniteMeasure.comap : {Ω : Type u_1} →
  {Ω' : Type u_2} →
    [inst : MeasurableSpace Ω] →
      [inst_1 : MeasurableSpace Ω'] → (Ω → Ω') → MeasureTheory.FiniteMeasure Ω' → MeasureTheory.FiniteMeasure Ω
-- Lean.Declaration
Lean.instBEqDefinitionSafety : BEq Lean.DefinitionSafety
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given an additive monoid homomorphism `g : M →* N` and a function `f : α → M`, the
value of `g` at the sum of `f i` over `i ∈ s` equals the sum of `g (f i)` over `s`.  -/
AddMonoidHom.map_finsum_mem : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {s : Set α}
  (f : α → M) (g : M →+ N), s.Finite → g (∑ᶠ (j : α) (_ : j ∈ s), f j) = ∑ᶠ (i : α) (_ : i ∈ s), g (f i)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.externalCoveringNumber_pos_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  0 < Metric.externalCoveringNumber ε A ↔ A.Nonempty
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- Angles in a vector space are invariant under inversion.  -/
EuclideanGeometry.angle_neg : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (v₁ v₂ v₃ : V),
  EuclideanGeometry.angle (-v₁) (-v₂) (-v₃) = EuclideanGeometry.angle v₁ v₂ v₃
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.lit.injEq : ∀ (v v_1 : Lean.Literal), (Lean.Meta.RefinedDiscrTree.Key.lit v = Lean.Meta.RefinedDiscrTree.Key.lit v_1) = (v = v_1)
-- Lean.Meta.Tactic.Grind.Internalize
/-- Returns `true` if we should use `funCC` for applications of the given constant symbol.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.useFunCongrAtDecl : Lean.Name → Lean.Meta.Grind.GrindM Bool
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.SpecToEquivOfLocalRing_apply_fst : ∀ (X : AlgebraicGeometry.Scheme) (R : CommRingCat) [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X),
  ((AlgebraicGeometry.SpecToEquivOfLocalRing X R) f).fst = f (IsLocalRing.closedPoint ↑R)
-- Mathlib.Topology.Sheaves.Flasque
/-- Given a morphism of sheaves `g: F ⟶ G` and a section `s` of `G(U)`, `Under g s` is comprised of
an open `V` and a section of `F(V)` that maps to `s |_ V` via `g`.  -/
TopCat.Sheaf.IsFlasque.Under : {X : TopCat} →
  {U : TopologicalSpace.Opens ↑X} →
    {F G : TopCat.Sheaf AddCommGrpCat X} → (F ⟶ G) → ↑(G.obj.obj (Opposite.op U)) → Type u
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.UnitLike.instInhabitedState.default : Lean.Meta.Grind.UnitLike.State
-- Init.Data.Order.MinMaxOn
maxOn_eq_left : ∀ {β : Type u_1} {α : Sort u_2} [le : LE β] [inst : DecidableLE β] {f : α → β} {x y : α}, f y ≤ f x → maxOn f x y = x
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The order of the monomial `a*X^n` is `n` if `a ≠ 0`.  -/
MvPowerSeries.weightedOrder_monomial_of_ne_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {d : σ →₀ ℕ} {a : R},
  a ≠ 0 → MvPowerSeries.weightedOrder w ((MvPowerSeries.monomial d) a) = ↑((Finsupp.weight w) d)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey? k = none
-- Mathlib.Order.CountableSupClosed
infClosed_countableInfClosure : ∀ {α : Type u_2} {s : Set α} [inst : SemilatticeInf α], InfClosed (countableInfClosure s)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mk.inj : ∀ {G : Type u_1} {inst : Group G} {inst_1 : TopologicalSpace G} {toSubgroup : Subgroup G}
  {isOpen' : IsOpen toSubgroup.carrier} {toSubgroup_1 : Subgroup G} {isOpen'_1 : IsOpen toSubgroup_1.carrier},
  { toSubgroup := toSubgroup, isOpen' := isOpen' } = { toSubgroup := toSubgroup_1, isOpen' := isOpen'_1 } →
    toSubgroup = toSubgroup_1
-- Mathlib.NumberTheory.Padics.ValuativeRel
Padic.instIsNontrivial : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], ValuativeRel.IsNontrivial ℚ_[p]
-- Mathlib.Data.String.Lemmas
String.length_replicate : ∀ (n : ℕ) (c : Char), (String.replicate n c).length = n
-- Lean.Data.Lsp.CodeActions
/-- Marks that the code action cannot currently be applied.  -/
Lean.Lsp.CodeAction.disabled? : Lean.Lsp.CodeAction → Option Lean.Lsp.CodeActionDisabled
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.step_flatMapAfter : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] {f : β → Std.Iter γ}
  {it₁ : Std.Iter β} {it₂ : Option (Std.Iter γ)},
  (Std.Iter.flatMapAfter f it₁ it₂).step =
    match it₂ with
    | none =>
      match it₁.step with
      | ⟨Std.IterStep.yield it₁' b, h⟩ => Std.PlausibleIterStep.skip (Std.Iter.flatMapAfter f it₁' (some (f b))) ⋯
      | ⟨Std.IterStep.skip it₁', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.flatMapAfter f it₁' none) ⋯
      | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.done ⋯
    | some it₂ =>
      match it₂.step with
      | ⟨Std.IterStep.yield it₂' out, h⟩ => Std.PlausibleIterStep.yield (Std.Iter.flatMapAfter f it₁ (some it₂')) out ⋯
      | ⟨Std.IterStep.skip it₂', h⟩ => Std.PlausibleIterStep.skip (Std.Iter.flatMapAfter f it₁ (some it₂')) ⋯
      | ⟨Std.IterStep.done, h⟩ => Std.PlausibleIterStep.skip (Std.Iter.flatMapAfter f it₁ none) ⋯
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_sub : ∀ (a b : UInt32), (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 4294967296
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.ext_iff : ∀ {basis_hd : ℝ → ℝ} {basis_tl : List (ℝ → ℝ)}
  (ms₁ ms₂ : Tactic.ComputeAsymptotics.MultiseriesExpansion (basis_hd :: basis_tl)),
  ms₁ = ms₂ ↔ ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun
-- Init.Data.SInt.Lemmas
Int32.succ_mul : ∀ {a b : Int32}, (a + 1) * b = a * b + b
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: if countably many closed sets cover the whole space, then their interiors
are dense. Formulated here with `⋃₀`.  -/
dense_sUnion_interior_of_closed : ∀ {X : Type u_1} [inst : TopologicalSpace X] [BaireSpace X] {S : Set (Set X)},
  (∀ s ∈ S, IsClosed s) → S.Countable → ⋃₀ S = Set.univ → Dense (⋃ s ∈ S, interior s)
-- Mathlib.RingTheory.HahnSeries.HEval
PowerSeries.heval_unit : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x : HahnSeries Γ R) (u : (PowerSeries R)ˣ), IsUnit ((PowerSeries.heval x) ↑u)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.single_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M), AddMonoidAlgebra.single m 0 = 0
-- Lean.MonadEnv
Lean.mkConstWithLevelParams : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Lean.Expr
-- Mathlib.Order.Interval.Finset.Box
Finset.box_succ_eq_sdiff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α] [inst_3 : LocallyFiniteOrder α]
  [inst_4 : DecidableEq α] (n : ℕ), Finset.box (n + 1) = Finset.Icc (-↑n.succ) ↑n.succ \ Finset.Icc (-↑n) ↑n
-- Init.Data.List.Sublist
List.instTransSubsetSublist : {α : Type u_1} → Trans Subset List.Sublist Subset
-- Mathlib.RingTheory.SimpleModule.Basic
LinearMap.isCoatom_ker_of_surjective : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsSimpleModule R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑f → IsCoatom f.ker