mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.getKey!_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, m₁.Equiv m₂ → m₁.getKey! k = m₂.getKey! k
-- Lean.Parser.Types
Lean.Parser.ParserCacheKey.mk.sizeOf_spec : ∀ (toCacheableParserContext : Lean.Parser.CacheableParserContext) (parserName : Lean.Name) (pos : String.Pos.Raw),
  sizeOf { toCacheableParserContext := toCacheableParserContext, parserName := parserName, pos := pos } =
    1 + sizeOf toCacheableParserContext + sizeOf parserName + sizeOf pos
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get!_union_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst : Inhabited β], k ∉ t₁ → (t₁ ∪ t₂).get! k = t₂.get! k
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.subset_zeroLocus_iff_subset_vanishingIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (t : Set (ProjectiveSpectrum 𝒜)) (s : Set A),
  t ⊆ ProjectiveSpectrum.zeroLocus 𝒜 s ↔ s ⊆ ↑(ProjectiveSpectrum.vanishingIdeal t)
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.sub_int_mul_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c x : α} [inst : NonAssocRing α] [inst_1 : NonAssocRing β],
  Function.Antiperiodic f c → ∀ (n : ℤ), f (x - ↑n * c) = ↑↑n.negOnePow * f x
-- Std.Async.Signal
_private.Std.Async.Signal.0.Std.Async.Signal.Waiter.ofNative.inj : ∀ {native native_1 : Std.Internal.UV.Signal}, { native := native } = { native := native_1 } → native = native_1
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
_private.Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing.0.AlgebraicGeometry.LocallyRingedSpace.GlueData.«term𝖣» : Lean.ParserDescr
-- Init.Data.Rat.Lemmas
Rat.le_antisymm : ∀ {a b : ℚ}, a ≤ b → b ≤ a → a = b
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.killCompl_C : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ} (r : R),
  (MvPowerSeries.killCompl e) (MvPowerSeries.C r) = MvPowerSeries.C r
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_pempty : Cardinal.mk PEmpty.{u_1 + 1} = 0
-- Mathlib.ModelTheory.Bundled
CategoryTheory.Bundled.structure : {L : FirstOrder.Language} → (M : CategoryTheory.Bundled L.Structure) → L.Structure ↑M
-- Mathlib.Tactic.Algebra.Basic
/-- Infer from the expression what base ring the normalization should use.
Finds all scalar rings in the expression and picks the 'larger' one in the sense that
it is an algebra over the smaller rings.  -/
Mathlib.Tactic.Algebra.inferBase : {v : Lean.Level} →
  {A : Q(Type v)} →
    {sA : Q(CommSemiring «$A»)} →
      Mathlib.Tactic.Algebra.Cache q(«$sA») → Lean.Expr → Lean.MetaM ((u : Lean.Level) × Q(Type u))
-- Mathlib.Analysis.Normed.Unbundled.InvariantExtension
/-- The algebra norm `invariantExtension` is power-multiplicative.  -/
IsUltrametricDist.isPowMul_invariantExtension : ∀ (K : Type u_1) [inst : NormedField K] (L : Type u_2) [inst_1 : Field L] [inst_2 : Algebra K L]
  [h_fin : FiniteDimensional K L] [hu : IsUltrametricDist K], IsPowMul ⇑(IsUltrametricDist.invariantExtension K L)
