mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Process.Predictable
/-- Given a filtration `𝓕`, the predictable σ-algebra is the σ-algebra on `ι × Ω` generated by
sets of the form `(t, ∞) × A` for `t ∈ ι` and `A ∈ 𝓕 t` and `{⊥} × A` for `A ∈ 𝓕 ⊥`.  -/
MeasureTheory.Filtration.predictable : {Ω : Type u_1} →
  {ι : Type u_2} →
    {m : MeasurableSpace Ω} →
      [inst : Preorder ι] → [OrderBot ι] → MeasureTheory.Filtration ι m → MeasurableSpace (ι × Ω)
-- Std.Http.Data.Headers.Basic
/-- The normalized connection-option tokens.
 -/
Std.Http.Header.Connection.tokens : Std.Http.Header.Connection → Array String
-- Mathlib.Data.TwoPointing
/-- The `False`, `True` two-pointing of `Prop`.  -/
TwoPointing.prop : TwoPointing Prop
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_mul_self : ∀ (a b : ℤ), a.fdiv b * b = a - a.fmod b
-- Mathlib.Computability.EpsilonNFA
εNFA.isPath_append : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ) {s u : σ} {x y : List (Option α)},
  M.IsPath s u (x ++ y) ↔ ∃ t, M.IsPath s t x ∧ M.IsPath t u y
-- Mathlib.Algebra.Order.Group.Unbundled.Abs
LatticeOrderedAddCommGroup.isSolid_solidClosure : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] (s : Set α),
  LatticeOrderedAddCommGroup.IsSolid (LatticeOrderedAddCommGroup.solidClosure s)
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_sum_index : ∀ {α : Type u_1} {β : Type u_7} {M : Type u_8} {N : Type u_10} {P : Type u_11} [inst : Zero M]
  [inst_1 : AddCommMonoid N] [inst_2 : AddCommMonoid P] {f : α →₀ M} {g : α → M → β →₀ N} {h : β → N → P},
  (∀ (a : β), h a 0 = 0) →
    (∀ (a : β) (b₁ b₂ : N), h a (b₁ + b₂) = h a b₁ + h a b₂) → (f.sum g).sum h = f.sum fun a b => (g a b).sum h
