mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.Fintype
Multiset.cast_symm_apply_fst : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α} (h : s = t) (x : t.ToType),
  ((Multiset.cast h).symm x).fst = x.fst
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Option (γ a)} {k : α} {h' : k ∈ Std.DHashMap.Raw.filterMap f m}
  (h : m.WF), (Std.DHashMap.Raw.filterMap f m).get k h' = (f k (m.get k ⋯)).get ⋯
-- Aesop.Tracing
Aesop.withAesopTraceNodeBefore : {m : Type → Type} →
  {ε : Type} →
    [Monad m] →
      [Lean.MonadTrace m] →
        [MonadLiftT BaseIO m] →
          [Lean.MonadRef m] →
            [Lean.AddMessageContext m] →
              [Lean.MonadOptions m] →
                [Lean.MonadAlwaysExcept ε m] →
                  {α : Type} →
                    [Lean.ExceptToTraceResult ε α] →
                      Aesop.TraceOption → m Lean.MessageData → m α → optParam Bool true → m α
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.apply_smulCommClass' : ∀ {R : Type uR} {A₁ : Type uA₁} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Algebra R A₁] {S : Type u_1}
  [inst_3 : SMul S R] [inst_4 : SMul S A₁] [IsScalarTower S R A₁], SMulCommClass (A₁ ≃ₐ[R] A₁) S A₁
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.limsup_add_of_left_tendsto_zero : ∀ {ι : Type u_4} {u : Filter ι} {f : ι → ENNReal},
  Filter.Tendsto f u (nhds 0) → ∀ (g : ι → ENNReal), Filter.limsup (f + g) u = Filter.limsup g u
-- Mathlib.Algebra.Order.Monoid.ToMulBot
WithZero.toMulBot_strictMono : ∀ {α : Type u} [inst : Add α] [inst_1 : Preorder α], StrictMono ⇑WithZero.toMulBot
-- Mathlib.Topology.Algebra.PontryaginDual
/-- A compact monoid has discrete Pontryagin dual.  -/
PontryaginDual.instDiscreteTopologyOfCompactSpace : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A] [CompactSpace A], DiscreteTopology (PontryaginDual A)
-- Mathlib.InformationTheory.KullbackLeibler.KLFun
/-- For two finite measures `μ ≪ ν`, the function `x ↦ klFun (μ.rnDeriv ν x).toReal` is integrable
with respect to `ν` iff `llr μ ν` is integrable with respect to `μ`.  -/
InformationTheory.integrable_klFun_rnDeriv_iff : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    (MeasureTheory.Integrable (fun x => InformationTheory.klFun (μ.rnDeriv ν x).toReal) ν ↔
      MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.ext : ∀ {X Y : Bipointed} {x y : X.Hom Y}, x.toFun = y.toFun → x = y
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {f : β → α} {b : β},
  {b}.lcm f = normalize (f b)
-- Mathlib.Analysis.SpecialFunctions.RegularizedHypergeometric
Complex.regularizedHGFunSeries_eq_zero : ∀ {a b : Multiset ℂ} {n : ℕ}, Complex.regularizedHGFunSeries a b n = 0 ↔ Complex.regularizedHGFunCoeff a b n = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.ExtractAndExtendBitTarget.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α] (start : ℕ)
  (x : aig.RefVec w), sizeOf { start := start, x := x } = 1 + sizeOf start + sizeOf x
-- Mathlib.NumberTheory.SmoothNumbers
Nat.equivProdNatSmoothNumbers_apply : ∀ {p e m : ℕ} (hp : Nat.Prime p) (hm : m ∈ p.smoothNumbers),
  ↑((Nat.equivProdNatSmoothNumbers hp) (e, ⟨m, hm⟩)) = p ^ e * m
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map_isIso : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b ⟶ g b)
  [∀ (b : β), CategoryTheory.IsIso (p b)], CategoryTheory.IsIso (CategoryTheory.Limits.Pi.map p)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.restrictFreeVar.eq_4 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (x : ℕ) (φ₁ φ₂ : L.BoundedFormula α x)
  (f : ↥(φ₁.imp φ₂).freeVarFinset → β),
  (φ₁.imp φ₂).restrictFreeVar f =
    (φ₁.restrictFreeVar (f ∘ Set.inclusion ⋯)).imp (φ₂.restrictFreeVar (f ∘ Set.inclusion ⋯))
-- Mathlib.Control.LawfulFix
Part.Fix.approx_mem_approxChain : ∀ {α : Type u_1} {β : α → Type u_2} (f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)) {i : ℕ},
  Part.Fix.approx (⇑f) i ∈ Part.Fix.approxChain f