-- Mathlib.Order.SymmDiff
symmDiff_eq_top : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), symmDiff a b = ⊤ ↔ IsCompl a b
-- Mathlib.GroupTheory.PresentedGroup
PresentedGroup.mk_eq_mk_of_mul_inv_mem : ∀ {α : Type u_1} {rels : Set (FreeGroup α)} {x y : FreeGroup α},
  x * y⁻¹ ∈ rels → (PresentedGroup.mk rels) x = (PresentedGroup.mk rels) y
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.instInhabitedDecl : {a : Lean.Compiler.LCNF.Purity} → Inhabited (Lean.Compiler.LCNF.Decl a)
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.involutiveNeg.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_3} [inst : Neg M₂] [inst_1 : InvolutiveNeg M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (inv : ∀ (x : M₁), f (-x) = -f x), Function.Surjective.involutiveNeg f hf inv = { toNeg := inst, neg_neg := ⋯ }
-- Init.Data.Nat.Lemmas
Nat.mul_lt_mul_of_le_of_lt' : ∀ {a c b d : ℕ}, a ≤ c → b < d → 0 < a → a * b < c * d
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_neg_left : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {x y : E}, inner A (-x) y = -inner A x y
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- The adjoint is involutive.  -/
ContinuousLinearMap.adjoint_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] (A : E →L[𝕜] F),
  ContinuousLinearMap.adjoint (ContinuousLinearMap.adjoint A) = A
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_preimage_of_isLinearSet : ∀ {M : Type u_1} {ι : Type u_3} [inst : AddCommMonoid M] [Finite ι] {F : Type u_5} [inst_2 : FunLike F (ι → ℕ) M]
  [AddMonoidHomClass F (ι → ℕ) M] {s : Set M}, IsLinearSet s → ∀ (f : F), IsSemilinearSet (⇑f ⁻¹' s)
-- Mathlib.Geometry.Manifold.MFDeriv.UniqueDifferential
/-- If `s` has the unique differential property at `x`, `f` is differentiable within `s` at `x` and
its derivative has dense range, then `f '' s` has the unique differential property at `f x`.  -/
UniqueMDiffWithinAt.image_denseRange : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {s : Set M} {x : M},
  UniqueMDiffAt[s] x →
    ∀ {f : M → M'} {f' : E →L[𝕜] E'}, HasMFDerivAt[s] f x f' → DenseRange ⇑f' → UniqueMDiffAt[f '' s] (f x)
-- Mathlib.Topology.Semicontinuity.Defs
upperHemicontinuousWithinAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → Set β} {s : Set α}
  {x : α}, UpperHemicontinuousWithinAt f s x ↔ ∀ t ∈ nhdsSet (f x), ∀ᶠ (x' : α) in nhdsWithin x s, t ∈ nhdsSet (f x')
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.ConnectionState.mk.inj : ∀ {β : Type} {machine : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving}
  {requestStream : Std.Http.Body.Stream} {keepAliveTimeout : Option Std.Time.Millisecond.Offset}
  {currentTimeout : Std.Time.Millisecond.Offset} {headerTimeout : Option Std.Time.Timestamp}
  {response : Std.Channel (Except IO.Error (Std.Http.Response β))} {respStream : Option β} {requiresData : Bool}
  {expectData : Option ℕ} {handlerDispatched : Bool} {pendingHead : Option Std.Http.Request.Head}
  {machine_1 : Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving}
  {requestStream_1 : Std.Http.Body.Stream} {keepAliveTimeout_1 : Option Std.Time.Millisecond.Offset}
  {currentTimeout_1 : Std.Time.Millisecond.Offset} {headerTimeout_1 : Option Std.Time.Timestamp}
  {response_1 : Std.Channel (Except IO.Error (Std.Http.Response β))} {respStream_1 : Option β} {requiresData_1 : Bool}
  {expectData_1 : Option ℕ} {handlerDispatched_1 : Bool} {pendingHead_1 : Option Std.Http.Request.Head},
  { machine := machine, requestStream := requestStream, keepAliveTimeout := keepAliveTimeout,
        currentTimeout := currentTimeout, headerTimeout := headerTimeout, response := response,
        respStream := respStream, requiresData := requiresData, expectData := expectData,
        handlerDispatched := handlerDispatched, pendingHead := pendingHead } =
      { machine := machine_1, requestStream := requestStream_1, keepAliveTimeout := keepAliveTimeout_1,
        currentTimeout := currentTimeout_1, headerTimeout := headerTimeout_1, response := response_1,
        respStream := respStream_1, requiresData := requiresData_1, expectData := expectData_1,
        handlerDispatched := handlerDispatched_1, pendingHead := pendingHead_1 } →
    machine = machine_1 ∧
      requestStream = requestStream_1 ∧
        keepAliveTimeout = keepAliveTimeout_1 ∧
          currentTimeout = currentTimeout_1 ∧
            headerTimeout = headerTimeout_1 ∧
              response = response_1 ∧
                respStream = respStream_1 ∧
                  requiresData = requiresData_1 ∧
                    expectData = expectData_1 ∧ handlerDispatched = handlerDispatched_1 ∧ pendingHead = pendingHead_1
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.WF.insertManyIfNewUnit : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ α] {m : Std.HashMap.Raw α Unit}
  {l : ρ}, m.WF → (m.insertManyIfNewUnit l).WF