-- Mathlib.CategoryTheory.Shift.Induced
/-- The `zero` field of the `ShiftMkCore` structure for the induced shift.  -/
CategoryTheory.HasShift.Induced.zero : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (F : CategoryTheory.Functor C D) →
          {A : Type u_3} →
            [inst_2 : AddMonoid A] →
              [inst_3 : CategoryTheory.HasShift C A] →
                (s : A → CategoryTheory.Functor D D) →
                  ((a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F) →
                    [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full] →
                      [((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] →
                        s 0 ≅ CategoryTheory.Functor.id D
-- Init.Data.UInt.Bitwise
UInt64.xor_comm : ∀ (a b : UInt64), a ^^^ b = b ^^^ a
-- Mathlib.CategoryTheory.Bicategory.Free
/-- Auxiliary definition for `lift`.  -/
CategoryTheory.FreeBicategory.liftHom₂ : {B : Type u₁} →
  [inst : Quiver B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : B ⥤q C) →
          {a b : CategoryTheory.FreeBicategory B} →
            {f g : a ⟶ b} →
              CategoryTheory.FreeBicategory.Hom₂ f g →
                (CategoryTheory.FreeBicategory.liftHom F f ⟶ CategoryTheory.FreeBicategory.liftHom F g)
-- Mathlib.Algebra.Polynomial.Sequence
Polynomial.Sequence.basis.congr_simp : ∀ {R : Type u_1} [inst : Ring R] (S S_1 : Polynomial.Sequence R) (e_S : S = S_1) [inst_1 : IsDomain R]
  (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff), S.basis hCoeff = S_1.basis ⋯
-- Std.Http.Protocol.H1.Reader
/-- Adds body bytes parsed for the current message.
 -/
Std.Http.Protocol.H1.Reader.addBodyBytes : {dir : Std.Http.Protocol.H1.Direction} → ℕ → Std.Http.Protocol.H1.Reader dir → Std.Http.Protocol.H1.Reader dir
-- Mathlib.Algebra.Module.Equiv.Basic
/-- The product over `S ⊕ T` of a family of modules is isomorphic to the product of
(the product over `S`) and (the product over `T`).

This is `Equiv.sumPiEquivProdPi` as a `LinearEquiv`.
 -/
LinearEquiv.sumPiEquivProdPi : (R : Type u_9) →
  [inst : Semiring R] →
    (S : Type u_10) →
      (T : Type u_11) →
        (A : S ⊕ T → Type u_12) →
          [inst_1 : (st : S ⊕ T) → AddCommMonoid (A st)] →
            [inst_2 : (st : S ⊕ T) → Module R (A st)] →
              ((st : S ⊕ T) → A st) ≃ₗ[R] ((s : S) → A (Sum.inl s)) × ((t : T) → A (Sum.inr t))
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.neighborFinset_sdiff : ∀ {V : Type u_1} (v : V) [inst : DecidableEq V] {G₁ G₂ : SimpleGraph V} [inst_1 : Fintype ↑((G₁ \ G₂).neighborSet v)]
  [inst_2 : Fintype ↑(G₁.neighborSet v)] [inst_3 : Fintype ↑(G₂.neighborSet v)],
  (G₁ \ G₂).neighborFinset v = G₁.neighborFinset v \ G₂.neighborFinset v
-- Mathlib.Algebra.Category.MonCat.Basic
CommMonCat.id_apply : ∀ (M : CommMonCat) (x : ↑M), (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id M)) x = x
-- Mathlib.CategoryTheory.Sites.Adjunction
/-- The forgetful functor from `Sheaf J D` to sheaves of types, for a concrete category `D`
whose forgetful functor preserves the correct limits.  -/
CategoryTheory.sheafForget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {FD : D → D → Type u_2} →
            {CD : D → Type u_3} →
              [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] →
                [inst_3 : CategoryTheory.ConcreteCategory D FD] →
                  [J.HasSheafCompose (CategoryTheory.forget D)] →
                    CategoryTheory.Functor (CategoryTheory.Sheaf J D) (CategoryTheory.Sheaf J (Type u_3))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k k' : α}
  {f : β → β}, (t.modify k f).contains k' = t.contains k'
-- Std.Do.Triple.SpecLemmas
modify.eq_1 : ∀ {σ : Type u} {m : Type u → Type v} [inst : MonadState σ m] (f : σ → σ),
  modify f = modifyGet fun s => (PUnit.unit, f s)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_insertIfNew!_le : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {v : β k}, (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).size ≤ t.size + 1
-- Mathlib.Analysis.Matrix.HermitianFunctionalCalculus
Matrix.IsHermitian.cfcAux_apply : ∀ {n : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜}
  (hA : A.IsHermitian) (g : C(↑(spectrum ℝ A), ℝ)),
  hA.cfcAux g =
    ((Unitary.conjStarAlgAut 𝕜 (Matrix n n 𝕜)) hA.eigenvectorUnitary)
      (Matrix.diagonal (RCLike.ofReal ∘ ⇑g ∘ fun i => ⟨hA.eigenvalues i, ⋯⟩))
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.inv_app : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {φ : M ⟶ N} {U : X.Opens} [inst : CategoryTheory.IsIso φ],
  AlgebraicGeometry.Scheme.Modules.Hom.app (CategoryTheory.inv φ) U =
    CategoryTheory.inv (AlgebraicGeometry.Scheme.Modules.Hom.app φ U)
-- Mathlib.CategoryTheory.Limits.Types.Multiequalizer
/-- The data of an element in `I.left i` for each `i : J.L`.  -/
CategoryTheory.Limits.MulticospanIndex.sections.val : {J : CategoryTheory.Limits.MulticospanShape} →
  {I : CategoryTheory.Limits.MulticospanIndex J (Type u)} → I.sections → (i : J.L) → I.left i
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.getSimprocFromDecl : Lean.Name → Lean.ImportM (Lean.Meta.Simp.Simproc ⊕ Lean.Meta.Simp.DSimproc)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyReal_iff_ofRingEquiv : ∀ {F : Type u_1} [inst : Field F] {K : Type u_2} [inst_1 : Field K] (f : F ≃+* K),
  NumberField.IsTotallyReal F ↔ NumberField.IsTotallyReal K
-- Mathlib.RingTheory.IsTensorProduct
IsBaseChange.iff_lift_unique : ∀ {R : Type u_1} {M : Type v₁} {N : Type v₂} {S : Type v₃} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : CommSemiring R] [inst_3 : CommSemiring S] [inst_4 : Algebra R S] [inst_5 : Module R M] [inst_6 : Module R N]
  [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] {f : M →ₗ[R] N},
  IsBaseChange S f ↔
    ∀ (Q : Type (max v₁ v₂ v₃)) [inst_9 : AddCommMonoid Q] [inst_10 : Module R Q] [inst_11 : Module S Q]
      [inst_12 : IsScalarTower R S Q] (g : M →ₗ[R] Q), ∃! g', ↑R g' ∘ₗ f = g
-- Mathlib.GroupTheory.Congruence.Defs
Con.Quotient.inhabited.eq_1 : ∀ {M : Type u_1} [inst : Mul M] [inst_1 : One M] {c : Con M}, Con.Quotient.inhabited = { default := ↑1 }
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- If `χ` factors through `d` and `d ∣ m ∣ n`, then `χ` also factors through `m`.  -/
DirichletCharacter.FactorsThrough.mono : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} (χ : DirichletCharacter R n) {d m : ℕ} [NeZero n],
  χ.FactorsThrough d → d ∣ m → m ∣ n → χ.FactorsThrough m
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.injective_lift_iff : ∀ {G : Type u_1} {M : Type u_4} [inst : AddGroup G] [inst_1 : AddMonoid M] (N : AddSubgroup G) [nN : N.Normal]
  (φ : G →+ M) (HN : N ≤ φ.ker), Function.Injective ⇑(QuotientAddGroup.lift N φ HN) ↔ N = φ.ker
