mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Basic
/-- The `MetaM` monad is a core component of Lean's metaprogramming framework, facilitating the
construction and manipulation of expressions (`Lean.Expr`) within Lean.

It builds on top of `CoreM` and additionally provides:
- A `LocalContext` for managing free variables.
- A `MetavarContext` for managing metavariables.
- A `Cache` for caching results of the key `MetaM` operations.

The key operations provided by `MetaM` are:
- `inferType`, which attempts to automatically infer the type of a given expression.
- `whnf`, which reduces an expression to the point where the outermost part is no longer reducible
  but the inside may still contain unreduced expression.
- `isDefEq`, which determines whether two expressions are definitionally equal, possibly assigning
  meta variables in the process.
- `forallTelescope` and `lambdaTelescope`, which make it possible to automatically move into
  (nested) binders while updating the local context.

The following is a small example that demonstrates how to obtain and manipulate the type of a
`Fin` expression:
```
public import Lean

open Lean Meta

def getFinBound (e : Expr) : MetaM (Option Expr) := do
  let type ← whnf (← inferType e)
  let_expr Fin bound := type | return none
  return bound

def a : Fin 100 := 42

run_meta
  match ← getFinBound (.const ``a []) with
  | some limit => IO.println (← ppExpr limit)
  | none => IO.println "no limit found"
```
 -/
Lean.Meta.MetaM : Type → Type
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.smul : ∀ {S : Type uS} [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] {r : A → A → Prop}
  (k : S) ⦃a b : A⦄, RingQuot.Rel r a b → RingQuot.Rel r (k • a) (k • b)
-- Mathlib.Condensed.Explicit
/-- The condensed object associated to a presheaf on `Profinite` which preserves finite products and
satisfies the equalizer condition.
 -/
Condensed.ofSheafProfinite : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : CompHausᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X profiniteToCompHaus.op) A] →
      (F : CategoryTheory.Functor Profiniteᵒᵖ A) →
        [CategoryTheory.Limits.PreservesFiniteProducts F] →
          CategoryTheory.regularTopology.EqualizerCondition F → Condensed A
-- Mathlib.Order.WithBot
WithBot.denselyOrdered_iff : ∀ {α : Type u_1} [inst : LT α] [NoMinOrder α], DenselyOrdered (WithBot α) ↔ DenselyOrdered α
-- Mathlib.RingTheory.Ideal.Cotangent
/-- `I ⧸ I ^ 2` as an ideal of `R ⧸ I ^ 2`.  -/
Ideal.cotangentIdeal : {R : Type u} → [inst : CommRing R] → (I : Ideal R) → Ideal (R ⧸ I ^ 2)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.plusPlusSheaf_obj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D),
  ((CategoryTheory.plusPlusSheaf J D).obj P).obj = J.sheafify P
-- Mathlib.Order.RelSeries
/-- Every relation series gives a list  -/
RelSeries.toList : {α : Type u_1} → {r : SetRel α α} → RelSeries r → List α
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setIntegral_setAverage : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → E) (s : Set α),
  ∫ (x : α) in s, ⨍ (a : α) in s, f a ∂μ ∂μ = ∫ (x : α) in s, f x ∂μ
-- Init.Data.SInt.Bitwise
Int16.xor_eq_zero_iff : ∀ {a b : Int16}, a ^^^ b = 0 ↔ a = b
-- Mathlib.Analysis.Analytic.Inverse
FormalMultilinearSeries.rightInv.eq_2 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E),
  p.rightInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