-- Mathlib.LinearAlgebra.Complex.Module
Complex.imLm_coe : ⇑Complex.imLm = Complex.im
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.toAdd_unzero_eq_log : ∀ {M : Type u_4} [inst : AddMonoid M] {x : WithZero (Multiplicative M)} (hx : x ≠ 0),
  Multiplicative.toAdd (WithZero.unzero hx) = x.log
-- Mathlib.Computability.Partrec
Nat.Partrec.prec : ∀ {f g : ℕ →. ℕ},
  Nat.Partrec f →
    Nat.Partrec g →
      Nat.Partrec
        (Nat.unpaired fun a n =>
          Nat.rec (f a)
            (fun y IH => do
              let i ← IH
              g (Nat.pair a (Nat.pair y i)))
            n)
-- Init.Data.Option.Lemmas
Option.pure_apply : ∀ {α : Type u_1} {x : α}, pure x = some x
-- Mathlib.Algebra.Module.Hom
AddMonoid.End.instModule : {R : Type u_1} →
  {A : Type u_4} → [inst : Semiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Module R (AddMonoid.End A)
-- Mathlib.Algebra.Group.Defs
/-- Scalar multiplication by repeated self-addition,
the additive version of exponentiation by repeated squaring.  -/
nsmulBinRec : {M : Type u_2} → [Zero M] → [Add M] → ℕ → M → M
-- Mathlib.Algebra.Vertex.HVertexOperator
/-- The coefficients of a heterogeneous vertex operator, viewed as a linear map to formal power
series with coefficients in linear maps.  -/
HVertexOperator.coeff : {Γ : Type u_1} →
  [inst : PartialOrder Γ] →
    {R : Type u_2} →
      {V : Type u_3} →
        {W : Type u_4} →
          [inst_1 : CommRing R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : Module R V] →
                [inst_4 : AddCommGroup W] → [inst_5 : Module R W] → HVertexOperator Γ R V W →ₗ[R] Γ → V →ₗ[R] W
-- Mathlib.Data.Part
Part.eq_get_iff_mem : ∀ {α : Type u_1} {o : Part α} {a : α} (h : o.Dom), a = o.get h ↔ a ∈ o
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.measure_fundamentalInterior : ∀ {G : Type u_1} {α : Type u_3} [Countable G] [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.IsFundamentalDomain G s μ → μ (MeasureTheory.fundamentalInterior G s) = μ s
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_le_iff_le_add' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a + -b ≤ c ↔ a ≤ b + c
-- Mathlib.Geometry.Manifold.Diffeomorph
ContinuousLinearEquiv.coe_toDiffeomorph : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  (e : E ≃L[𝕜] E'), ⇑e.toDiffeomorph = ⇑e
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabLink.mk.sizeOf_spec : ∀ (name : Lean.StrLit), sizeOf { name := name } = 1 + sizeOf name
-- Init.Data.SInt.Lemmas
Int16.ofIntLE_bitVecToInt : ∀ (n : BitVec 16), Int16.ofIntLE n.toInt ⋯ ⋯ = Int16.ofBitVec n
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.homothety_apply_same : ∀ {k : Type u_2} {V1 : Type u_3} {P1 : Type u_4} [inst : CommRing k] [inst_1 : AddCommGroup V1]
  [inst_2 : AddTorsor V1 P1] [inst_3 : Module k V1] (c : P1) (r : k), (AffineMap.homothety c r) c = c
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.IntegrableOn.mul_continuousOn_of_subset : ∀ {X : Type u_1} {R : Type u_8} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] {μ : MeasureTheory.Measure X}
  [OpensMeasurableSpace X] {A K : Set X} [inst_3 : NormedRing R] [SecondCountableTopologyEither X R] {g g' : X → R},
  MeasureTheory.IntegrableOn g A μ →
    ContinuousOn g' K → MeasurableSet A → IsCompact K → A ⊆ K → MeasureTheory.IntegrableOn (fun x => g x * g' x) A μ
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `F` is a field of exponential characteristic `q`, `F(S) / F` is separable, then
`F(S) = F(S ^ (q ^ n))` for any natural number `n`.  -/
IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (S : Set E)
  [Algebra.IsSeparable F ↥(IntermediateField.adjoin F S)] (q : ℕ) [ExpChar F q] (n : ℕ),
  IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun x => x ^ q ^ n) '' S)
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.nnnorm_eq_of_mul_nnnorm_lt_max : ∀ {S : Type u_1} [inst : SeminormedGroup S] [IsUltrametricDist S] {x y : S}, ‖x * y‖₊ < max ‖x‖₊ ‖y‖₊ → ‖x‖₊ = ‖y‖₊
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β k}, (t.insertIfNew k v).size = if k ∈ t then t.size else t.size + 1
-- Init.Prelude
/-- The equality relation. It has one introduction rule, `Eq.refl`.
We use `a = b` as notation for `Eq a b`.
A fundamental property of equality is that it is an equivalence relation.
```
variable (α : Type) (a b c d : α)
variable (hab : a = b) (hcb : c = b) (hcd : c = d)

example : a = d :=
  Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd
```
Equality is much more than an equivalence relation, however. It has the important property that every assertion
respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value.
That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`.
Example:
```
example (α : Type) (a b : α) (p : α → Prop)
        (h1 : a = b) (h2 : p a) : p b :=
  Eq.subst h1 h2

