mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.DFinsupp
iSupIndep.linearEquiv_apply : ∀ {ι : Type u_1} {R : Type u_3} {N : Type u_6} [inst : DecidableEq ι] [inst_1 : Ring R] [inst_2 : AddCommGroup N]
  [inst_3 : Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ i, p i = ⊤) (x : Π₀ (i : ι), ↥(p i)),
  (ind.linearEquiv iSup_top) x = (DFinsupp.sumAddHom fun i => (p i).subtype.toAddMonoidHom) x
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_add_measure : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.HasFiniteIntegral f (μ + ν) ↔ MeasureTheory.HasFiniteIntegral f μ ∧ MeasureTheory.HasFiniteIntegral f ν
-- Mathlib.Data.Fin.Embedding
Fin.coe_succAboveEmb : ∀ {n : ℕ} (p : Fin (n + 1)), ⇑p.succAboveEmb = p.succAbove
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
SSet.Truncated.Edge.mk.injEq : ∀ {X : SSet.Truncated 2} {x₀ x₁ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })}
  (edge : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 }))
  (src_eq :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge =
        x₀)
      SSet.Truncated.Edge.src_eq._autoParam)
  (tgt_eq :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge =
        x₁)
      SSet.Truncated.Edge.tgt_eq._autoParam)
  (edge_1 : X.obj (Opposite.op { obj := { len := 1 }, property := SSet.Truncated.Edge._proof_2 }))
  (src_eq_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 1 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge_1 =
        x₀)
      SSet.Truncated.Edge.src_eq._autoParam)
  (tgt_eq_1 :
    autoParam
      ((CategoryTheory.ConcreteCategory.hom
            (X.map (SimplexCategory.Truncated.δ₂ 0 SSet.Truncated.Edge._proof_1 SSet.Truncated.Edge._proof_3).op))
          edge_1 =
        x₁)
      SSet.Truncated.Edge.tgt_eq._autoParam),
  ({ edge := edge, src_eq := src_eq, tgt_eq := tgt_eq } = { edge := edge_1, src_eq := src_eq_1, tgt_eq := tgt_eq_1 }) =
    (edge = edge_1)
