mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.MLList.Basic
/-- Performs a case distinction on a `MLList` when the motive is a `MLList` as well.
(We need to be in a monadic context to distinguish a nil from a cons.)
 -/
MLList.cases : {m : Type u_1 → Type u_1} →
  {α β : Type u_1} → [Monad m] → MLList m α → (Unit → MLList m β) → (α → MLList m α → MLList m β) → MLList m β
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Key.proj : Lean.Name → ℕ → ℕ → Lean.Meta.LazyDiscrTree.Key
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackFree
/-- The pullback of a free sheaf of modules is a free sheaf of modules.  -/
SheafOfModules.pullbackObjFreeIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] →
                        [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat] →
                          [inst_5 : CategoryTheory.HasWeakSheafify K AddCommGrpCat] →
                            [inst_6 : J.WEqualsLocallyBijective AddCommGrpCat] →
                              [inst_7 : K.WEqualsLocallyBijective AddCommGrpCat] →
                                [F.Final] →
                                  (I : Type u) →
                                    (SheafOfModules.pullback φ).obj (SheafOfModules.free I) ≅ SheafOfModules.free I
-- Std.Data.DTreeMap.Internal.Balanced
Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_zero : Std.DTreeMap.Internal.Impl.BalancedAtRoot 0 0
-- Init.Data.Nat.Fold
Nat.foldRev_succ : ∀ {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n + 1 → α → α) (init : α),
  (n + 1).foldRev f init = n.foldRev (fun i h => f i ⋯) (f n ⋯ init)
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
ofDegLex_symm_eq : ∀ {α : Type u_1}, ofDegLex.symm = toDegLex
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.instSubcanonicalFpqcTopology : AlgebraicGeometry.Scheme.fpqcTopology.Subcanonical
-- Init.Data.List.TakeDrop
List.drop_eq_nil_iff : ∀ {α : Type u_1} {l : List α} {i : ℕ}, List.drop i l = [] ↔ l.length ≤ i
-- Std.Data.DTreeMap.Internal.Balancing
/-- Slower version of `balanceL` which can be used in the complete absence of balancing information
but still assumes that the preconditions of `balanceL` or `balanceL` are satisfied
(otherwise panics).
 -/
Std.DTreeMap.Internal.Impl.balanceL! : {α : Type u} →
  {β : α → Type v} →
    (k : α) → β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.Scheme.Hom.quasiFiniteAt_iff_isOpen_singleton_asFiber : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [AlgebraicGeometry.LocallyOfFiniteType f] {x : ↥X},
  AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x ↔ IsOpen {AlgebraicGeometry.Scheme.Hom.asFiber f x}
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ResolvableCompletionList.isIncomplete : Lean.Lsp.ResolvableCompletionList → Bool
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.restrict_Ioo_eq_restrict_Ico : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : PartialOrder α] {a b : α}, μ.restrict (Set.Ioo a b) = μ.restrict (Set.Ico a b)
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.toHeap.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.BinomialHeap.Imp.HeapNode α → ℕ → Batteries.BinomialHeap.Imp.Heap α → Sort u_2)
  (a : α) (c s : Batteries.BinomialHeap.Imp.HeapNode α) (n : ℕ) (res : Batteries.BinomialHeap.Imp.Heap α)
  (h_1 : (x : ℕ) → (res : Batteries.BinomialHeap.Imp.Heap α) → motive Batteries.BinomialHeap.Imp.HeapNode.nil x res)
  (h_2 :
    (a : α) →
      (c s : Batteries.BinomialHeap.Imp.HeapNode α) →
        (n : ℕ) →
          (res : Batteries.BinomialHeap.Imp.Heap α) → motive (Batteries.BinomialHeap.Imp.HeapNode.node a c s) n res),
  (match Batteries.BinomialHeap.Imp.HeapNode.node a c s, n, res with
    | Batteries.BinomialHeap.Imp.HeapNode.nil, x, res => h_1 x res
    | Batteries.BinomialHeap.Imp.HeapNode.node a c s, n, res => h_2 a c s n res) =
    h_2 a c s n res
