mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Extra
/-- The parser `hygieneInfo` parses no text, but creates a `hygieneInfoKind` node
containing an anonymous identifier as if it were parsed at the current position.
This identifier is modified by syntax quotations to add macro scopes like a regular identifier.

This is used to implement `have := ...` syntax: the `hygieneInfo` between the `have` and `:=`
collects macro scopes, which we can apply to `this` when expanding to `have this := ...`.
See [the language reference](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=macro-hygiene) for more information about
macro hygiene.

This is also used to implement cdot functions such as `(1 + ·)`. The opening parenthesis contains
a `hygieneInfo` node as does the cdot, which lets cdot expansion hygienically associate parentheses to cdots.

This parser has arity 1: it produces a `hygieneInfoKind` node containing an anonymous `Syntax.ident`.
You can use `HygieneInfo.mkIdent` to create an `Ident` from the syntax object,
but you can also use `TSyntax.getHygieneInfo` to get the raw name from the identifier.  -/
Lean.Parser.hygieneInfo : Lean.Parser.Parser
-- Mathlib.Algebra.GCDMonoid.PUnit
PUnit.instStrongNormalizedGCDMonoid : StrongNormalizedGCDMonoid PUnit.{u_1 + 1}
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β}, (t.containsThenInsertIfNew k v).2 = t.insertIfNew k v
-- Mathlib.Analysis.Normed.Module.Connected
/-- In a real vector space of dimension `> 1`, the complement of any countable set is path
connected.  -/
Set.Countable.isPathConnected_compl_of_one_lt_rank : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E], 1 < Module.rank ℝ E → ∀ {s : Set E}, s.Countable → IsPathConnected sᶜ
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_coeff_nilRank_ne_zero : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) [inst_9 : Module.Finite R L] [inst_10 : Module.Free R L] [Nontrivial R],
  (φ.polyCharpoly b).coeff φ.nilRank ≠ 0
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
/-- Given an ideal `𝓟` of a commutative semiring `R`, we say that a polynomial `f : R[X]`
is *Eisenstein at `𝓟`* if `f.leadingCoeff ∉ 𝓟`, `∀ n, n < f.natDegree → f.coeff n ∈ 𝓟` and
`f.coeff 0 ∉ 𝓟 ^ 2`.  -/
Polynomial.IsEisensteinAt : {R : Type u} → [inst : CommSemiring R] → Polynomial R → Ideal R → Prop
-- Mathlib.RingTheory.ChainOfDivisors
DivisorChain.eq_second_of_chain_of_prime_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p q r : Associates M} {n : ℕ},
  n ≠ 0 →
    ∀ {c : Fin (n + 1) → Associates M},
      StrictMono c → (∀ {r : Associates M}, r ≤ q ↔ ∃ i, r = c i) → Prime p → r ∣ q → p ∣ r → p = c 1
-- Mathlib.Data.Matrix.Block
/-- Given a matrix whose row and column indexes are sum types, we can extract the corresponding
"bottom right" submatrix.  -/
Matrix.toBlocks₂₂ : {l : Type u_1} →
  {m : Type u_2} → {n : Type u_3} → {o : Type u_4} → {α : Type u_12} → Matrix (n ⊕ o) (l ⊕ m) α → Matrix o m α
-- Mathlib.Data.Vector.Defs
/-- The length of a vector.  -/
List.Vector.length : {α : Type u_1} → {n : ℕ} → List.Vector α n → ℕ
-- Mathlib.Analysis.InnerProductSpace.SingularValues
_private.Mathlib.Analysis.InnerProductSpace.SingularValues.0.LinearMap.singularValues.eq_1 : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F),
  T.singularValues = Finsupp.embDomain Fin.valEmbedding (Finsupp.ofSupportFinite (fun i => √(⋯.eigenvalues ⋯ i)) ⋯)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w)
  (curr : ℕ) (hcurr : curr ≤ w) (cin : aig.Ref) (s : aig.RefVec curr),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s =
    if hidx : curr < w then
      have lin := lhs.get curr hidx;
      have rin := rhs.get curr hidx;
      have res := Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdder aig { lhs := lin, rhs := rin, cin := cin };
      let aig_1 := res.aig;
      have outRef := res.out;
      have carryRef := res.cout;
      have s := s.cast ⋯;
      have lhs := lhs.cast ⋯;
      have rhs := rhs.cast ⋯;
      have s := s.push outRef;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig_1 lhs rhs (curr + 1) ⋯ carryRef s
    else
      have hcurr := ⋯;
      { aig := aig, vec := hcurr ▸ s }