example (α : Type) (a b : α) (p : α → Prop)
    (h1 : a = b) (h2 : p a) : p b :=
  h1 ▸ h2
```
The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`.
For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)


Conventions for notations in identifiers:

 * The recommended spelling of `=` in identifiers is `eq`. -/
Eq : {α : Sort u_1} → α → α → Prop
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.mono_pre_nat : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal),
  Monotone fun k => MeasureTheory.OuterMeasure.mkMetric'.pre m (↑k)⁻¹
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_erase_eq_of_not_compare_min!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t.erase k).isEmpty = false → ¬cmp k t.min! = Ordering.eq → (t.erase k).min! = t.min!
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.Hom.mk.inj : ∀ {X Y : Pointed} {toFun : X.X → Y.X} {map_point : toFun X.point = Y.point} {toFun_1 : X.X → Y.X}
  {map_point_1 : toFun_1 X.point = Y.point},
  { toFun := toFun, map_point := map_point } = { toFun := toFun_1, map_point := map_point_1 } → toFun = toFun_1
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.map'_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β) (x : α),
  (WithZero.map' f) ↑x = ↑(f x)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanCompIso_hom_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.spanCompIso F f g).hom.app CategoryTheory.Limits.WalkingSpan.left =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Limits.span f g).comp F).obj CategoryTheory.Limits.WalkingSpan.left)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.UnitLike.State.mk.injEq : ∀ (map map_1 : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr)),
  ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.coherentExtensiveEquivalence_unitIso_inv_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] [inst_2 : CategoryTheory.Preregular C]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : ∀ (X : C), CategoryTheory.Projective X]
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X_1 : Cᵒᵖ),
  (CategoryTheory.Presheaf.coherentExtensiveEquivalence.unitIso.inv.app X).hom.app X_1 =
    CategoryTheory.CategoryStruct.id (X.obj.obj X_1)
-- Std.Data.HashMap.RawLemmas
/-- Variant of `getElem?_map` that holds with `EquivBEq` (i.e. without `LawfulBEq`).  -/
Std.HashMap.Raw.getElem?_map' : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {f : α → β → γ} {k : α} (h : m.WF),
  (Std.HashMap.Raw.map f m)[k]? = Option.pmap (fun v h' => f (m.getKey k h') v) m[k]? ⋯
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.commute_X_pow : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ : MvPowerSeries σ R) (s : σ) (n : ℕ),
  Commute φ (MvPowerSeries.X s ^ n)
-- ProofWidgets.Cancellable
/-- Check whether a request has finished computing,
and return the response if so.
The request is removed from `runningRequests` the first time it is checked
and found to have finished.
Throws an error if the `rid` is invalid,
or if the request itself threw an error.  -/
ProofWidgets.checkRequest : ProofWidgets.RequestId → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.CheckRequestResponse)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.ofSubsingleton.congr_simp : ∀ {R : Type u_1} (M : Type u_5) (M₂ : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] [inst_5 : Subsingleton M]
  [inst_6 : Subsingleton M₂], LinearEquiv.ofSubsingleton M M₂ = LinearEquiv.ofSubsingleton M M₂
-- Init.Grind.AC
Lean.Grind.AC.superpose_ac_idempotent : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  {inst₃ : Std.IdempotentOp ctx.op} (x : Lean.Grind.AC.Var) (lhs₁ rhs₁ rhs : Lean.Grind.AC.Seq),
  Lean.Grind.AC.superpose_ac_idempotent_cert x lhs₁ rhs₁ rhs = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- `liftOfRightInverse f f_inv hf g hg` is the unique additive group homomorphism `φ`