-- Mathlib.Probability.Kernel.Category.SFinKer
/-- The category of measurable spaces and s-finite kernels.  -/
SFinKer : Type (u + 1)
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.instBEqCall : BEq Lean.Meta.FunInd.Call
-- Mathlib.Data.Setoid.Basic
/-- The uniqueness part of the universal property for quotients of an arbitrary type.  -/
Setoid.lift_unique : ∀ {α : Type u_1} {β : Type u_2} {r : Setoid α} {f : α → β} (H : r ≤ Setoid.ker f) (g : Quotient r → β),
  f = g ∘ Quotient.mk'' → Quotient.lift f H = g
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The integral `PowerBasis` of `𝓞 K` given by `ζ - 1`, where `K` is a `p ^ k` cyclotomic
extension of `ℚ`.  -/
IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow : {p k : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [hp : Fact (Nat.Prime p)] →
          [inst_1 : CharZero K] →
            [IsCyclotomicExtension {p ^ k} ℚ K] →
              IsPrimitiveRoot ζ (p ^ k) → PowerBasis ℤ (NumberField.RingOfIntegers K)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_insertIfNew : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {k a : α} {v : β} {h₁ : a ∈ m.insertIfNew k v},
  Std.DHashMap.Raw.Const.get (m.insertIfNew k v) a h₁ =
    if h₂ : (k == a) = true ∧ k ∉ m then v else Std.DHashMap.Raw.Const.get m a ⋯
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.equiv_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {ι' : Type u_5} {E' : Type u_6} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E']
  {v : Module.Basis ι 𝕜 E} (hv : Orthonormal 𝕜 ⇑v) {v' : Module.Basis ι' 𝕜 E'} (hv' : Orthonormal 𝕜 ⇑v') (e : ι ≃ ι'),
  (hv.equiv hv' e).symm = hv'.equiv hv e.symm
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.map_germ_eq_Γgerm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U : TopologicalSpace.Opens ↑X} {i : U ⟶ ⊤} (x : ↑X) (hx : x ∈ U),
  CategoryTheory.CategoryStruct.comp (F.map i.op) (F.germ U x hx) = F.Γgerm x
-- Lean.Parser.Term
Lean.Parser.Term.macroLastArg.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.IsAffineOpen.iSup_of_disjoint : ∀ {σ : Type v} {X : AlgebraicGeometry.Scheme} [Finite σ] {U : σ → X.Opens},
  (∀ (i : σ), AlgebraicGeometry.IsAffineOpen (U i)) →
    Pairwise (Function.onFun Disjoint U) → AlgebraicGeometry.IsAffineOpen (iSup U)
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- If a function is `C^2` within a set at a point, and accumulated by points in the interior
of the set, then its second derivative there is symmetric. Over a field
different from `ℝ` or `ℂ`, we should require that the function is analytic.  -/
ContDiffWithinAt.isSymmSndFDerivWithinAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x : E}
  {n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x →
    minSmoothness 𝕜 2 ≤ n → UniqueDiffOn 𝕜 s → x ∈ closure (interior s) → x ∈ s → IsSymmSndFDerivWithinAt 𝕜 f s x
-- Init.Data.List.Sublist
List.instTransSubsetMem : {α : Type u_1} → Trans (fun l₁ l₂ => l₂ ⊆ l₁) Membership.mem Membership.mem
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (c : C) {d d' : D}
  (f : d ⟶ d'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f))
      (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d)
      (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f))
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.nontrivial_iff : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G}, Nontrivial (G ⧸ N) ↔ N ≠ ⊤
-- Mathlib.Topology.Algebra.Monoid
continuousMul_inf : ∀ {M : Type u_3} [inst : Mul M] {t₁ t₂ : TopologicalSpace M}, ContinuousMul M → ContinuousMul M → ContinuousMul M
-- Init.Data.FloatArray.Basic
FloatArray.mk.inj : ∀ {data data_1 : Array Float}, { data := data } = { data := data_1 } → data = data_1
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `Finset.analyticAt_sum`

---

Finite sums of analytic functions are analytic  -/
Finset.analyticAt_fun_sum : ∀ {α : Type u_1} {𝕜 : 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]
  {f : α → E → F} {c : E} (N : Finset α), (∀ n ∈ N, AnalyticAt 𝕜 (f n) c) → AnalyticAt 𝕜 (fun a => ∑ c ∈ N, f c a) c
-- Init.Data.Array.Attach
Array.toList_attachWith : ∀ {α : Type u_1} {xs : Array α} {P : α → Prop} {H : ∀ x ∈ xs, P x},
  (xs.attachWith P H).toList = xs.toList.attachWith P ⋯
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_eq_coe : ∀ {x y : ℝ}, ↑x = ↑y ↔ x = y
-- Mathlib.Algebra.Polynomial.PartialFractions
/-- Let `R` be a commutative ring and `f g : R[X]`. Let `n` be a natural number.
Then `f` can be written in the form `g ^ n * (q + ∑ i : Fin n, r i / g ^ (i + 1))`
in at most one way, where `degree (r i) < degree g` and the denominator cancels formally.
See `eq_quo_mul_pow_add_sum_rem_mul_pow` for the existence of such a representation.  -/
Polynomial.quo_mul_pow_add_sum_rem_mul_pow_unique : ∀ {R : Type u_1} [inst : CommRing R] {g : Polynomial R},
  g.Monic →
    ∀ {n : ℕ} {q₁ q₂ : Polynomial R} {r₁ r₂ : Fin n → Polynomial R},
      (∀ (i : Fin n), (r₁ i).degree < g.degree) →
        (∀ (i : Fin n), (r₂ i).degree < g.degree) →
          q₁ * g ^ n + ∑ i, r₁ i * g ^ ↑i = q₂ * g ^ n + ∑ i, r₂ i * g ^ ↑i → q₁ = q₂ ∧ r₁ = r₂
-- Mathlib.Algebra.Opposites
AddOpposite.unop_bijective : ∀ {α : Type u_1}, Function.Bijective AddOpposite.unop
-- Mathlib.Algebra.Homology.Bifunctor
CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_d : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  {I₁ : Type u_4} {I₂ : Type u_5} {c₁ : ComplexShape I₁} (c₂ : ComplexShape I₂) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (i₁ : I₁) (i₂ i₂' : I₂),
  (((F.mapBifunctorHomologicalComplexObj c₂ K₁).obj K₂).X i₁).d i₂ i₂' = (F.obj (K₁.X i₁)).map (K₂.d i₂ i₂')
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.move.sizeOf_spec : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  sizeOf (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) = 1 + sizeOf k₁ + sizeOf k₂ + sizeOf q
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.exists_measurable_superset_iff_measure_eq_zero : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  (∃ t, s ⊆ t ∧ MeasurableSet t ∧ μ t = 0) ↔ μ s = 0
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.instAddCancelCommMonoid : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddCancelCommMonoid α] → AddCancelCommMonoid (Matrix m n α)
-- Mathlib.Data.Fintype.Defs
Fintype.decidableSubsingleton : {α : Type u_1} → [Fintype α] → [DecidableEq α] → {s : Set α} → [DecidablePred fun x => x ∈ s] → Decidable s.Subsingleton
-- Mathlib.Analysis.Convex.Function
ConcaveOn.comp_strictConcaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {α : Type u_4} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid α] [inst_4 : PartialOrder α] [inst_5 : AddCommMonoid β]
  [inst_6 : PartialOrder β] [inst_7 : SMul 𝕜 E] [inst_8 : SMul 𝕜 α] [inst_9 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {g : β → α}, ConcaveOn 𝕜 (f '' s) g → StrictConcaveOn 𝕜 s f → StrictMonoOn g (f '' s) → StrictConcaveOn 𝕜 s (g ∘ f)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.instCountableSubtypeAddOppositeMemOp : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G) [Countable ↥H], Countable ↥H.op
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.of_degree_le_one_of_invertible : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.degree ≤ 1 → ∀ (h : Invertible f.leadingCoeff), f.Splits
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.add : ∀ {m : Type u_1} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [AddLeftMono R]
  {A B : Matrix m m R}, A.PosDef → B.PosDef → (A + B).PosDef