-- Mathlib.Algebra.BigOperators.WithTop
WithTop.prod_eq_top : ∀ {ι : Type u_1} {M₀ : Type u_3} [inst : CommMonoidWithZero M₀] [inst_1 : NoZeroDivisors M₀] [inst_2 : Nontrivial M₀]
  [inst_3 : DecidableEq M₀] {s : Finset ι} {f : ι → WithTop M₀} {i : ι},
  i ∈ s → f i = ⊤ → (∀ j ∈ s, f j ≠ 0) → ∏ j ∈ s, f j = ⊤
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Class
Std.Tactic.BVDecide.LRAT.Internal.Formula.performRatAdd : {α : outParam (Type u)} →
  {β : outParam (Type v)} →
    {inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β} →
      {σ : Type w} →
        {inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ} →
          [self : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] →
            σ → β → Std.Sat.Literal α → Array ℕ → Array (ℕ × Array ℕ) → σ × Bool
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- **Alias** of `ModelWithCorners.contDiffOn_extendCoordChange`. -/
OpenPartialHomeomorph.contDiffOn_extend_coord_change : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {n : WithTop ℕ∞} {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H} [inst_5 : ChartedSpace H M],
  e ∈ IsManifold.maximalAtlas I n M →
    e' ∈ IsManifold.maximalAtlas I n M →
      ContDiffOn 𝕜 n (↑(ModelWithCorners.extendCoordChange e e')) (ModelWithCorners.extendCoordChange e e').source
-- Mathlib.ModelTheory.Order
FirstOrder.Language.realize_noTopOrder : ∀ (L : FirstOrder.Language) (M : Type w') [inst : L.IsOrdered] [inst_1 : L.Structure M] [inst_2 : LE M]
  [L.OrderedStructure M] [h : NoTopOrder M], M ⊨ L.noTopOrderSentence
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.ctor.injEq : ∀ (i : Lean.IR.CtorInfo) (ys : Array Lean.IR.Arg) (i_1 : Lean.IR.CtorInfo) (ys_1 : Array Lean.IR.Arg),
  (Lean.IR.Expr.ctor i ys = Lean.IR.Expr.ctor i_1 ys_1) = (i = i_1 ∧ ys = ys_1)
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_above_le`. -/
Ideal.inertiaDeg'_above_le : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] (q : Ideal S) (r : Ideal T)
  [r.IsPrime] [r.LiesOver q] [Module.Finite R T], r.inertiaDeg S ≤ r.inertiaDeg R
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_1.splitter : (motive : Lean.Name → Sort u_1) →
  (x : Lean.Name) →
    ((pre : Lean.Name) → (str : String) → motive (pre.str str)) →
      ((x : Lean.Name) → (∀ (pre : Lean.Name) (str : String), x = pre.str str → False) → motive x) → motive x
-- Mathlib.Data.Fin.VecNotation
Matrix.vecCons_const : ∀ {α : Type u} {n : ℕ} (a : α), (Matrix.vecCons a fun x => a) = fun x => a
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.restrictScalars : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {𝕜' : Type u_9}
  [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : NormedSpace 𝕜' E]
  [inst_8 : IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜' E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → HasFPowerSeriesOnBall f (FormalMultilinearSeries.restrictScalars 𝕜 p) x r
-- Mathlib.Data.List.Pi
/-- Given `f` a function whose domain is `i :: l`, get its value at `i`.  -/
List.Pi.head : {ι : Type u_1} → {α : ι → Sort u_2} → {i : ι} → {l : List ι} → ((j : ι) → j ∈ i :: l → α j) → α i
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_set_mk : ∀ {R : Type u} [inst : NonAssocRing R] (S : Subsemiring R) (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier),
  ↑{ toSubsemiring := S, neg_mem' := h } = ↑S
-- Mathlib.Order.PartialSups
partialSups_apply : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  (f : ι → α) (i : ι), (partialSups f) i = (Finset.Iic i).sup' ⋯ f
-- Mathlib.Algebra.Exact.Basic
/-- **Alias** of the forward direction of `Function.Exact.iff_linearMap_rangeRestrict`.

---

Two maps `f : M →ₗ[R] N` and `g : N →ₗ[R] P` are exact if and only if the induced maps
`LinearMap.range f → N → LinearMap.range g` are exact.  -/
Function.Exact.linearMap_rangeRestrict : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P},
  Function.Exact ⇑f ⇑g → Function.Exact ⇑f.range.subtype ⇑g.rangeRestrict
-- Mathlib.Algebra.Colimit.Ring
/-- The direct limit constructed as a quotient of the free commutative ring is isomorphic to
the direct limit constructed as a quotient of the disjoint union.  -/
Ring.DirectLimit.ringEquiv : {ι : Type u_1} →
  [inst : Preorder ι] →
    (G : ι → Type u_2) →
      [inst_1 : (i : ι) → CommRing (G i)] →
        (f' : (i j : ι) → i ≤ j → G i →+* G j) →
          [inst_2 : DirectedSystem G fun i j h => ⇑(f' i j h)] →
            [inst_3 : IsDirectedOrder ι] →
              [Nonempty ι] → (Ring.DirectLimit G fun x1 x2 x3 => ⇑(f' x1 x2 x3)) ≃+* DirectLimit G f'
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.encode : {α : Type u} →
  {inst : LE α} →
    {inst_1 : LT α} →
      {β : outParam (Type v)} →
        {inst_2 : LE β} →
          {inst_3 : LT β} →
            {inst_4 : Std.PRange.UpwardEnumerable β} →
              {inst_5 : Std.PRange.LawfulUpwardEnumerable β} →
                {inst_6 : Std.PRange.LawfulUpwardEnumerableLE β} →
                  {inst_7 : Std.PRange.LawfulUpwardEnumerableLT β} → [self : HasModel✝ α β] → α → β
-- Lean.Meta.LazyDiscrTree
/-- Find values that match `e` in `d`.

The results are ordered so that the longest matches in terms of number of
non-star keys are first with ties going to earlier operators first.
 -/
Lean.Meta.LazyDiscrTree.getMatch : {α : Type} →
  Lean.Meta.LazyDiscrTree α → Lean.Expr → Lean.MetaM (Lean.Meta.LazyDiscrTree.MatchResult α × Lean.Meta.LazyDiscrTree α)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_omega0 : ∀ {o : Ordinal.{u_4}}, o < Ordinal.omega0 ↔ ∃ n, o = ↑n
-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.transOrd : ∀ {α : Type u} (self : Std.Packages.LinearPreorderOfOrdArgs α), Std.TransOrd α
-- Mathlib.Algebra.Order.IsBotOne
/-- **Alias** of `one_lt_of_ne_one`.

---

**Alias** of the reverse direction of `one_lt_iff_ne_one`. -/
Ne.one_lt : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α], a ≠ 1 → 1 < a
-- Init.Data.Fin.Fold
/-- Combine all the values that can be represented by `Fin n` with an initial value, starting at `0` and
nesting to the left.

Example:
 * `Fin.foldl 3 (· + ·.val) (0 : Nat) = ((0 + (0 : Fin 3).val) + (1 : Fin 3).val) + (2 : Fin 3).val`
 -/
Fin.foldl : {α : Sort u_1} → (n : ℕ) → (α → Fin n → α) → α → α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- If `s` is a countable set, then the measure of its preimage can be found as the sum of measures
of the fibers `f ⁻¹' {y}`.  -/
MeasureTheory.tsum_measure_preimage_singleton : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set β},
  s.Countable → ∀ {f : α → β}, (∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) → ∑' (b : ↑s), μ (f ⁻¹' {↑b}) = μ (f ⁻¹' s)
-- Batteries.Data.PairingHeap
/-- `O(1)`. Merge the contents of two heaps.  -/
Batteries.PairingHeap.merge : {α : Type u} →
  {le : α → α → Bool} → Batteries.PairingHeap α le → Batteries.PairingHeap α le → Batteries.PairingHeap α le
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- The sum of a locally finite collection of sections is `C^k` at `x` iff each section is.  -/
ContMDiffAt.sum_section_of_locallyFinite : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {x₀ : M} {ι : Type u_7} {t : ι → (x : M) → V x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t i x⟩) x₀) →
      ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, ∑' (i : ι), t i x⟩) x₀