-- Lean.Server.Requests
Lean.Server.RequestM.readDoc : {m : Type → Type u_1} →
  [Monad m] → [MonadReaderOf Lean.Server.RequestContext m] → m Lean.Server.FileWorker.EditableDocument
-- Lean.Data.PersistentArray
Lean.PersistentArray.push : {α : Type u} → Lean.PersistentArray α → α → Lean.PersistentArray α
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
/-- Even Hurwitz zeta kernel (function whose Mellin transform will be the even part of the
completed Hurwitz zeta function). See `evenKernel_def` for the defining formula, and
`hasSum_int_evenKernel` for an expression as a sum over `ℤ`.  -/
HurwitzZeta.evenKernel : UnitAddCircle → ℝ → ℝ
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.pointwise_smul_le_pointwise_smul_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ {S T : Subring R}, a • S ≤ a • T ↔ S ≤ T
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPreregular_functor_obj_obj_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preregular C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.regularTopology C) A) {X_1 Y : Dᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Equivalence.sheafCongrPreregular A e).functor.obj X).obj.map f = X.obj.map (e.inverse.map f.unop).op
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.isLeast_opNNNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F), IsLeast {C | ∀ (x : E), ‖f x‖₊ ≤ C * ‖x‖₊} ‖f‖₊
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Surjective.instFstScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.Surjective g],
  AlgebraicGeometry.Surjective (CategoryTheory.Limits.pullback.fst f g)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.endsWith_eq_endsWith_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.endsWith pat = s.toSlice.endsWith pat
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- `IsGaloisGroup` for rings implies `IsGaloisGroup` for their fraction fields.  -/
IsGaloisGroup.to_isFractionRing : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [inst : Group G] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : MulSemiringAction G B] [inst_4 : Algebra A B] [inst_5 : Field K] [inst_6 : Field L]
  [inst_7 : Algebra K L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : Algebra A L] [IsFractionRing A K]
  [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [inst_15 : MulSemiringAction G L]
  [SMulDistribClass G B L] [Finite G] [hGAB : IsGaloisGroup G A B], IsGaloisGroup G K L
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.comparePkg_eq_extension : ∀ (K : Type u_2) [inst : Field K] (x : LaurentSeries.RatFuncAdicCompl K),
  (LaurentSeries.comparePkg K) x = (LaurentSeries.extensionAsRingHom K ⋯) x.toCompletion
-- Mathlib.Algebra.Ring.Int.Parity
Int.even_sign_iff : ∀ {z : ℤ}, Even z.sign ↔ z = 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
mul_eq_one_iff_of_one_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : PartialOrder α] [MulLeftMono α] [MulRightMono α] {a b : α},
  1 ≤ a → 1 ≤ b → (a * b = 1 ↔ a = 1 ∧ b = 1)