/-- Canonical embedding of `SL(2, ℤ)` into `GL(2, ℝ)⁺`.  -/
ModularGroup.coe : Matrix.SpecialLinearGroup (Fin 2) ℤ → ↥(Matrix.GLPos (Fin 2) ℝ)
-- Mathlib.Tactic.Translate.Core
Mathlib.Tactic.Translate.TranslateData.mk.inj : ∀ {ignoreArgsAttr : Lean.NameMapExtension (List ℕ)} {doTranslateAttr : Lean.NameMapExtension Bool}
  {unfoldBoundaries? : Option Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt}
  {translations : Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo} {attrName : Lean.Name}
  {changeNumeral isDual : Bool} {guessNameExt : Mathlib.Tactic.GuessName.GuessNameExt}
  {ignoreArgsAttr_1 : Lean.NameMapExtension (List ℕ)} {doTranslateAttr_1 : Lean.NameMapExtension Bool}
  {unfoldBoundaries?_1 : Option Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaryExt}
  {translations_1 : Lean.NameMapExtension Mathlib.Tactic.Translate.TranslationInfo} {attrName_1 : Lean.Name}
  {changeNumeral_1 isDual_1 : Bool} {guessNameExt_1 : Mathlib.Tactic.GuessName.GuessNameExt},
  { ignoreArgsAttr := ignoreArgsAttr, doTranslateAttr := doTranslateAttr, unfoldBoundaries? := unfoldBoundaries?,
        translations := translations, attrName := attrName, changeNumeral := changeNumeral, isDual := isDual,
        guessNameExt := guessNameExt } =
      { ignoreArgsAttr := ignoreArgsAttr_1, doTranslateAttr := doTranslateAttr_1,
        unfoldBoundaries? := unfoldBoundaries?_1, translations := translations_1, attrName := attrName_1,
        changeNumeral := changeNumeral_1, isDual := isDual_1, guessNameExt := guessNameExt_1 } →
    ignoreArgsAttr = ignoreArgsAttr_1 ∧
      doTranslateAttr = doTranslateAttr_1 ∧
        unfoldBoundaries? = unfoldBoundaries?_1 ∧
          translations = translations_1 ∧
            attrName = attrName_1 ∧ changeNumeral = changeNumeral_1 ∧ isDual = isDual_1 ∧ guessNameExt = guessNameExt_1
-- Std.Time.Duration
Std.Time.Duration.mk.injEq : ∀ (second : Std.Time.Second.Offset) (nano : Std.Time.Nanosecond.Span)
  (proof : second.val ≥ 0 ∧ ↑nano ≥ 0 ∨ second.val ≤ 0 ∧ ↑nano ≤ 0) (second_1 : Std.Time.Second.Offset)
  (nano_1 : Std.Time.Nanosecond.Span) (proof_1 : second_1.val ≥ 0 ∧ ↑nano_1 ≥ 0 ∨ second_1.val ≤ 0 ∧ ↑nano_1 ≤ 0),
  ({ second := second, nano := nano, proof := proof } = { second := second_1, nano := nano_1, proof := proof_1 }) =
    (second = second_1 ∧ nano = nano_1)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_div_div_cancel_right₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {c : G₀}, c ≠ 0 → ∀ (a b : G₀), a / c / (b / c) = a / b
-- Mathlib.FieldTheory.AlgebraicClosure
/-- Let `E / F` be a field extension. If a polynomial `p`
splits in `E`, then it splits in the relative algebraic closure of `F` in `E` already.
 -/
Splits.algebraicClosure : ∀ {F : Type u_1} (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {p : Polynomial F},
  (Polynomial.map (algebraMap F E) p).Splits → (Polynomial.map (algebraMap F ↥(algebraicClosure F E)) p).Splits
-- Mathlib.Algebra.Group.Units.Defs
Units.instMonoid : {α : Type u} → [inst : Monoid α] → Monoid αˣ
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_map_unmop_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' : C} (f : c ⟶ c') (d : D),
  ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D).map f).unmop.app d =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