-- Mathlib.Topology.Defs.Filter
/-- `x` specializes to `y` (notation: `x ⤳ y`) if either of the following equivalent properties
hold:

* `𝓝 x ≤ 𝓝 y`; this property is used as the definition;
* `pure x ≤ 𝓝 y`; in other words, any neighbourhood of `y` contains `x`;
* `y ∈ closure {x}`;
* `closure {y} ⊆ closure {x}`;
* for any closed set `s` we have `x ∈ s → y ∈ s`;
* for any open set `s` we have `y ∈ s → x ∈ s`;
* `y` is a cluster point of the filter `pure x = 𝓟 {x}`.

This relation defines a `Preorder` on `X`. If `X` is a T₀ space, then this preorder is a partial
order. If `X` is a T₁ space, then this partial order is trivial : `x ⤳ y ↔ x = y`.  -/
Specializes : {X : Type u_1} → [TopologicalSpace X] → X → X → Prop
-- Mathlib.Tactic.Widget.StringDiagram
/-- Add constructor `tp v := nm (vs)` to the substance program.  -/
Mathlib.Tactic.Widget.StringDiagram.addConstructor : String →
  Mathlib.Tactic.Widget.StringDiagram.PenroseVar →
    String → List Mathlib.Tactic.Widget.StringDiagram.PenroseVar → ProofWidgets.Penrose.DiagramBuilderM Unit