-- Mathlib.Algebra.Category.Grp.Ulift
/-- The universe lift functor for commutative additive groups is fully faithful.  -/
AddCommGrpCat.uliftFunctorFullyFaithful : AddCommGrpCat.uliftFunctor.FullyFaithful
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval.linearMap_apply : ∀ (R : Type u_1) [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : Module R S] (x : S), (Polynomial.smeval.linearMap R x) p = p.smeval x
-- Mathlib.Order.LiminfLimsup
/-- Writing a limsup as an infimum of supremum, in a (possibly non-complete) conditionally complete
linear order. A reparametrization trick is needed to avoid taking the supremum of sets which are
not bounded above.  -/
Filter.HasBasis.limsup_eq_ciInf_ciSup : ∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : ConditionallyCompleteLinearOrder α] {v : Filter ι}
  {p : ι' → Prop} {s : ι' → Set ι} [inst_1 : Countable (Subtype p)] [inst_2 : Nonempty (Subtype p)],
  v.HasBasis p s →
    ∀ {f : ι → α},
      (∀ (j : Subtype p), (s ↑j).Nonempty) →
        (∃ j, BddAbove (Set.range fun i => f ↑i)) → Filter.limsup f v = ⨅ j, ⨆ i, f ↑i
-- Mathlib.Topology.Order.OrderClosed
Filter.Tendsto.min_right : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {f : β → α}
  {l : Filter β} {a : α}, Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun i => min a (f i)) l (nhds a)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsCycle.getVert_sub_one_ne_getVert_add_one : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {i : ℕ} {p : G.Walk u u},
  p.IsCycle → i ≤ p.length → p.getVert (i - 1) ≠ p.getVert (i + 1)
-- Mathlib.Algebra.GroupWithZero.Basic
div_self_mul_self' : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), a / (a * a) = a⁻¹
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RatAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ratAdd_sound : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)
  (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) (rupHints : Array ℕ)
  (ratHints : Array (ℕ × Array ℕ)) (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n),
  f.ReadyForRatAdd →
    pivot ∈ Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c →
      f.performRatAdd c pivot rupHints ratHints = (f', true) →
        Std.Tactic.BVDecide.LRAT.Internal.Equisat (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) f f'
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.div_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] [Lean.Grind.IsCharP α 0] (a b : α) (v₁ v₂ v : ℚ),
  (v == v₁ / v₂) = true →
    a = Lean.Grind.Field.NormNum.ofRat v₁ →
      b = Lean.Grind.Field.NormNum.ofRat v₂ → a / b = Lean.Grind.Field.NormNum.ofRat v
-- Mathlib.Order.Filter.AtTopBot.ModEq
Nat.frequently_odd : ∃ᶠ (m : ℕ) in Filter.atTop, Odd m
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- **Alias** of `BoxIntegral.Prepartition.injOn_setOfPred_mem_Icc_setOfPred_lower_eq`.

---

An auxiliary lemma used to prove that the same point can't belong to more than
`2 ^ Fintype.card ι` closed boxes of a prepartition.  -/
BoxIntegral.Prepartition.injOn_setOf_mem_Icc_setOf_lower_eq : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) (x : ι → ℝ),
  Set.InjOn (fun J => {i | J.lower i = x i}) {J | J ∈ π ∧ x ∈ BoxIntegral.Box.Icc J}
-- Mathlib.CategoryTheory.ConcreteCategory.Basic
/-- Convert a morphism of `C` to a bundled function.  -/
CategoryTheory.ConcreteCategory.hom : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {FC : outParam (C → C → Type u_1)} →
      {CC : outParam (C → Type w)} →
        {inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))} →
          [self : CategoryTheory.ConcreteCategory C FC] → {X Y : C} → (X ⟶ Y) → FC X Y
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_of_indep_of_le : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} {m₁ m₂ m₃ m₄ _mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α},
  ProbabilityTheory.Kernel.Indep m₁ m₂ κ μ → m₃ ≤ m₁ → m₄ ≤ m₂ → ProbabilityTheory.Kernel.Indep m₃ m₄ κ μ
-- Init.Data.SInt.Lemmas
Int16.toBitVec_toISize : ∀ (x : Int16), x.toISize.toBitVec = BitVec.signExtend System.Platform.numBits x.toBitVec
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.ofList_singleton : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {k : α}
  {v : β}, Std.ExtDHashMap.Const.ofList [(k, v)] = ∅.insert k v
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_inj : ∀ {a b : ONote} [a.NF] [b.NF], a.repr = b.repr ↔ a = b
-- Mathlib.Tactic.LinearCombination
/-- Result of `expandLinearCombo`, either an equality/inequality proof or a value.  -/
Mathlib.Tactic.LinearCombination.Expanded : Type
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- Let `ζ` be a primitive root of unity of order `n` with `2 ≤ n`. Any prime number that divides the
norm, relative to `ℤ`, of `ζ - 1` divides also `n`.
 -/