uliftMultiplesHom_apply_apply : ∀ (M : Type u) [inst : AddMonoid M] (a : M) (x : ULift.{u, 0} ℕ), ((uliftMultiplesHom M) a) x = AddEquiv.ulift x • a
-- Mathlib.CategoryTheory.Sites.Plus
/-- The canonical map from `P` to `J.plusObj P`.
See `toPlusNatTrans` for a functorial version.  -/
CategoryTheory.GrothendieckTopology.toPlus : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type w} →
        [inst_1 : CategoryTheory.Category.{w', w} D] →
          [inst_2 :
              ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X),
                CategoryTheory.Limits.HasMultiequalizer (S.index P)] →
            (P : CategoryTheory.Functor Cᵒᵖ D) →
              [inst_3 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D] → P ⟶ J.plusObj P
-- Lean.Elab.Tactic.Try
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.mkTryEvalSuggestStx : Lean.MVarId → Lean.Meta.Try.Info → Lean.MetaM (Lean.TSyntax `tactic)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.pullbackAwayιIso_hom_SpecMap_awayMap_left : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {f : A} {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m) {m' : ℕ} {g : A} (g_deg : g ∈ 𝒜 m')
  (hm' : 0 < m') {x : A} (hx : x = f * g),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Proj.pullbackAwayιIso 𝒜 f_deg hm g_deg hm' hx).hom
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (HomogeneousLocalization.awayMap 𝒜 g_deg hx))) =
    CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Proj.awayι 𝒜 f f_deg hm)
      (AlgebraicGeometry.Proj.awayι 𝒜 g g_deg hm')
-- Mathlib.Order.Interval.Multiset
Multiset.Ioc_eq_zero_of_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b : α}, b ≤ a → Multiset.Ioc a b = 0
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.natDegree_cubic_le : ∀ {R : Type u} {a b c d : R} [inst : Semiring R],
  (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X +
        Polynomial.C d).natDegree ≤
    3
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
ComplexShape.Embedding.AreComplementary.fromSum.eq_1 : ∀ {ι : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {c : ComplexShape ι} {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  (e₁ : c₁.Embedding c) (e₂ : c₂.Embedding c) (i₁ : ι₁),
  ComplexShape.Embedding.AreComplementary.fromSum e₁ e₂ (Sum.inl i₁) = e₁.f i₁
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_le_toNat : ∀ {c d : Cardinal.{u}}, c ≤ d → d < Cardinal.aleph0 → Cardinal.toNat c ≤ Cardinal.toNat d
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The second projection of a binary fan.  -/
CategoryTheory.Limits.BinaryFan.snd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (s : CategoryTheory.Limits.BinaryFan X Y) →
        ((CategoryTheory.Functor.const (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)).obj s.pt).obj
            { as := CategoryTheory.Limits.WalkingPair.right } ⟶
          (CategoryTheory.Limits.pair X Y).obj { as := CategoryTheory.Limits.WalkingPair.right }
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_rci : ∀ {α β : Type u} {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  [inst_2 : LE α] [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLE α] {xs : Std.Rci α}
  {init : β} {f : α → β → m (ForInStep β)} (inv : Std.Do.Invariant xs.toList β ps),
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := xs.toList, property := ⋯ }, init)⦄
      forIn xs init f ⦃(fun b => inv.1 ({ «prefix» := xs.toList, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
ModuleCat.free_μ_freeMk_tmul_freeMk : ∀ (R : Type u) [inst : CommRing R] {X Y : Type u} (x : X) (y : Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Functor.LaxMonoidal.μ (ModuleCat.free R) X Y))
      (ModuleCat.freeMk x ⊗ₜ[R] ModuleCat.freeMk y) =
    ModuleCat.freeMk (x, y)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.State.mk : String → ℕ → Std.Format.State✝
-- Mathlib.Topology.List
_private.Mathlib.Topology.List.0.List.Vector.elim.match_3.splitter : {α : Type u_1} →
  {n : ℕ} →
    (motive : List.Vector α n → Sort u_2) →
      (x : List.Vector α n) → ((l : List α) → (h : l.length = n) → motive ⟨l, h⟩) → motive x
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_of_mem : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {a : α}, a ∈ s → ∀ (f : α → M), s.mulIndicator f a = f a
-- Aesop.RuleSet.Filter
Aesop.RuleSetNameFilter.all : Aesop.RuleSetNameFilter
-- Mathlib.Tactic.SplitIfs
/-- Splits a single if-then-else expression and then reduces the resulting goals.
Has a similar effect as `SplitIf.splitIfTarget?` or `SplitIf.splitIfLocalDecl?` from
core Lean 4. We opt not to use those library functions so that we can better mimic
the behavior of mathlib3's `split_ifs`.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.splitIf1 : Lean.Expr → Lean.Name → Lean.Elab.Tactic.Location → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive],
  CategoryTheory.Pretriangulated C = CategoryTheory.Pretriangulated C
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry?.eq_3 : ∀ {α : Type u} {β : α → Type v} (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
  (l r r_1 : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minEntry? =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry?
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.SymmStruct.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {ι : Type w}
  {I : CategoryTheory.Limits.MultispanIndex (CategoryTheory.Limits.MultispanShape.prod ι) C}
  {iso : (i j : ι) → I.left (i, j) ≅ I.left (j, i)}
  {iso_hom_fst : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.fst (j, i)) = I.snd (i, j)}
  {iso_hom_snd : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso i j).hom (I.snd (j, i)) = I.fst (i, j)}
  {fst_eq_snd : ∀ (i : ι), I.fst (i, i) = I.snd (i, i)} {iso_1 : (i j : ι) → I.left (i, j) ≅ I.left (j, i)}
  {iso_hom_fst_1 : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso_1 i j).hom (I.fst (j, i)) = I.snd (i, j)}
  {iso_hom_snd_1 : ∀ (i j : ι), CategoryTheory.CategoryStruct.comp (iso_1 i j).hom (I.snd (j, i)) = I.fst (i, j)}
  {fst_eq_snd_1 : ∀ (i : ι), I.fst (i, i) = I.snd (i, i)},
  { iso := iso, iso_hom_fst := iso_hom_fst, iso_hom_snd := iso_hom_snd, fst_eq_snd := fst_eq_snd } =
      { iso := iso_1, iso_hom_fst := iso_hom_fst_1, iso_hom_snd := iso_hom_snd_1, fst_eq_snd := fst_eq_snd_1 } →
    iso = iso_1
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.nndist_eq_iSup : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β]
  {f g : BoundedContinuousFunction α β}, nndist f g = ⨆ x, nndist (f x) (g x)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.mapCycles₂_id_comp_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C)
  (x : ↥(groupHomology.cycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom
        (groupHomology.mapCycles₂ (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ)))
      x =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ (MonoidHom.id G) ψ))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.mapCycles₂ (MonoidHom.id G) φ)) x)
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_cancel_left : ∀ {a : ℤ} (b : ℤ), a ≠ 0 → a * b / a = b
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_apply : ∀ {α : Type u_2} {β : Type u_3} {C : β → Type u_7} [inst : (b : β) → SemilatticeSup (C b)]
  [inst_1 : (b : β) → OrderBot (C b)] (s : Finset α) (f : α → (b : β) → C b) (b : β), s.sup f b = s.sup fun a => f a b
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.map_neighborFinset_induce : ∀ {V : Type u_1} {s : Set V} [inst : DecidablePred fun x => x ∈ s] [inst_1 : Fintype V] {G : SimpleGraph V}
  [inst_2 : DecidableRel G.Adj] [inst_3 : DecidableEq V] (v : ↑s),
  Finset.map (Function.Embedding.subtype fun x => x ∈ s) ((SimpleGraph.induce s G).neighborFinset v) =
    G.neighborFinset ↑v ∩ s.toFinset
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMon_naturality_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X Y : C} [inst_2 : CategoryTheory.AddMonObj M] [inst_3 : CategoryTheory.AddMonObj N]
  (α : CategoryTheory.yonedaAddMonObj M ⟶ CategoryTheory.yonedaAddMonObj N) (f : X ⟶ Y) (g : Y ⟶ M) {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.relabel_id_eq_id : ∀ {L : FirstOrder.Language} {α : Type u'}, FirstOrder.Language.Term.relabel id = id
-- Init.Data.List.Sort.Lemmas
List.length_merge : ∀ {α : Type u_1} (s : α → α → Bool) (l r : List α), (l.merge r s).length = l.length + r.length
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.not_isRoot_C : ∀ {R : Type u} [inst : Semiring R] (r a : R), r ≠ 0 → ¬(Polynomial.C r).IsRoot a
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- `FreeSimplexQuiver.δ i` represents the `i`-th face map `.mk n ⟶ .mk (n + 1)`.  -/
FreeSimplexQuiver.δ : {n : ℕ} → Fin (n + 2) → (FreeSimplexQuiver.mk n ⟶ FreeSimplexQuiver.mk (n + 1))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.getVert_le_length_takeUntil_eq_iff : ∀ {V : Type u} {G : SimpleGraph V} {v w u : V} [inst : DecidableEq V] {n : ℕ} {p : G.Walk v w} (h : u ∈ p.support),
  n ≤ (p.takeUntil u h).length → (p.getVert n = u ↔ n = (p.takeUntil u h).length)
-- Mathlib.Algebra.Lie.Submodule
LieModuleEquiv.range_coe : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] (M : Type u_1) [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {M' : Type u_2} [inst_5 : AddCommGroup M'] [inst_6 : Module R M']
  [inst_7 : LieRingModule L M'] (e : M ≃ₗ⁅R,L⁆ M'), e.range = ⊤
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `inv_mul_le_iff₀'` for a version with multiplication on the other side.  -/
inv_mul_le_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (c⁻¹ * b ≤ a ↔ b ≤ c * a)
-- Mathlib.RingTheory.Bialgebra.Quotient
Bialgebra.Quotient.comul_comp_mkₐ : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Bialgebra R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : (Submodule.restrictScalars R I).IsCoideal],
  (Bialgebra.Quotient.comulAlgHom I).toLinearMap ∘ₗ (Ideal.Quotient.mkₐ R I).toLinearMap =
    TensorProduct.map (Ideal.Quotient.mkₐ R I).toLinearMap (Ideal.Quotient.mkₐ R I).toLinearMap ∘ₗ CoalgebraStruct.comul
-- Mathlib.RingTheory.Trace.Defs
Algebra.trace_self_apply : ∀ {R : Type u_1} [inst : CommRing R] (a : R), (Algebra.trace R R) a = a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_eq_isSome_getKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  t.contains a = (t.getKey? a).isSome
-- Mathlib.RingTheory.FilteredAlgebra.Basic
/-- A convenience constructor for `IsRingFiltration` when the index is the integers.  -/
IsRingFiltration.mk_int : ∀ {R : Type u_2} {σ : Type u_3} [inst : Preorder σ] [inst_1 : Semiring R] [inst_2 : SetLike σ R] (F : ℤ → σ),
  Monotone F → ∀ [SetLike.GradedMonoid F], IsRingFiltration F fun n => F (n - 1)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a `PullbackObjObj` of `f₁ : Arrow C₁` and `f₃ : Arrow C₃`, a `PullbackObjObj` of `f₁` and
`f₃' : Arrow C₃`, and a morphism `f₃ ⟶ f₃'`, this defines a morphism between the induced
pullback maps.  -/
CategoryTheory.Functor.PullbackObjObj.mapArrowRight : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} →
              {f₁ : CategoryTheory.Arrow C₁} →
                {f₃ f₃' : CategoryTheory.Arrow C₃} →
                  (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) →
                    (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom) →
                      (f₃ ⟶ f₃') → (CategoryTheory.Arrow.mk sq₁₃.π ⟶ CategoryTheory.Arrow.mk sq₁₃'.π)
-- Mathlib.RingTheory.Polynomial.ScaleRoots
Polynomial.scaleRoots.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (s : R),
  p.scaleRoots s = ∑ i ∈ p.support, (Polynomial.monomial i) (p.coeff i * s ^ (p.natDegree - i))
-- Mathlib.Combinatorics.Young.YoungDiagram
/-- A Young diagram is a finite collection of cells on the `ℕ × ℕ` grid such that whenever
a cell is present, so are all the ones above and to the left of it. Like matrices, an `(i, j)` cell
is a cell in row `i` and column `j`, where rows are enumerated downward and columns rightward.

Young diagrams are modeled as finite sets in `ℕ × ℕ` that are lower sets with respect to the
standard order on products.  -/
YoungDiagram : Type
-- Init.Data.UInt.Lemmas
USize.toUInt16_toUInt64 : ∀ (n : USize), n.toUInt64.toUInt16 = n.toUInt16
-- Mathlib.SetTheory.Cardinal.Defs
/-- `ℵ₀` is the smallest infinite cardinal. 

Conventions for notations in identifiers:

 * The recommended spelling of `ℵ₀` in identifiers is `aleph0`. -/
Cardinal.aleph0 : Cardinal.{u}
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.isDecompOn : ∀ {X : Type u_1} {G : Type u_2} [inst : SMul G X] (f : Equidecomp X G),
  Equidecomp.IsDecompOn (↑f.toPartialEquiv) f.source f.witness
-- Mathlib.Algebra.DualNumber
/-- Scaling on the left is sent by `DualNumber.lift` to multiplication on the left  -/
DualNumber.lift_smul : ∀ {R : Type u_1} {B : Type u_3} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (fe : { _fe // _fe.2 * _fe.2 = 0 ∧ ∀ (a : A), Commute _fe.2 (_fe.1 a) })
  (a : A) (ad : DualNumber A), (DualNumber.lift fe) (a • ad) = (↑fe).1 a * (DualNumber.lift fe) ad
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
/-- If `f, g` is cosplit, then `G f, G g` is cosplit.  -/
CategoryTheory.map_is_cosplit_pair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.HasSplitEqualizer f g],
  CategoryTheory.HasSplitEqualizer (G.map f) (G.map g)