-- Init.Conv
/-- `rfl` closes one conv goal "trivially", by using reflexivity
(that is, no rewriting).  -/
Lean.Parser.Tactic.Conv.convRfl : Lean.ParserDescr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiff.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → ContDiff ℝ n fun x => Real.sin (f x)
-- Lean.DocString.Syntax
Lean.Doc.Syntax.arg_ident : Lean.ParserDescr
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.IsStableUnderComposition.op : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  [P.IsStableUnderComposition], P.op.IsStableUnderComposition
-- Init.Data.UInt.Lemmas
UInt64.toUInt32_neg : ∀ (a : UInt64), (-a).toUInt32 = -a.toUInt32
-- Aesop.Tree.Data
/-- The forward state reflects the local context of the current goal. Before
normalisation, this is the local context of `preNormGoal`; after normalisation,
it is the local context of the post-normalisation goal (unless normalisation
solved the goal, in which case the forward state is undetermined).  -/
Aesop.GoalData.forwardState : {Rapp MVarCluster : Type} → Aesop.GoalData Rapp MVarCluster → Aesop.ForwardState
-- Mathlib.CategoryTheory.MorphismProperty.Ind
CategoryTheory.MorphismProperty.exists_hom_of_isFinitelyPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : CategoryTheory.SmallCategory J]
  [CategoryTheory.IsFiltered J] {D : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone D}
  (hc : CategoryTheory.Limits.IsColimit c) {X A : C} {p : X ⟶ A},
  CategoryTheory.MorphismProperty.isFinitelyPresentable C p →
    ∀ (s : (CategoryTheory.Functor.const J).obj X ⟶ D) (f : A ⟶ c.pt),
      (∀ (j : J), CategoryTheory.CategoryStruct.comp (s.app j) (c.ι.app j) = CategoryTheory.CategoryStruct.comp p f) →
        ∃ j q, CategoryTheory.CategoryStruct.comp p q = s.app j ∧ CategoryTheory.CategoryStruct.comp q (c.ι.app j) = f