-- Lean.Setup
Lean.ModuleArtifacts.oleanPrivate? : Lean.ModuleArtifacts → Option System.FilePath
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.Monadic.step_eq_step : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] {it : Std.IterM Id α},
  Std.Iterator.step it = pure (Std.Shrink.deflate ⟨Std.Rxc.Iterator.Monadic.step it, ⋯⟩)
-- Mathlib.Algebra.Group.Submonoid.Finsupp
AddSubmonoid.exists_finsupp_of_mem_closure_range : ∀ {M : Type u_1} [inst : AddCommMonoid M] {ι : Type u_2} (f : ι → M),
  ∀ x ∈ AddSubmonoid.closure (Set.range f), ∃ a, x = a.sum fun x1 x2 => x2 • f x1
-- Init.Data.String.Defs
String.Slice.Pos.isAtEnd_iff : ∀ {s : String.Slice} {pos : s.Pos}, pos.IsAtEnd ↔ pos = s.endPos
-- Mathlib.Data.Finset.Prod
Finset.product_singleton : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {b : β}, s ×ˢ {b} = Finset.map { toFun := fun i => (i, b), inj' := ⋯ } s
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_balance : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β} {hlb : l.Balanced}
  {hrb : r.Balanced}
  {hlr :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l.size r.size ∨
      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond r.size l.size},
  (Std.DTreeMap.Internal.Impl.balance k v l r hlb hrb hlr).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotientInfEquivSupQuotient_symm_apply_left : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M)
  (x : ↥(p ⊔ p')) (hx : ↑x ∈ p),
  (LinearMap.quotientInfEquivSupQuotient p p').symm (Submodule.Quotient.mk x) = Submodule.Quotient.mk ⟨↑x, hx⟩
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
hasSum_nat_add_iff : ∀ {G : Type u_2} [inst : AddCommGroup G] {g : G} [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G}
  (k : ℕ), HasSum (fun n => f (n + k)) g ↔ HasSum f (g + ∑ i ∈ Finset.range k, f i)
-- Mathlib.Algebra.Order.Group.Action.End
/-- The tautological action by `r ↪r r` on `α`.  -/
RelEmbedding.applyMulAction : {α : Type u_1} → {r : α → α → Prop} → MulAction (r ↪r r) α
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatWith : Std.Time.DateFormat → (modifier : Std.Time.Modifier) → Std.Time.TypeFormat modifier → String
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mk : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          (toSubalgebra : Subalgebra K L) →
            (∀ x ∈ toSubalgebra.carrier, x⁻¹ ∈ toSubalgebra.carrier) → IntermediateField K L
-- Mathlib.RingTheory.FinitePresentation
/-- If `f : A →ₐ[R] B` is surjective with finitely generated kernel and `A` is finitely presented,
then so is `B`.  -/
Algebra.FinitePresentation.of_surjective : ∀ {R : Type w₁} {A : Type w₂} {B : Type w₃} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] {f : A →ₐ[R] B},
  Function.Surjective ⇑f →
    (RingHom.ker f.toRingHom).FG → ∀ [Algebra.FinitePresentation R A], Algebra.FinitePresentation R B
-- Mathlib.Topology.Semicontinuity.Defs
LowerHemicontinuous.lowerHemicontinuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β},
  LowerHemicontinuous f → ∀ (x : α), LowerHemicontinuousAt f x
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mkIso_hom_hom_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (e : ρ.Equiv σ) (x : X), (Rep.Hom.hom (Rep.mkIso e).hom) x = (↑e).toLinearMap x
-- Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
Matrix.fin_two_smul_prod : ∀ {R : Type u_1} [inst : Semiring R] (g : Matrix (Fin 2) (Fin 2) R) (v : R × R),
  g • v = (g 0 0 * v.1 + g 0 1 * v.2, g 1 0 * v.1 + g 1 1 * v.2)
-- Lean.Elab.Term.TermElabM
/-- Incremental elaboration helper. Avoids leakage of data from outside syntax via the monadic context
when running `act` on `stx` by
* setting `stx` as the `ref` and
* deactivating `suppressElabErrors` if `stx` is `missing`-free, which also helps with not hiding
  useful errors in this part of the input. Note that if `stx` has `missing`, this should always be
  true for the outer syntax as well, so taking the old value of `suppressElabErrors` into account
  should not introduce data leakage.

This combinator should always be used when narrowing reuse to a syntax subtree, usually (in the case
of tactics, to be generalized) via `withNarrowed(Arg)TacticReuse`.
 -/
Lean.Elab.Term.withReuseContext : {m : Type → Type u_1} → {α : Type} → [Monad m] → [MonadWithReaderOf Lean.Core.Context m] → Lean.Syntax → m α → m α
-- Lean.Meta.Check
_private.Lean.Meta.Check.0.Lean.Meta.getFunctionDomain : Lean.Expr → Lean.MetaM (Lean.Expr × Lean.BinderInfo)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_helper : ∀ {G₀ : Type u_3} [inst : CommGroupWithZero G₀] {a : G₀} (b : G₀), a ≠ 0 → 1 / (a * b) * a = 1 / b
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict_inv_ofRestrict : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.isoRestrict f).inv f =
    Y.ofRestrict ⋯
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuous_parametric_intervalIntegral_of_continuous : ∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : TopologicalSpace X]
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {f : X → ℝ → E} {a₀ : ℝ},
  Continuous (Function.uncurry f) → ∀ {s : X → ℝ}, Continuous s → Continuous fun x => ∫ (t : ℝ) in a₀..s x, f x t ∂μ
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.card_Iio : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → AddCommMonoid (α i)] [inst_3 : (i : ι) → PartialOrder (α i)]
  [inst_4 : ∀ (i : ι), IsBotZeroClass (α i)] [inst_5 : (i : ι) → OrderBot (α i)]
  [inst_6 : (i : ι) → LocallyFiniteOrder (α i)] (f : Π₀ (i : ι), α i),
  (Finset.Iio f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card - 1
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).getKey? k' =
    if cmp k k' = Ordering.eq then if (f (t.get? k)).isSome = true then some k else none else t.getKey? k'