* such that `φ.comp f = g` (`AddMonoidHom.liftOfRightInverse_comp`),
* where `f : G₁ →+ G₂` has a RightInverse `f_inv` (`hf`),
* and `g : G₂ →+ G₃` satisfies `hg : f.ker ≤ g.ker`.
See `AddMonoidHom.eq_liftOfRightInverse` for the uniqueness lemma.
```
   G₁.
   |  \
 f |   \ g
   |    \
   v     \⌟
   G₂----> G₃
      ∃!φ
```  -/
AddMonoidHom.liftOfRightInverse : {G₁ : Type u_5} →
  {G₂ : Type u_6} →
    {G₃ : Type u_7} →
      [inst : AddGroup G₁] →
        [inst_1 : AddGroup G₂] →
          [inst_2 : AddGroup G₃] →
            (f : G₁ →+ G₂) → (f_neg : G₂ → G₁) → Function.RightInverse f_neg ⇑f → { g // f.ker ≤ g.ker } ≃ (G₂ →+ G₃)
-- Mathlib.RingTheory.Coalgebra.Basic
Prod.comul_comp_fst : ∀ (R : Type u) (A : Type v) (B : Type w) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : AddCommMonoid B]
  [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : Coalgebra R A] [inst_6 : Coalgebra R B],
  CoalgebraStruct.comul ∘ₗ LinearMap.fst R A B =
    TensorProduct.map (LinearMap.fst R A B) (LinearMap.fst R A B) ∘ₗ CoalgebraStruct.comul
-- Init.Data.String.TakeDrop
String.stripSuffix : String → String → String
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc'_C_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ) (a : R)
  (p : MvPowerSeries σ R),
  (MvPowerSeries.trunc' R n) (MvPowerSeries.C a * p) = MvPolynomial.C a * (MvPowerSeries.trunc' R n) p
-- Mathlib.SetTheory.Ordinal.FixedPoint
/-- The next common fixed point, at least `a`, for a family of normal functions.

This is defined for any family of functions, as the supremum of all values reachable by applying
finitely many functions in the family to `a`.

`Ordinal.nfpFamily_fp` shows this is a fixed point, `Ordinal.le_nfpFamily` shows it's at
least `a`, and `Ordinal.nfpFamily_le_fp` shows this is the least ordinal with these properties.  -/
Ordinal.nfpFamily : {ι : Type u_1} → (ι → Ordinal.{u} → Ordinal.{u}) → Ordinal.{u} → Ordinal.{u}
-- Lean.Expr
Lean.mkApp9 : Lean.Expr →
  Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.add_equiv_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {f1 f2 g1 g2 : CauSeq β abv},
  f1 ≈ f2 → g1 ≈ g2 → f1 + g1 ≈ f2 + g2