-- Mathlib.Algebra.Order.Monoid.Unbundled.OrderDual
OrderDual.addLeftStrictMono : ∀ {α : Type u} [inst : LT α] [inst_1 : Add α] [c : AddLeftStrictMono α], AddLeftStrictMono αᵒᵈ
-- Mathlib.Algebra.BigOperators.Finprod
finsum_apply : ∀ {N : Type u_6} [inst : AddCommMonoid N] {α : Type u_7} {ι : Type u_8} {f : ι → α → N},
  Function.HasFiniteSupport f → ∀ (a : α), (∑ᶠ (i : ι), f i) a = ∑ᶠ (i : ι), f i a
-- Batteries.Data.List.Lemmas
List.dropPrefix?.eq_3 : ∀ {α : Type u_1} [inst : BEq α] (a : α) (as : List α) (b : α) (bs : List α),
  (a :: as).dropPrefix? (b :: bs) = if (a == b) = true then as.dropPrefix? bs else none
-- Mathlib.Algebra.DirectSum.Decomposition
/-- A convenience method to construct a decomposition from an `LinearMap`, such that the proofs
of left and right inverse can be constructed via `ext`.  -/
DirectSum.Decomposition.ofLinearMap : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : DecidableEq ι] →
        [inst_1 : Semiring R] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              (ℳ : ι → Submodule R M) →
                (decompose : M →ₗ[R] DirectSum ι fun i => ↥(ℳ i)) →
                  DirectSum.coeLinearMap ℳ ∘ₗ decompose = LinearMap.id →
                    decompose ∘ₗ DirectSum.coeLinearMap ℳ = LinearMap.id → DirectSum.Decomposition ℳ
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.nonnegg_neg_pos : ∀ {c d a b : ℕ}, Zsqrtd.Nonnegg c d (-↑a) ↑b ↔ Zsqrtd.SqLe a d b c
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.lowerClosure_subset_closure : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] {s : Set α} [Topology.IsScott α Set.univ],
  ↑(lowerClosure s) ⊆ closure s
-- Mathlib.Tactic.Ring.NamePowerVars
/-- The command `name_power_vars` names variables in
`MvPowerSeries (Fin n) R` for the appropriate value of `n`.
The notation introduced by this command is local.

Usage:

```lean
variable (R : Type) [CommRing R]

name_power_vars X, Y, Z over R

#check Y -- Y : MvPowerSeries (Fin 3) R
```
 -/
Mathlib.Tactic.elabNamePowerSeriesVariablesOver : Lean.Elab.Command.CommandElab
-- Lean.Parser.Term
Lean.Parser.Term.letOpts : Lean.Parser.Parser
-- Mathlib.SetTheory.ZFC.Basic
/-- The image of a (definable) ZFC set function  -/
ZFSet.image : (f : ZFSet.{u_1} → ZFSet.{u_1}) → [ZFSet.Definable₁ f] → ZFSet.{u_1} → ZFSet.{u_1}
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.IsEquiv.refl : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : LinearOrderedAddCommMonoidWithTop Γ₀] [inst_1 : Ring R]
  {v : AddValuation R Γ₀}, v.IsEquiv v
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.fac : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} (self : W₁.MapFactorizationData W₂ f), CategoryTheory.CategoryStruct.comp self.i self.p = f
-- Mathlib.Order.InitialSeg
InitialSeg.transPrincipal.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → α → Prop} {s : β → β → Prop} {t : γ → γ → Prop}
  [inst : IsWellOrder β s] [inst_1 : IsTrans γ t] (f : InitialSeg r s) (g : PrincipalSeg s t),
  f.transPrincipal g =
    match f.principalSumRelIso with
    | Sum.inl f' => f'.trans g
    | Sum.inr f' => PrincipalSeg.relIsoTrans f' g
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.mk_right_unitor_hom : ∀ {B : Type u} [inst : Quiver B] {a b : CategoryTheory.FreeBicategory B} (f : a ⟶ b),
  Quot.mk CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.right_unitor f) =
    (CategoryTheory.Bicategory.rightUnitor f).hom