-- Mathlib.Order.Heyting.Regular
Heyting.Regular.coe_sdiff : ∀ {α : Type u_1} [inst : HeytingAlgebra α] (a b : Heyting.Regular α), ↑(a \ b) = ↑a ⊓ (↑b)ᶜ
-- Init.Data.List.Nat.Perm
/-- Variant of `List.Perm.drop` specifying that the permutation is constant before `i` elementwise.  -/
List.Perm.drop_of_getElem? : ∀ {α : Type u_1} {l₁ l₂ : List α},
  l₁.Perm l₂ → ∀ {i : ℕ}, (∀ j < i, l₁[j]? = l₂[j]?) → (List.drop i l₁).Perm (List.drop i l₂)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_roo : ∀ {α : Type u} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Roo.Sliceable.mkSlice t lowerBound<...upperBound) =
        List.filter (fun e => decide ((compare e lowerBound).isGT = true ∧ (compare e upperBound).isLT = true)) t.keys
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.roots_C_mul_X_add_C : ∀ {R : Type u} {a : R} [inst : Field R] (b : R),
  a ≠ 0 → (Polynomial.C a * Polynomial.X + Polynomial.C b).roots = {-(a⁻¹ * b)}
-- ProofWidgets.Component.Panel.Basic
ProofWidgets.instRpcEncodablePanelWidgetProps : Lean.Server.RpcEncodable ProofWidgets.PanelWidgetProps
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
CategoryTheory.Enriched.FunctorCategory.functorEnriched_comp_id_assoc : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} C] {J : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} J]
  [inst_4 : CategoryTheory.EnrichedOrdinaryCategory V C] (F₁ F₂ : CategoryTheory.Functor J C)
  [inst_5 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₁ F₂]
  [inst_6 : CategoryTheory.Enriched.FunctorCategory.HasFunctorEnrichedHom V F₂ F₂] {Z : CategoryTheory.Functor J V}
  (h : CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedHom V F₁ F₂)
          (CategoryTheory.Enriched.FunctorCategory.functorEnrichedId V F₂))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Enriched.FunctorCategory.functorEnrichedComp V F₁ F₂ F₂)
          h)) =
    h