-- Mathlib.Topology.VectorBundle.Hom
hom_trivializationAt : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂]
  [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] (x₀ : B),
  trivializationAt (F₁ →SL[σ] F₂) (fun x => E₁ x →SL[σ] E₂ x) x₀ =
    Bundle.Trivialization.continuousLinearMap σ (trivializationAt F₁ E₁ x₀) (trivializationAt F₂ E₂ x₀)
-- Mathlib.Algebra.Module.LocalizedModule.Submodule
Submodule.toLocalized'_apply_coe : ∀ {R : Type u_1} (S : Type u_2) {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Algebra R S] [inst_7 : Module S N] [inst_8 : IsScalarTower R S N] (p : Submonoid R)
  [inst_9 : IsLocalization p S] (f : M →ₗ[R] N) [inst_10 : IsLocalizedModule p f] (M' : Submodule R M) (c : ↥M'),
  ↑((Submodule.toLocalized' S p f M') c) = f ↑c
-- Init.Data.Float.Model.Float32
/-- Return a `Float32.Model` with positive sign.
 -/
Float32.Model.abs : Float32.Model → Float32.Model
-- Mathlib.SetTheory.Ordinal.Notation
/-- Notation for ω  -/
ONote.omega : ONote
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_left : ∀ {α : Type u_1} (s t : Set α), s.ite s t = s ∪ t
-- Mathlib.Data.List.Sigma
List.keys_append : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)}, (l₁ ++ l₂).keys = l₁.keys ++ l₂.keys
-- Batteries.Data.ByteSlice
/-- Implementation of `forIn` for a `ByteSlice`.  -/
ByteSlice.forIn : {m : Type u_1 → Type u_2} → {β : Type u_1} → [Monad m] → ByteSlice → β → (UInt8 → β → m (ForInStep β)) → m β
-- Lean.Meta.Tactic.Ext
/-- Declaration name of the extensionality theorem.  -/
Lean.Meta.Ext.ExtTheorem.declName : Lean.Meta.Ext.ExtTheorem → Lean.Name
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumMap_comp_inr : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L₁ : FirstOrder.Language}
  {L₂ : FirstOrder.Language} (ψ : L₁ →ᴸ L₂),
  (ϕ.sumMap ψ).comp FirstOrder.Language.LHom.sumInr = FirstOrder.Language.LHom.sumInr.comp ψ