-- Mathlib.MeasureTheory.Integral.Bochner.Set
MeasureTheory.setIntegral_neg_eq_setIntegral_nonpos : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {μ : MeasureTheory.Measure X} [inst_2 : PartialOrder E] {f : X → E},
  MeasureTheory.AEStronglyMeasurable f μ → ∫ (x : X) in {x | f x < 0}, f x ∂μ = ∫ (x : X) in {x | f x ≤ 0}, f x ∂μ
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.unitsEquivPos_apply_coe : ∀ (R : Type u_2) [inst : DivisionSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : PosMulReflectLT R] (r : { r // 0 ≤ r }ˣ), ↑((Nonneg.unitsEquivPos R) r) = ↑↑r
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
BoundedContinuousFunction.probCharDual_apply : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (L : StrongDual ℝ F) (x : F),
  (BoundedContinuousFunction.probCharDual L) x = Complex.exp (↑(L x) * Complex.I)
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_subset_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {t : Set β} {a : α} {s : Set α}, a ∈ s → a +ᵥ t ⊆ s +ᵥ t
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int32.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable Int32
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_nonneg : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : Nontrivial R]
  [inst_3 : StarRing R] [inst_4 : MetricSpace R] [inst_5 : IsTopologicalSemiring R] [inst_6 : ContinuousStar R]
  [ContinuousSqrt R] [StarOrderedRing R] [NoZeroDivisors R] [inst_10 : TopologicalSpace A] [inst_11 : NonUnitalRing A]
  [inst_12 : StarRing A] [inst_13 : PartialOrder A] [StarOrderedRing A] [inst_15 : Module R A]
  [inst_16 : IsScalarTower R A A] [inst_17 : SMulCommClass R A A]
  [inst_18 : NonUnitalContinuousFunctionalCalculus R A p] {f : R → R} {a : A},
  (∀ x ∈ quasispectrum R a, 0 ≤ f x) → 0 ≤ cfcₙ f a
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.IsWide.id_mem : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {S : CategoryTheory.Subgroupoid C},
  S.IsWide → ∀ (c : C), CategoryTheory.CategoryStruct.id c ∈ S.arrows c c
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.mk.injEq : ∀ (argPos targetPos : ℕ) (motive : Option Lean.MVarId) (f fType : Lean.Expr) (alts : Array Lean.Elab.Tactic.ElimApp.Alt)
  (insts : Array Lean.MVarId) (argPos_1 targetPos_1 : ℕ) (motive_1 : Option Lean.MVarId) (f_1 fType_1 : Lean.Expr)
  (alts_1 : Array Lean.Elab.Tactic.ElimApp.Alt) (insts_1 : Array Lean.MVarId),
  ({ argPos := argPos, targetPos := targetPos, motive := motive, f := f, fType := fType, alts := alts,
        insts := insts } =
      { argPos := argPos_1, targetPos := targetPos_1, motive := motive_1, f := f_1, fType := fType_1, alts := alts_1,
        insts := insts_1 }) =
    (argPos = argPos_1 ∧
      targetPos = targetPos_1 ∧ motive = motive_1 ∧ f = f_1 ∧ fType = fType_1 ∧ alts = alts_1 ∧ insts = insts_1)
-- Batteries.Tactic.Lint.Basic
/-- `@[nolint linterName]` omits the tagged declaration from being checked by
the linter with name `linterName`.  -/
Batteries.Tactic.Lint.nolint : Lean.ParserDescr
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.instInhabitedInlayHintState.default : Lean.Server.FileWorker.InlayHintState
-- Lean.Meta.PPGoal
_private.Lean.Meta.PPGoal.0.Lean.Meta.addLine : Std.Format → Std.Format
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_smul : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (f : X → E) (μ : MeasureTheory.VectorMeasure X F) (B : E →L[ℝ] F →L[ℝ] G) (c : ℝ),
  ∫ᵛ (x : X), (c • f) x ∂[B; μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.Order.Booleanisation
Booleanisation.comp_lt_comp : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {a b : α}, Booleanisation.comp a < Booleanisation.comp b ↔ b < a
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp : {R : Type u_1} → [inst : Semiring R] → AddMonoidAlgebra R ℕ → Polynomial R
-- Mathlib.Combinatorics.Additive.CauchyDavenport
/-- The relation we induct along in the proof by DeVos of the Cauchy-Davenport theorem.
`(s₁, t₁) < (s₂, t₂)` iff
* `|s₁ + t₁| < |s₂ + t₂|`
* or `|s₁ + t₁| = |s₂ + t₂|` and `|s₂| + |t₂| < |s₁| + |t₁|`
* or `|s₁ + t₁| = |s₂ + t₂|` and `|s₁| + |t₁| = |s₂| + |t₂|` and `|s₁| < |s₂|`.  -/
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.DevosAddRel : {α : Type u_2} → [AddGroup α] → [DecidableEq α] → Finset α × Finset α → Finset α × Finset α → Prop
-- Mathlib.Order.Std
PartialOrder.OfStdArgs.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : SizeOf α] (toPreorderArgs : Preorder.OfStdArgs α)
  (isPartialOrder :
    autoParam
      (let this := toPreorderArgs.le;
      Std.IsPartialOrder α)
      PartialOrder.OfStdArgs.isPartialOrder._autoParam),
  sizeOf { toPreorderArgs := toPreorderArgs, isPartialOrder := isPartialOrder } =
    1 + sizeOf toPreorderArgs + sizeOf isPartialOrder
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.descResidueField_fromSpecResidueField : ∀ {K : Type u_1} [inst : Field K] (X : AlgebraicGeometry.Scheme) {x : ↥X} (f : X.presheaf.stalk x ⟶ CommRingCat.of K)
  [inst_1 : IsLocalHom (CommRingCat.Hom.hom f)],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.descResidueField f))
      (X.fromSpecResidueField x) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map f) (X.fromSpecStalk x)
-- Mathlib.Analysis.Meromorphic.Divisor
/-- Divisors are invariant under translation, special case where the set is a ball..  -/
MeromorphicOn.divisor_ball_comp_sub_const_eq_divisor_ball : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {z : 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {c : 𝕜} {R : ℝ} {f : 𝕜 → E},
  (MeromorphicOn.divisor (f ∘ fun x => x - c) (Metric.ball c R)) (z + c) = (MeromorphicOn.divisor f (Metric.ball 0 R)) z