-- Mathlib.CategoryTheory.Comma.StructuredArrow.CommaMap
CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso_hom_app_right_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor C T}
  {R : CategoryTheory.Functor D T} {C' : Type u₄} [inst_3 : CategoryTheory.Category.{v₄, u₄} C'] {D' : Type u₅}
  [inst_4 : CategoryTheory.Category.{v₅, u₅} D'] {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T']
  {L' : CategoryTheory.Functor C' T'} {R' : CategoryTheory.Functor D' T'} {F₁ : CategoryTheory.Functor C C'}
  {F₂ : CategoryTheory.Functor D D'} {F : CategoryTheory.Functor T T'} (α : F₁.comp L' ⟶ L.comp F)
  (β : R.comp F ⟶ F₂.comp R') [inst_6 : CategoryTheory.IsIso β] (X : CategoryTheory.Comma L' R')
  (X_1 : CategoryTheory.StructuredArrow X (CategoryTheory.Comma.map α β)),
  ((CategoryTheory.StructuredArrow.commaMapEquivalenceUnitIso α β X).hom.app X_1).right.left =
    CategoryTheory.CategoryStruct.id X_1.right.left
-- Mathlib.CategoryTheory.LiftingProperties.Adjunction
CategoryTheory.CommSq.instHasLiftLeftAdjoin : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {G : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C}
  {A B : C} {X Y : D} {i : B ⟶ A} {p : Y ⟶ X} {u : X ⟶ G.obj A} {v : Y ⟶ G.obj B}
  (sq : CategoryTheory.CommSq v p (G.map i) u) (adj : F ⊣ G) [sq.HasLift], ⋯.HasLift
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.intMinSealed_def : ∀ {n : ℕ}, BitVec.Signed.intMinSealed✝ n = ↑(2 ^ (n - 1))
-- Mathlib.Data.Num.Bitwise
/-- Bitwise `not` for `NzsNum`.  -/
NzsNum.not : NzsNum → NzsNum
-- Mathlib.Control.Traversable.Instances
List.traverse_nil : ∀ {F : Type u → Type u} [inst : Applicative F] {α' β' : Type u} (f : α' → F β'), traverse f [] = pure []