-- Mathlib.Topology.Compactness.Compact
Bornology.inCompact.isBounded_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, Bornology.IsBounded s ↔ ∃ t, IsCompact t ∧ s ⊆ t
-- Mathlib.Algebra.Lie.Weights.Linear
/-- A weight of a Lie module, bundled as a linear map.  -/
LieModule.Weight.toLinear : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [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] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      [LieModule.LinearWeights R L M] → LieModule.Weight R L M → L →ₗ[R] R
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.isAcyclic_iff_subsingleton_path : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsAcyclic ↔ ∀ (u v : V), Subsingleton (G.Path u v)
-- Init.Data.Vector.Lemmas
Vector.getElem?_replicate_of_lt : ∀ {α : Type u_1} {a : α} {n i : ℕ}, i < n → (Vector.replicate n a)[i]? = some a
-- Mathlib.RingTheory.Henselian
HenselianRing.mk : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R},
  I ≤ ⊥.jacobson →
    (∀ (f : Polynomial R),
        f.Monic →
          ∀ (a₀ : R),
            Polynomial.eval a₀ f ∈ I →
              IsUnit ((Ideal.Quotient.mk I) (Polynomial.eval a₀ (Polynomial.derivative f))) →
                ∃ a, f.IsRoot a ∧ a - a₀ ∈ I) →
      HenselianRing R I
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- `ζ - 1` is prime if `p ≠ 2` and `ζ` is a primitive `p ^ (k + 1)`-th root of unity.
See `zeta_sub_one_prime` for a general statement.  -/
IsPrimitiveRoot.zeta_sub_one_prime_of_ne_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))), p ≠ 2 → Prime (hζ.toInteger - 1)
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_mul_comm : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_6} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : AddCommMonoid R]
  [inst_3 : CommMagma R] (A : Matrix m n R) (B : Matrix n m R), (A * B).trace = (B * A).trace
-- Lean.Meta.InferType
/-- Return type for the auxiliary function `isArrowProposition'`  -/
_private.Lean.Meta.InferType.0.Lean.Meta.ArrowPropResult : Type
-- Mathlib.Analysis.InnerProductSpace.JointEigenspace
/-- If A and B are commuting symmetric operators acting on a finite-dimensional inner product space,
then the simultaneous eigenspaces of A and B exhaust the space.  -/
LinearMap.IsSymmetric.iSup_iSup_eigenspace_inf_eigenspace_eq_top_of_commute : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E],
  A.IsSymmetric → B.IsSymmetric → Commute A B → ⨆ α, ⨆ γ, Module.End.eigenspace A α ⊓ Module.End.eigenspace B γ = ⊤
-- Mathlib.Algebra.Category.ModuleCat.EpiMono
ModuleCat.forget_preservesMonomorphisms : ∀ {R : Type u} [inst : Ring R], (CategoryTheory.forget (ModuleCat R)).PreservesMonomorphisms
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ),
  Polynomial.derivative (Polynomial.X ^ n) = Polynomial.C ↑n * Polynomial.X ^ (n - 1)
-- Mathlib.Order.Bounds.Basic
mem_lowerBounds_iff_subset_Ici : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a : α}, a ∈ lowerBounds s ↔ s ⊆ Set.Ici a
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₁_shape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂), ¬c₁₂.Rel i₁₂ i₁₂' → K.D₁ c₁₂ i₁₂ i₁₂' = 0
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_right : ∀ {R : Type u} [inst : CommSemiring R] {x y z : R}, IsCoprime x y → IsCoprime x z → IsCoprime x (y * z)