IsPrimitiveRoot.prime_dvd_of_dvd_norm_sub_one : ∀ {n : ℕ} (hn : 2 ≤ n) {K : Type u_1} [inst : Field K] [NumberField K] {ζ : K} {p : ℕ} [hF : Fact (Nat.Prime p)]
  (hζ : IsPrimitiveRoot ζ n), ↑p ∣ (Algebra.norm ℤ) (hζ.toInteger - 1) → p ∣ n
-- Mathlib.Algebra.Lie.DirectSum
/-- The fact that this instance is necessary seems to be a bug in typeclass inference. See
[this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Typeclass.20resolution.20under.20binders/near/245151099).  -/
DirectSum.lieRingOfIdeals : {R : Type u} →
  {ι : Type v} →
    [inst : CommRing R] →
      {L : Type w} →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] → (I : ι → LieIdeal R L) → LieRing (DirectSum ι fun i => ↥(I i))
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj adj' : F ⊣ G},
  adj = adj' ↔ adj.unit = adj'.unit
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.congr.eq_1 : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i ≃ₗ[R] t i),
  PiTensorProduct.congr f =
    LinearEquiv.ofLinearMap (PiTensorProduct.map fun i => ↑(f i)) (PiTensorProduct.map fun i => ↑(f i).symm) ⋯ ⋯
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
/-- Equivalence between an induced subgraph and its corresponding simple graph.  -/
SimpleGraph.Subgraph.coeInduceIso : {V : Type u} →
  {G : SimpleGraph V} →
    {G' : G.Subgraph} → (s : Set V) → s ⊆ G'.verts → (G'.induce s).coe ≃g SimpleGraph.induce {v | ↑v ∈ s} G'.coe
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- A fork on `f` and `g` is just a `Cone (parallelPair f g)`.  -/
CategoryTheory.Limits.Fork : {C : Type u} → {X Y : C} → [inst : CategoryTheory.Category.{v, u} C] → (X ⟶ Y) → (X ⟶ Y) → Type (max (max 0 u) v)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- An `affineCombination` with sum of weights 1 is in the
`affineSpan` of an indexed family, if the family is nonempty.  -/
affineCombination_mem_affineSpan_of_nonempty : ∀ {ι : Type u_1} {k : Type u_2} {V : Type u_3} {P : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [Nonempty ι] {s : Finset ι} {w : ι → k},
  ∑ i ∈ s, w i = 1 → ∀ (p : ι → P), (Finset.affineCombination k s p) w ∈ affineSpan k (Set.range p)
-- Init.Data.List.Find
List.findFinIdx?_nil : ∀ {α : Type u_1} {p : α → Bool}, List.findFinIdx? p [] = none
-- Init.Data.Bool
Bool.toNat_eq_one : ∀ {b : Bool}, b.toNat = 1 ↔ b = true
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_tsub_distrib : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [inst_2 : Sub M] [OrderedSub M]
  [AddLeftMono M] [AddLeftReflectLE M] [ExistsAddOfLE M] (s : Finset ι) {f g : ι → M},
  (∀ x ∈ s, g x ≤ f x) → ∑ x ∈ s, (f x - g x) = ∑ x ∈ s, f x - ∑ x ∈ s, g x
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.HasCofilteredLimitsOfSize.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (I : Type w) [inst_1 : CategoryTheory.Category.{w', w} I] [CategoryTheory.IsCofiltered I],
      CategoryTheory.Limits.HasLimitsOfShape I C) →
    CategoryTheory.Limits.HasCofilteredLimitsOfSize.{w', w, v, u} C
-- Init.Data.SInt.Lemmas
Int8.toInt16_toISize : ∀ (n : Int8), n.toISize.toInt16 = n.toInt16
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.sumToIter_C : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (a : R),
  (MvPolynomial.sumToIter R S₁ S₂) (MvPolynomial.C a) = MvPolynomial.C (MvPolynomial.C a)
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.symm_symm : ∀ {X : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G X] (f : Equidecomp X G), f.symm.symm = f
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.instFinalProdProd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor C' D')
  [F.Final] [G.Final], (F.prod G).Final
-- Init.Data.Array.Attach
/-- Maps an array of terms in a subtype to the corresponding terms in the type by forgetting that they
satisfy the predicate.

This is the inverse of `Array.attachWith` and a synonym for `xs.map (·.val)`.

Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such
as `map_subtype`, and is ideally subsequently simplified away by `unattach_attach`.

This function is usually inserted automatically by Lean as an intermediate step while proving
termination. It is rarely used explicitly in code. It is introduced as an intermediate step during
the elaboration of definitions by [well-founded
recursion](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=well-founded-recursion). If this function is encountered in a proof
state, the right approach is usually the tactic `simp [Array.unattach, -Array.map_subtype]`.
 -/
Array.unattach : {α : Type u_1} → {p : α → Prop} → Array { x // p x } → Array α
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_const_id_cobounded : ∀ {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F''] (c : F''),
  (fun x => c) =o[Bornology.cobounded E''] id
-- Mathlib.Topology.MetricSpace.Defs
MetricSpace.toPseudoMetricSpace : {α : Type u} → [self : MetricSpace α] → PseudoMetricSpace α
-- Mathlib.MeasureTheory.Measure.Haar.Quotient
/-- If `μ` on `G ⧸ Γ` satisfies `QuotientMeasureEqMeasurePreimage` relative to a both left- and
right-invariant measure on `G` and `Γ` is a normal subgroup, then `μ` is a left-invariant
measure.  -/
MeasureTheory.QuotientMeasureEqMeasurePreimage.mulInvariantMeasure_quotient : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : TopologicalSpace G] [IsTopologicalGroup G]
  [BorelSpace G] [PolishSpace G] {Γ : Subgroup G} [inst_6 : Γ.Normal] [T2Space (G ⧸ Γ)]
  [SecondCountableTopology (G ⧸ Γ)] {μ : MeasureTheory.Measure (G ⧸ Γ)} (ν : MeasureTheory.Measure G)
  [ν.IsMulLeftInvariant] [hasFun : MeasureTheory.HasFundamentalDomain (↥Γ.op) G ν]
  [MeasureTheory.QuotientMeasureEqMeasurePreimage ν μ], μ.IsMulLeftInvariant
-- Lean.Meta.Basic
Lean.Meta.mkFreshExprMVar : Option Lean.Expr →
  optParam Lean.MetavarKind Lean.MetavarKind.natural → optParam Lean.Name Lean.Name.anonymous → Lean.MetaM Lean.Expr
-- Lean.Meta.Tactic.TryThis
/-- Add a term suggestion.

The parameters are:
* `ref`: the span of the widget diagnostic
* `e`: the replacement expression
* `origSpan?`: a syntax object whose span is the actual text to be replaced by `suggestion`.
  If not provided it defaults to `ref`.
* `header`: a string which precedes the suggestion. By default, it's `"Try this:"`.
* `codeActionPrefix?`: an optional string to be used as the prefix of the replacement text if the
  suggestion does not have a custom `toCodeActionTitle?`. If not provided, `"Try this: "` is used.
 -/
Lean.Meta.Tactic.TryThis.addTermSuggestion : Lean.Syntax →
  Lean.Expr →
    optParam (Option Lean.Syntax) none → optParam String "Try this:" → optParam (Option String) none → Lean.MetaM Unit
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step.sizeOf_spec : ∀ (p : Lean.Grind.CommRing.Poly) (k₁ : ℤ) (d : Lean.Meta.Grind.Arith.CommRing.PolyDerivation) (k₂ : ℤ)
  (m₂ : Lean.Grind.CommRing.Mon) (c : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.PolyDerivation.step p k₁ d k₂ m₂ c) =
    1 + sizeOf p + sizeOf k₁ + sizeOf d + sizeOf k₂ + sizeOf m₂ + sizeOf c
-- Mathlib.AlgebraicGeometry.QuasiAffine
/-- A quasi-compact scheme is quasi-affine if
it can be covered by affine basic opens of global sections.  -/
AlgebraicGeometry.Scheme.IsQuasiAffine.of_forall_exists_mem_basicOpen : ∀ (X : AlgebraicGeometry.Scheme) [CompactSpace ↥X],
  (∀ (x : ↥X), ∃ r, AlgebraicGeometry.IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r) → X.IsQuasiAffine
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.homologyMap_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L M : HomologicalComplex C c} (φ : K ⟶ L) (ψ : L ⟶ M) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : M.HasHomology i],
  HomologicalComplex.homologyMap (CategoryTheory.CategoryStruct.comp φ ψ) i =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap φ i) (HomologicalComplex.homologyMap ψ i)
-- Mathlib.Algebra.Order.Module.Defs
SMulPosMono.toSMulPosReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : LinearOrder α] [inst_2 : Preorder β] [inst_3 : Zero β]
  [SMulPosMono α β], SMulPosReflectLT α β
-- Lean.Parser.Extra
Lean.Parser.antiquotExpr.formatter : Lean.PrettyPrinter.Formatter