-- Init.Grind.Module.Basic
Lean.Grind.IntModule.zsmul_neg : ∀ {M : Type u} [inst : Lean.Grind.IntModule M] (n : ℤ) (a : M), n • -a = -(n • a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_eq_iff_mem_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp],
  t.WF → t.isEmpty = false → ∀ {km fallback : α}, t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.mk.sizeOf_spec : ∀ (stx : Lean.TSyntax `Lean.Parser.Command.declModifiers)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)) (visibility : Lean.Elab.Visibility)
  (isProtected : Bool) (computeKind : Lean.Elab.ComputeKind) (recKind : Lean.Elab.RecKind) (isUnsafe : Bool)
  (attrs : Array Lean.Elab.Attribute),
  sizeOf
      { stx := stx, docString? := docString?, visibility := visibility, isProtected := isProtected,
        computeKind := computeKind, recKind := recKind, isUnsafe := isUnsafe, attrs := attrs } =
    1 + sizeOf stx + sizeOf docString? + sizeOf visibility + sizeOf isProtected + sizeOf computeKind + sizeOf recKind +
        sizeOf isUnsafe +
      sizeOf attrs
-- Mathlib.Analysis.Convex.Function
/-- A function `-f` is concave iff `f` is convex.  -/
neg_concaveOn_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : SMul 𝕜 E] [inst_7 : Module 𝕜 β]
  {s : Set E} {f : E → β}, ConcaveOn 𝕜 s (-f) ↔ ConvexOn 𝕜 s f
-- Mathlib.Computability.TuringMachine.Tape
Turing.instCoeFunPointedMapForall : {Γ : Type u_1} →
  {Γ' : Type u_2} → [inst : Inhabited Γ] → [inst_1 : Inhabited Γ'] → CoeFun (Turing.PointedMap Γ Γ') fun x => Γ → Γ'
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.SameKeys.size_eq : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1} [Ord α] {t : Std.DTreeMap.Internal.Impl α β}
  {t' : Std.DTreeMap.Internal.Impl α β'}, t.SameKeys t' → t.size = t'.size
-- Mathlib.Topology.Closure
/-- **Alias** of `self_sdiff_frontier`. -/
self_diff_frontier : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), s \ frontier s = interior s
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
Array.toList_iterFromIdxM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} [LawfulMonad m] {array : Array β} {pos : ℕ},
  (array.iterFromIdxM m pos).toList = pure (List.drop pos array.toList)
-- Mathlib.Algebra.WithConv
WithConv.instAddMonoid : {A : Type u_2} → [AddMonoid A] → AddMonoid (WithConv A)
-- Init.Data.String.Decode
ByteArray.add_utf8Size_utf8DecodeChar_le_size : ∀ {b : ByteArray} {i : ℕ} {h : (b.utf8DecodeChar? i).isSome = true}, i + (b.utf8DecodeChar i h).utf8Size ≤ b.size
-- Mathlib.RingTheory.Ideal.Quotient.Operations
/-- The natural algebra isomorphism `(A / I) / J' → (A / J) / I'`,
where `J'` (resp. `I'`) is the projection of `J` in `A / I` (resp. `I` in `A / J`).  -/
DoubleQuot.quotQuotEquivCommₐ : (R : Type u) →
  {A : Type u_1} →
    [inst : CommSemiring R] →
      [inst_1 : CommRing A] →
        [inst_2 : Algebra R A] →
          (I J : Ideal A) →
            ((A ⧸ I) ⧸ Ideal.map (Ideal.Quotient.mkₐ R I) J) ≃ₐ[R] (A ⧸ J) ⧸ Ideal.map (Ideal.Quotient.mkₐ R J) I
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight_cons_cons_cons_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {n : ℕ} (a b : K) (x : Fin n → K),
  Height.mulHeight (Matrix.vecCons a (Matrix.vecCons b (Matrix.vecCons 0 x))) =
    Height.mulHeight (Matrix.vecCons a (Matrix.vecCons b x))
-- Std.Time.Time.PlainTime
/-- Creates a `PlainTime` value from the provided hours, minutes, seconds and nanoseconds components.
 -/
Std.Time.PlainTime.ofHourMinuteSecondsNano : Std.Time.Hour.Ordinal →
  Std.Time.Minute.Ordinal → Std.Time.Second.Ordinal true → Std.Time.Nanosecond.Ordinal → Std.Time.PlainTime
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
WittVector.RecursionMain.succNthVal_spec' : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : IsAlgClosed k]
  (n : ℕ) (a₁ a₂ : WittVector p k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0),
  WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) +
        a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      WittVector.nthRemainder p n (fun v => bs v ^ p) (WittVector.truncateFun (n + 1) a₁) =
    WittVector.RecursionMain.succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) +
        a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
      WittVector.nthRemainder p n bs (WittVector.truncateFun (n + 1) a₂)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsLittleOTVS.isBigOTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F},
  f =o[𝕜; l] g → f =O[𝕜; l] g
-- Lean.Expr
Lean.instReprFVarId : Repr Lean.FVarId
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.next?.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.nonempty_mk_iff : ∀ {x : PSet.{u_1}}, (ZFSet.mk x).Nonempty ↔ x.Nonempty
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- Given a prime ideal `P`, the typeclass `IsLocalization.AtPrime S P` states that `S` is
isomorphic to the localization of `R` at the complement of `P`.  -/
IsLocalization.AtPrime : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) → [inst_1 : CommSemiring S] → [Algebra R S] → (P : Ideal R) → [hp : P.IsPrime] → Prop
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- The language of rings contains the operations `(+,*,-,0,1)`  -/
FirstOrder.Language.ring : FirstOrder.Language
-- Mathlib.Topology.MetricSpace.CoveringNumbers
/-- A finite internal `ε`-cover of a set `A` by closed balls with minimal cardinality.
It is defined as the empty set if no such finite cover exists.  -/
Metric.minimalCover : {X : Type u_1} → [PseudoEMetricSpace X] → NNReal → Set X → Set X
-- Mathlib.CategoryTheory.Extensive
/-- If `C` has pullbacks and is finitary (pre-)extensive, pullbacks distribute over finite
coproducts, i.e., `∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ)`.
For a variant, see `FinitaryPreExtensive.isIso_sigmaDesc_map`.  -/
CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.FinitaryPreExtensive C] {ι : Type u_1} {ι' : Type u_2} [inst_3 : Finite ι]
  [inst_4 : Finite ι'] {S : C} {X : ι → C} {Y : ι' → C} (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S),
  CategoryTheory.IsPullback
    (CategoryTheory.Limits.Sigma.desc fun p =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (f p.1) (g p.2))
        (CategoryTheory.Limits.Sigma.ι X p.1))
    (CategoryTheory.Limits.Sigma.desc fun p =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (f p.1) (g p.2))
        (CategoryTheory.Limits.Sigma.ι Y p.2))
    (CategoryTheory.Limits.Sigma.desc f) (CategoryTheory.Limits.Sigma.desc g)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inl_inl_pushoutLeftPushoutInrIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g')
        (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom) =
    CategoryTheory.Limits.pushout.inl f (CategoryTheory.CategoryStruct.comp g g')
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- **Alias** of `CuspForm.discriminant`.

---

The modular discriminant `Δ` as a cusp form of weight 12 and level 1.  -/
ModularForm.discriminantCuspForm : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
-- Lean.Meta.LazyDiscrTree
_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.getChildNgen.match_1.eq_1 : ∀ (motive : Lean.NameGenerator × Lean.NameGenerator → Sort u_1) (cngen ngen : Lean.NameGenerator)
  (h_1 : (cngen ngen : Lean.NameGenerator) → motive (cngen, ngen)),
  (match (cngen, ngen) with
    | (cngen, ngen) => h_1 cngen ngen) =
    h_1 cngen ngen
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_inv_conjugation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X X' Y Y' Z Z' : C} (f : X ⟶ X') (g : Y ⟶ Y') (h : Z ⟶ Z'),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
        (CategoryTheory.MonoidalCategoryStruct.associator X' Y' Z').hom)
-- Mathlib.Data.Set.Function
Set.SurjOn.invOn_invFunOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} [inst : Nonempty α],
  Set.SurjOn f s t → Set.InvOn (Function.invFunOn f s) f (Function.invFunOn f s '' t) t
-- Std.Time.Date.Unit.Day
Std.Time.Day.instDecidableEqOffset : DecidableEq Std.Time.Day.Offset
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k k' : α} {f : β k → β k}
  (l : List ((a : α) × β a)),
  Std.Internal.List.DistinctKeys l →
    ∀ (h : Std.Internal.List.containsKey k' (Std.Internal.List.modifyKey k f l) = true),
      Std.Internal.List.getKey k' (Std.Internal.List.modifyKey k f l) h =
        if (k == k') = true then k else Std.Internal.List.getKey k' l ⋯
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.fold.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (h_1 : Unit → motive RBTree.RBNode.nil)
  (h_2 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.node c l v r)),
  (match RBTree.RBNode.nil with
    | RBTree.RBNode.nil => h_1 ()
    | RBTree.RBNode.node c l v r => h_2 c l v r) =
    h_1 ()
-- Mathlib.Analysis.Convex.Topology
subset_closedConvexHull : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] {s : Set E}, s ⊆ (closedConvexHull 𝕜) s
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.norm_compContinuous_linearIsometry_le : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →ₗᵢ[𝕜] E₁ i),
  ‖g.compContinuousLinearMap fun i => (f i).toContinuousLinearMap‖ ≤ ‖g‖
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.mem_carrier : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] {s : NonUnitalStarSubalgebra R A} {x : A}, x ∈ s.carrier ↔ x ∈ s
-- Lean.Parser.Extension
Lean.Parser.getCategory : Lean.Parser.ParserCategories → Lean.Name → Option Lean.Parser.ParserCategory
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.withLetValue : {α : Type} →
  [Inhabited α] →
    {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → [MonadWithReaderOf Lean.SubExpr m] → m α → m α
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.ofBoxProdLeft.eq_def : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [inst : DecidableEq β]
  [inst_1 : DecidableRel G.Adj] {x y : α × β} (x_1 : (G □ H).Walk x y),
  x_1.ofBoxProdLeft =
    match y, x_1 with
    | .(x), SimpleGraph.Walk.nil => SimpleGraph.Walk.nil
    | y, SimpleGraph.Walk.cons h w =>
      Or.by_cases h (fun hG => SimpleGraph.Walk.cons ⋯ w.ofBoxProdLeft) fun hH => ⋯ ▸ w.ofBoxProdLeft
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates
Tactic.ComputeAsymptotics.UnitMonomial.AllZero.not_FirstNonzeroIsPos : ∀ {li : Tactic.ComputeAsymptotics.UnitMonomial}, li.AllZero → ¬li.FirstNonzeroIsPos
-- Mathlib.Algebra.Group.Submonoid.Operations
MulEquiv.coe_submonoidMap_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N) (S : Submonoid M) (g : ↥S),
  ↑((e.submonoidMap S) g) = e ↑g
-- Mathlib.Topology.IsClosedRestrict
Topology.reorderRestrictProd_of_compl : ∀ {ι : Type u_1} {α : ι → Type u_2} {s : Set ((i : ι) → α i)} {S : Set ι}
  (p : ↑(Sᶜ.domRestrict '' s) × ((i : ↑S) → α ↑i)) (j : ↑Sᶜ), Topology.reorderRestrictProd S s p ↑j = ↑p.1 j
-- Batteries.Data.MLList.Basic
/-- Extract an array inside the monad from a `MLList`.  -/
MLList.asArray : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → m (Array α)
-- Lean.DocString.Types
Lean.Doc.Inline.math.inj : ∀ {i : Type u} {mode : Lean.Doc.MathMode} {string : String} {mode_1 : Lean.Doc.MathMode} {string_1 : String},
  Lean.Doc.Inline.math mode string = Lean.Doc.Inline.math mode_1 string_1 → mode = mode_1 ∧ string = string_1
-- Init.Data.Int.Lemmas
Int.instLawfulIdentityHAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.carg : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℂ},
  AEMeasurable f μ → AEMeasurable (fun x => (f x).arg) μ
-- Std.Do.WP.SimpLemmas
Std.Do.WP.getModify_MonadStateOf : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} {Q : Std.Do.PostCond σ ps} [inst : Std.Do.WP m ps]
  [inst_1 : MonadStateOf σ m] (f : σ → σ),
  (Std.Do.wp (getModify f)).apply Q = (Std.Do.wp (MonadStateOf.modifyGet fun s => (s, f s))).apply Q
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
_private.Mathlib.RingTheory.Perfectoid.FontaineTheta.0.term𝕎_ : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instNoMaxOrder : NoMaxOrder Ordinal.{u_1}
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.instInhabitedSplittingFieldAux : (n : ℕ) → {K : Type u} → [inst : Field K] → (f : Polynomial K) → Inhabited (Polynomial.SplittingFieldAux n f)
-- Init.Data.String.Lemmas.Slice
String.Slice.back_eq : ∀ {s : String.Slice}, s.back = s.back?.getD default
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLin'_one : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  Matrix.toLin' 1 = LinearMap.id
-- Mathlib.Order.Fin.Tuple
Fin.pi_lex_lt_cons_cons : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} {x₀ y₀ : α 0} {x y : (i : Fin n) → α i.succ}
  (s : {i : Fin n.succ} → α i → α i → Prop),
  Pi.Lex (fun x1 x2 => x1 < x2) s (Fin.cons x₀ x) (Fin.cons y₀ y) ↔
    s x₀ y₀ ∨ x₀ = y₀ ∧ Pi.Lex (fun x1 x2 => x1 < x2) (fun i => s) x y
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.Context.mk.inj : ∀ {symPrios : Lean.Meta.Grind.SymbolPriorities} {minPrio : ℕ} {symPrios_1 : Lean.Meta.Grind.SymbolPriorities}
  {minPrio_1 : ℕ},
  { symPrios := symPrios, minPrio := minPrio } = { symPrios := symPrios_1, minPrio := minPrio_1 } →
    symPrios = symPrios_1 ∧ minPrio = minPrio_1
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_def : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.OrdConnected ↔ ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → Set.Icc x y ⊆ s
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.var.inj : ∀ {v v_1 : Nat.Internal.Linear.Var}, Nat.Internal.SOM.Expr.var v = Nat.Internal.SOM.Expr.var v_1 → v = v_1
-- Mathlib.Algebra.Ring.Semireal.Defs
IsSemireal.one_add_ne_zero : ∀ {R : Type u_1} {inst : Add R} {inst_1 : Mul R} {inst_2 : One R} {inst_3 : Zero R} [self : IsSemireal R] {s : R},
  IsSumSq s → 1 + s ≠ 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_eq_getD_get? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a fallback : α},
  t.getD a fallback = (t.get? a).getD fallback
-- Batteries.Data.String.Lemmas
Substring.Raw.Valid.any : ∀ (f : Char → Bool) {s : Substring.Raw}, s.Valid → Substring.Raw.Legacy.any s f = s.toString.toList.any f
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_natAddEmb_Ici : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Finset.map (Fin.natAddEmb m) (Finset.Ici i) = Finset.Ici (Fin.natAdd m i)
-- Mathlib.ModelTheory.Order
FirstOrder.Language.order.card_eq_one : FirstOrder.Language.order.card = 1
-- Mathlib.CategoryTheory.Localization.Linear
/-- If `L : C ⥤ D` is a localization functor and `C` is `R`-linear, then `D` is
`R`-linear if we already know that `D` is preadditive and `L` is additive.  -/
CategoryTheory.Localization.linear : (R : Type w) →
  [inst : Ring R] →
    {C : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} C] →
        {D : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_3 : CategoryTheory.Preadditive C] →
              [inst_4 : CategoryTheory.Preadditive D] →
                (L : CategoryTheory.Functor C D) →
                  (W : CategoryTheory.MorphismProperty C) →
                    [L.IsLocalization W] → [L.Additive] → [CategoryTheory.Linear R C] → CategoryTheory.Linear R D
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instMonoidHomClass : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], MonoidHomClass (A →ₜ* B) A B
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.lTensor_tmul : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {Q : Type uQ} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid Q]
  [inst_10 : Module R Q] (f : N →ₗ[R] Q) (m : M) (n : N),
  ((TensorProduct.AlgebraTensorModule.lTensor A M) f) (m ⊗ₜ[R] n) = m ⊗ₜ[R] f n
-- Mathlib.Data.Nat.Cast.Order.Basic
NeZero.nat_of_injective : ∀ {R : Type u_2} {S : Type u_3} {F : Type u_4} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S]
  [inst_2 : FunLike F R S] {n : ℕ} [NeZero ↑n] [RingHomClass F R S] {f : F}, Function.Injective ⇑f → NeZero ↑n