-- Mathlib.ModelTheory.Substructures
/-- The restriction of a first-order hom to a substructure `s ⊆ M` gives a hom `s → N`.  -/
FirstOrder.Language.Hom.domRestrict : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → L.Hom M N → (p : L.Substructure M) → L.Hom (↥p) N
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.adj_incidenceSet_inter : ∀ {V : Type u} (G : SimpleGraph V) {v : V} {e : Sym2 V},
  e ∈ G.edgeSet → ∀ (h : v ∈ e), G.incidenceSet v ∩ G.incidenceSet (Sym2.Mem.other h) = {e}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.forM.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m : Type w → Type w₂} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Std.TransCmp cmp] (f f_1 : α → β → m PUnit.{w + 1}),
  f = f_1 → ∀ (t t_1 : Std.ExtTreeMap α β cmp), t = t_1 → Std.ExtTreeMap.forM f t = Std.ExtTreeMap.forM f_1 t_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Mathlib.Meta.NormNum.rpow_isRat_eq_inv_rpow : ∀ (a b : ℝ) (n d : ℕ), Mathlib.Meta.NormNum.IsRat b (Int.negOfNat n) d → a ^ b = a⁻¹ ^ (↑n / ↑d)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.closedBall_eq_empty : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, Metric.closedBall x ε = ∅ ↔ ε < 0
-- Mathlib.Analysis.Convex.Between
/-- **Alias** of the reverse direction of `sbtw_neg_iff`. -/
Sbtw.neg : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] {x y z : V}, Sbtw R x y z → Sbtw R (-x) (-y) (-z)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.Location.mk'.inj : ∀ {startPosLine startPosCharacter endPosLine endPosCharacter : ℕ} {parentDecl : String}
  {startPosLine_1 startPosCharacter_1 endPosLine_1 endPosCharacter_1 : ℕ} {parentDecl_1 : String},
  { startPosLine := startPosLine, startPosCharacter := startPosCharacter, endPosLine := endPosLine,
        endPosCharacter := endPosCharacter, parentDecl := parentDecl } =
      { startPosLine := startPosLine_1, startPosCharacter := startPosCharacter_1, endPosLine := endPosLine_1,
        endPosCharacter := endPosCharacter_1, parentDecl := parentDecl_1 } →
    startPosLine = startPosLine_1 ∧
      startPosCharacter = startPosCharacter_1 ∧
        endPosLine = endPosLine_1 ∧ endPosCharacter = endPosCharacter_1 ∧ parentDecl = parentDecl_1
-- Batteries.Data.Vector.Lemmas
Vector.toList_scanrM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {n : ℕ} {init : β} [inst : Monad m] [LawfulMonad m]
  {f : α → β → m β} {as : Vector α n}, Vector.toList <$> Vector.scanrM f init as = List.scanrM f init as.toList
-- Mathlib.Algebra.BigOperators.Fin
/-- A product of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)`
is the product of `f (Fin.last n)` times the remaining product  -/
Fin.prod_univ_castSucc : ∀ {M : Type u_2} [inst : CommMonoid M] {n : ℕ} (f : Fin (n + 1) → M), ∏ i, f i = (∏ i, f i.castSucc) * f (Fin.last n)
-- Init.Data.Vector.MapIdx
Vector.mapIdx_eq_iff : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {f : ℕ → α → β} {ys : Vector β n},
  Vector.mapIdx f xs = ys ↔ ∀ (i : ℕ) (h : i < n), f i xs[i] = ys[i]
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.ofDual_intermediateFieldEquivSubgroup_apply : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [hGKL : IsGaloisGroup G K L] [inst_5 : Finite G]
  {F : IntermediateField K L},
  OrderDual.ofDual ((IsGaloisGroup.intermediateFieldEquivSubgroup G K L) F) = fixingSubgroup G ↑F
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.instCoeFunForallReal : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → [HasContDiffBump E] → {c : E} → CoeFun (ContDiffBump c) fun x => E → ℝ
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_apply_zero : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] (Φ : ZMod N → E),
  ZMod.dft Φ 0 = ∑ j, Φ j
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
HopfAlgCat.Hom.mk : {R : Type u} → [inst : CommRing R] → {V W : HopfAlgCat R} → (V.carrier →ₐc[R] W.carrier) → V.Hom W
-- Std.Tactic.Do.Syntax
/-- Either the contextual keyword ` invariants ` or its tracing form ` invariants? ` which suggests
skeletons for missing invariants as a hint.
 -/
Lean.Parser.Tactic.invariantsKW : Lean.ParserDescr
-- Mathlib.Data.Countable.Defs
Prop.countable : ∀ (p : Prop), Countable p
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
fderivWithin_comp_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_3} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜},
  fderivWithin 𝕜 (fun a => f (-a)) s x = -fderivWithin 𝕜 f (-s) (-x)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.instPreservesFiniteColimitsπ₃ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteColimits C],
  CategoryTheory.Limits.PreservesFiniteColimits CategoryTheory.ShortComplex.π₃
-- Init.Data.Vector.Lemmas
Vector.replicate_eq_mk_replicate : ∀ {α : Type u_1} {a : α} {n : ℕ}, Vector.replicate n a = Vector.mk (Array.replicate n a) ⋯
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierInvₗ_apply : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransformInv E F] [inst_6 : FourierInvAdd E F]
  [inst_7 : FourierInvSMul R E F] (f : E), (FourierTransform.fourierInvₗ R E) f = FourierTransformInv.fourierInv f
-- Mathlib.Topology.Constructible
Topology.IsConstructible.induction_of_isTopologicalBasis : ∀ {X : Type u_2} [inst : TopologicalSpace X] [CompactSpace X] {P : (s : Set X) → Topology.IsConstructible s → Prop}
  [inst_2 : QuasiSeparatedSpace X] {ι : Type u_4} [Nonempty ι] (b : ι → Set X)
  (basis : TopologicalSpace.IsTopologicalBasis (Set.range b)) (isCompact_basis : ∀ (i : ι), IsCompact (b i)),
  (∀ (i : ι) (s : Set ι) (hs : s.Finite), P (b i \ ⋃ j ∈ s, b j) ⋯) →
    (∀ (s : Set X) (hs : Topology.IsConstructible s) (t : Set X) (ht : Topology.IsConstructible t),
        P s hs → P t ht → P (s ∪ t) ⋯) →
      ∀ (s : Set X) (hs : Topology.IsConstructible s), P s hs
-- Lean.Meta.Tactic.Assert
/-- The hypothesis' `LocalDeclKind`  -/
Lean.Meta.Hypothesis.kind : Lean.Meta.Hypothesis → Lean.LocalDeclKind
-- Mathlib.Order.SetNotation
/-- Delaborator for indexed infimum.  -/
iInf_delab : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Topology.Order.NhdsSet
Ioi_mem_nhdsSet_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderClosedTopology α] {a b c : α},
  a < b → Set.Ioi a ∈ nhdsSet (Set.Ico b c)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCallHierarchyOutgoingCallsParams.toJson : Lean.Lsp.CallHierarchyOutgoingCallsParams → Lean.Json
-- Mathlib.Analysis.PSeries
/-- **Divergence of the Harmonic Series**  -/
Real.tendsto_sum_range_one_div_nat_succ_atTop : Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, 1 / (↑i + 1)) Filter.atTop Filter.atTop
-- Mathlib.Algebra.GroupWithZero.Regular
/-- In a non-trivial `MulZeroClass`, the `0` element is not left-regular.  -/
not_isLeftRegular_zero_iff : ∀ {R : Type u_1} [inst : MulZeroClass R], ¬IsLeftRegular 0 ↔ Nontrivial R
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.aeval_root_self : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), (Polynomial.aeval h.root) f = 0
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- The submodule `eigenspace f μ` for a linear map `f` and a scalar `μ` consists of all vectors `x`
such that `f x = μ • x`. (Def 5.52 of [axler2024]).  -/
Module.End.eigenspace : {R : Type v} →
  {M : Type w} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → Module.End R M → R → Submodule R M
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass
_private.Mathlib.Algebra.Homology.DerivedCategory.Ext.ExtClass.0.CategoryTheory.ShortComplex.ShortExact.hasSmallLocalizedShiftedHom_K_S'_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] [CategoryTheory.HasExt C]
  {S : CategoryTheory.ShortComplex C},
  S.ShortExact →
    CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ
      (CochainComplex.mappingCone (S.map (CochainComplex.singleFunctor C 0)).f)
      (S.map (CochainComplex.singleFunctor C 0)).X₁
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.δ_eventually_cofinite : EisensteinSeries.δ✝ =ᶠ[Filter.cofinite] 0
-- Mathlib.Logic.Relation
/-- **Alias** of `IsTrans.map`. -/
Relation.isTrans_map : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} [IsTrans α r] {f : α → β},
  (∀ (x y : α), f x = f y → r x y) → IsTrans β (Relation.Map r f f)