mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.BitVec.Lemmas
/-- Equation theorem for `Int.mod`  -/
_private.Init.Data.BitVec.Lemmas.0.BitVec.Int.negSucc_emod : ∀ (m : ℕ) (n : ℤ), -(↑m + 1) % n = Int.subNatNat n.natAbs (m % n.natAbs + 1)
-- Mathlib.Order.CompactlyGenerated.Basic
exists_sSupIndep_of_sSup_atoms : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsModularLattice α] [IsCompactlyGenerated α] (b : α),
  sSup {a | a ≤ b ∧ IsAtom a} = b → ∃ s, sSupIndep s ∧ sSup s = b ∧ ∀ ⦃a : α⦄, a ∈ s → IsAtom a
-- Mathlib.Algebra.Torsor.Defs
/-- Dividing a point by itself produces 1.  -/
sdiv_self : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] (p : P), p /ₛ p = 1
-- Mathlib.NumberTheory.MulChar.Lemmas
MulChar.starComp_apply : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : StarRing R'] (χ : MulChar R R')
  (a : R), χ.starComp a = (starRingEnd R') (χ a)
-- Mathlib.Algebra.Order.Group.Basic
zsmul_lt_zsmul_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] {n : ℤ} {a b : α},
  0 < n → (n • a < n • b ↔ a < b)
-- Mathlib.Topology.IsLocalHomeomorph
Topology.IsOpenEmbedding.isLocalHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsOpenEmbedding f → IsLocalHomeomorph f
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_sum_of_subadditive : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β),
  f 0 ≤ 0 → (∀ (a b : α), f (a + b) ≤ f a + f b) → ∀ (s : Multiset α), f s.sum ≤ (Multiset.map f s).sum
-- Mathlib.Data.Finsupp.Single
Finsupp.single_swap : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (a₁ a₂ : α) (b : M), (fun₀ | a₁ => b) a₂ = (fun₀ | a₂ => b) a₁
-- Mathlib.GroupTheory.Index
AddSubgroup.isFiniteRelIndex_top_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.IsFiniteRelIndex ⊤ ↔ H.FiniteIndex
-- Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
/-- Given two colimit cokernel coforks `c₁` and `c₂` for `f₁ : X₁ ⟶ Y₁` and
`f₂ : X₂ ⟶ Y₂`, if the cokernels of `f₁` and `f₂` are preserves by suitable
tensor products, then `c₁.pt ⊗ c₂.pt` is the cokernel of the
morphism `(X₁ ⊗ Y₂) ⨿ (Y₁ ⊗ X₂) ⟶ Y₁ ⊗ Y₂`.  -/
CategoryTheory.Limits.CokernelCofork.isColimitTensor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.MonoidalCategory C] →
        [inst_3 : CategoryTheory.MonoidalPreadditive C] →
          {X₁ Y₁ : C} →
            {f₁ : X₁ ⟶ Y₁} →
              {c₁ : CategoryTheory.Limits.CokernelCofork f₁} →
                CategoryTheory.Limits.IsColimit c₁ →
                  {X₂ Y₂ : C} →
                    {f₂ : X₂ ⟶ Y₂} →
                      {c₂ : CategoryTheory.Limits.CokernelCofork f₂} →
                        CategoryTheory.Limits.IsColimit c₂ →
                          [inst_4 :
                              CategoryTheory.Limits.HasBinaryCoproduct
                                (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₂)
                                (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ X₂)] →
                            [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0)
                                  (CategoryTheory.MonoidalCategory.tensorLeft c₁.pt)] →
                              [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0)
                                    (CategoryTheory.MonoidalCategory.tensorRight Y₂)] →
                                [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0)
                                      (CategoryTheory.MonoidalCategory.tensorRight X₂)] →
                                  CategoryTheory.Limits.IsColimit (c₁.tensor c₂)
-- Lean.ExtraModUses
Lean.instReprExtraModUse : Repr Lean.ExtraModUse
-- Lean.Elab.Command
Lean.Elab.Command.State.mk.injEq : ∀ (env : Lean.Environment) (messages : Lean.MessageLog) (scopes : List Lean.Elab.Command.Scope)
  (usedQuotCtxts : Lean.NameSet) (nextMacroScope maxRecDepth : ℕ) (ngen : Lean.NameGenerator)
  (auxDeclNGen : Lean.DeclNameGenerator) (infoState : Lean.Elab.InfoState) (traceState : Lean.TraceState)
  (snapshotTasks : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) (env_1 : Lean.Environment)
  (messages_1 : Lean.MessageLog) (scopes_1 : List Lean.Elab.Command.Scope) (usedQuotCtxts_1 : Lean.NameSet)
  (nextMacroScope_1 maxRecDepth_1 : ℕ) (ngen_1 : Lean.NameGenerator) (auxDeclNGen_1 : Lean.DeclNameGenerator)
  (infoState_1 : Lean.Elab.InfoState) (traceState_1 : Lean.TraceState)
  (snapshotTasks_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  ({ env := env, messages := messages, scopes := scopes, usedQuotCtxts := usedQuotCtxts,
        nextMacroScope := nextMacroScope, maxRecDepth := maxRecDepth, ngen := ngen, auxDeclNGen := auxDeclNGen,
        infoState := infoState, traceState := traceState, snapshotTasks := snapshotTasks } =
      { env := env_1, messages := messages_1, scopes := scopes_1, usedQuotCtxts := usedQuotCtxts_1,
        nextMacroScope := nextMacroScope_1, maxRecDepth := maxRecDepth_1, ngen := ngen_1, auxDeclNGen := auxDeclNGen_1,
        infoState := infoState_1, traceState := traceState_1, snapshotTasks := snapshotTasks_1 }) =
    (env = env_1 ∧
      messages = messages_1 ∧
        scopes = scopes_1 ∧
          usedQuotCtxts = usedQuotCtxts_1 ∧
            nextMacroScope = nextMacroScope_1 ∧
              maxRecDepth = maxRecDepth_1 ∧
                ngen = ngen_1 ∧
                  auxDeclNGen = auxDeclNGen_1 ∧
                    infoState = infoState_1 ∧ traceState = traceState_1 ∧ snapshotTasks = snapshotTasks_1)
-- Mathlib.Data.Fintype.BigOperators
Fintype.card_pi : ∀ {ι : Type u_4} {α : ι → Type u_6} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : (i : ι) → Fintype (α i)],
  Fintype.card ((i : ι) → α i) = ∏ i, Fintype.card (α i)
-- Std.Sync.SharedMutex
/-- `mutex.atomically k` runs `k` with read and write access to the mutex's state while locking the
mutex for exclusive write access.

Calling `mutex.atomically` while already holding the underlying `BaseSharedMutex` in the same thread
is undefined behavior.
 -/
Std.SharedMutex.atomically : {m : Type → Type} →
  {α β : Type} → [Monad m] → [MonadLiftT BaseIO m] → [MonadFinally m] → Std.SharedMutex α → Std.AtomicT α m β → m β
-- Init.Data.Int.Order
Int.nonneg_of_mul_nonpos_right : ∀ {a b : ℤ}, a * b ≤ 0 → a < 0 → 0 ≤ b
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_apply_ite : ∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} [inst : AddCommMonoid M] {s : Finset ι} {p : ι → Prop}
  [inst_1 : DecidablePred p] (f g : ι → γ) (h : γ → M),
  ∑ x ∈ s, h (if p x then f x else g x) = ∑ x ∈ s with p x, h (f x) + ∑ x ∈ s with ¬p x, h (g x)
-- Mathlib.Data.Num.ZNum
ZNum.ofInt'.eq_2 : ∀ (n : ℕ), ZNum.ofInt' (Int.negSucc n) = (Num.ofNat' (n + 1)).toZNumNeg
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.mem_range : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W) (f : ρ.IntertwiningMap σ) (w : W),
  w ∈ Representation.IntertwiningMap.range ρ σ f ↔ ∃ v, f v = w
-- Mathlib.Data.ZMod.QuotientGroup
/-- See also `Fintype.card_zmultiples`.  -/
Nat.card_zmultiples : ∀ {α : Type u_3} [inst : AddGroup α] (a : α), Nat.card ↥(AddSubgroup.zmultiples a) = addOrderOf a
-- Mathlib.Topology.Bornology.Hom
LocallyBoundedMap.mk.inj : ∀ {α : Type u_6} {β : Type u_7} {inst : Bornology α} {inst_1 : Bornology β} {toFun : α → β}
  {comap_cobounded_le' : Filter.comap toFun (Bornology.cobounded β) ≤ Bornology.cobounded α} {toFun_1 : α → β}
  {comap_cobounded_le'_1 : Filter.comap toFun_1 (Bornology.cobounded β) ≤ Bornology.cobounded α},
  { toFun := toFun, comap_cobounded_le' := comap_cobounded_le' } =
      { toFun := toFun_1, comap_cobounded_le' := comap_cobounded_le'_1 } →
    toFun = toFun_1
-- Init.Data.UInt.Lemmas
USize.ofInt_add : ∀ (x y : ℤ), USize.ofInt (x + y) = USize.ofInt x + USize.ofInt y
-- Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant
AlgebraicGeometry.Scheme.Hom.app_injective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsSchemeTheoreticallyDominant f]
  [AlgebraicGeometry.QuasiCompact f] (U : Y.Opens),
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Hom.app f U))
-- Init.Prelude
/-- Boolean equality, notated as `a == b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `==` in identifiers is `beq`. -/
BEq.beq : {α : Type u} → [self : BEq α] → α → α → Bool
-- Mathlib.NumberTheory.ArithmeticFunction.LFunction
ArithmeticFunction.isMultiplicative_eulerProduct : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] (f : ι → ArithmeticFunction R),
  (∀ (i : ι), (f i).IsMultiplicative) → (ArithmeticFunction.eulerProduct f).IsMultiplicative
-- Mathlib.RingTheory.Smooth.NoetherianDescent
_private.Mathlib.RingTheory.Smooth.NoetherianDescent.0.Algebra.Smooth.DescentAux.hphom : ∀ {A : Type u} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  (self : Algebra.Smooth.DescentAux✝ A B) (j : Algebra.Smooth.DescentAux.rels✝ self),
  (Algebra.Smooth.DescentAux.p✝ self j).IsHomogeneous 2
-- Mathlib.Topology.DiscreteSubset
/-- In a `T1Space`, complements of finite sets are codiscrete within any set.
 -/
compl_finite_mem_codiscreteWithin : ∀ {X : Type u_3} [inst : TopologicalSpace X] [T1Space X] {s t : Set X}, t.Finite → tᶜ ∈ Filter.codiscreteWithin s
-- Mathlib.Geometry.Euclidean.Projection
/-- The characteristic property of the orthogonal projection, for a point given in the underlying
space. This form is typically more convenient to use than
`inter_eq_singleton_orthogonalProjection`.  -/
EuclideanGeometry.coe_orthogonalProjection_eq_iff_mem : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {s : AffineSubspace 𝕜 P}
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] {p q : P},
  ↑((EuclideanGeometry.orthogonalProjection s) p) = q ↔ q ∈ s ∧ p -ᵥ q ∈ s.directionᗮ
-- Mathlib.Algebra.Group.Pi.Basic
Pi.addRightCancelSemigroup.eq_1 : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → AddRightCancelSemigroup (f i)],
  Pi.addRightCancelSemigroup = { toAddSemigroup := Pi.addSemigroup, toIsRightCancelAdd := ⋯ }
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.simprocs : Lean.Meta.SimpAll.State → Lean.Meta.Simp.SimprocsArray
-- Mathlib.Algebra.Order.Monoid.OrderDual
OrderDual.isOrderedCancelMonoid : ∀ {α : Type u} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedCancelMonoid α], IsOrderedCancelMonoid αᵒᵈ
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.Equiv.symm_symm : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Equiv M N), f.symm.symm = f
-- Mathlib.Algebra.Group.Semiconj.Defs
SemiconjBy.pow_right : ∀ {M : Type u_2} [inst : Monoid M] {a x y : M}, SemiconjBy a x y → ∀ (n : ℕ), SemiconjBy a (x ^ n) (y ^ n)
-- Init.Data.SInt.Lemmas
ISize.mod_one : ∀ {a : ISize}, a % 1 = 0
-- Mathlib.Combinatorics.SimpleGraph.StronglyRegular
SimpleGraph.IsSRGWith.congr_simp : ∀ {V : Type u} [inst : Fintype V] (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj] (n n_1 : ℕ),
      n = n_1 →
        ∀ (k k_1 : ℕ),
          k = k_1 →
            ∀ (ℓ ℓ_1 : ℕ), ℓ = ℓ_1 → ∀ (μ μ_1 : ℕ), μ = μ_1 → G.IsSRGWith n k ℓ μ = G_1.IsSRGWith n_1 k_1 ℓ_1 μ_1
-- Mathlib.Tactic.Core
/-- `iterateRange m n t`: Repeat the given tactic at least `m` times and
at most `n` times or until `t` fails. Fails if `t` does not run at least `m` times.
 -/
Lean.Elab.Tactic.iterateRange : {m : Type → Type u} → [Monad m] → [MonadExcept Lean.Exception m] → ℕ → ℕ → m Unit → m Unit
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
/-- Monoid homomorphisms from `ULift ℕ` are defined by the image of `1`.  -/
uliftMultiplesHom : (M : Type u) → [inst : AddMonoid M] → M ≃ (ULift.{u, 0} ℕ →+ M)
-- Mathlib.Data.ZMod.Defs
/-- The integers modulo `n : ℕ`.  -/
ZMod : ℕ → Type
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.commaFromUnder_map_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {X_1 Y : CategoryTheory.Functor J (CategoryTheory.Under X)} (f : X_1 ⟶ Y),
  (CategoryTheory.WithInitial.commaFromUnder.map f).right =
    CategoryTheory.Functor.whiskerRight f (CategoryTheory.Under.forget X)
-- Init.Data.String.OrderInstances
String.Slice.Pos.instTotalLe : ∀ {s : String.Slice}, Std.Total fun x1 x2 => x1 ≤ x2
-- Init.Data.SInt.Lemmas
Int8.ofIntTruncate_toInt : ∀ (x : Int8), Int8.ofIntClamp x.toInt = x
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- A family of units is of maximal rank if its image by `logEmbedding` is linearly independent
over `ℝ`.
 -/
NumberField.Units.IsMaxRank : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] → (Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ) → Prop
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- If the inner product of two unit vectors is `-1`, then the two vectors are negations of each
other.  -/
inner_eq_neg_one_iff_of_norm_eq_one : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {x y : E}, ‖x‖ = 1 → ‖y‖ = 1 → (inner 𝕜 x y = -1 ↔ x = -y)
-- Mathlib.Analysis.Calculus.FDeriv.WithLp
hasStrictFDerivAt_piLp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup H] [inst_2 : (i : ι) → NormedAddCommGroup (E i)] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_4 : NormedSpace 𝕜 H] [Finite ι] (p : ENNReal) [Fact (1 ≤ p)] {f : H → PiLp p E} {f' : H →L[𝕜] PiLp p E} {y : H},
  HasStrictFDerivAt f f' y ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => (f x).ofLp i) (PiLp.proj p E i ∘SL f') y
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} A]
  {J : CategoryTheory.GrothendieckTopology C} {S : C} {E : J.OneHypercover S} {F : CategoryTheory.Sheaf J A}
  (c : CategoryTheory.Limits.Multifork (E.multicospanIndex F.obj)) (i₀ : E.I₀),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.GrothendieckTopology.OneHypercover.multiforkLift c)
      (F.obj.map (E.f i₀).op) =
    c.ι i₀
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Two equivalent partial equivs are equal when the source and target are `univ`.  -/
PartialEquiv.eq_of_eqOnSource_univ : ∀ {α : Type u_1} {β : Type u_2} (e e' : PartialEquiv α β), e ≈ e' → e.source = Set.univ → e.target = Set.univ → e = e'
-- Mathlib.Order.Antichain
IsAntichain.preimage_relEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {t : Set β},
  IsAntichain r' t → ∀ (φ : r ↪r r'), IsAntichain r (⇑φ ⁻¹' t)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.congr_simp : ∀ (pat pat_1 : ByteArray) (e_pat : pat = pat_1) (stackPos stackPos_1 : ℕ) (e_stackPos : stackPos = stackPos_1)
  (hst : stackPos < pat.size),
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat stackPos hst =
    String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ pat_1 stackPos_1 ⋯
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.compare_ne_iff_beq_eq_false : ∀ {α : Type u} {instOrd : Ord α} {a b : α}, compare a b ≠ Ordering.eq ↔ (a == b) = false
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.lcm_neg_right : ∀ (a b : ℤ), a.lcm (-b) = a.lcm b
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instAddCommMonoid : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddCommMonoid β] → [ContinuousAdd β] → AddCommMonoid (ZeroAtInftyContinuousMap α β)
-- Mathlib.Topology.Covering.AddCircle
AddCircle.isAddQuotientCoveringMap_nsmul : ∀ {𝕜 : Type u_1} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [IsTopologicalRing 𝕜] (p : 𝕜) [T0Space (AddCircle p)]
  {n : ℕ}, IsUnit ↑n → IsAddQuotientCoveringMap (fun x => n • x) ↥(nsmulAddMonoidHom n).ker
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.mem_normalizer_iff_map_addConj_eq : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {g : G},
  g ∈ AddSubgroup.normalizer ↑H ↔ AddSubgroup.map (↑(AddAut.addConj g)) H = H
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_indicator : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ (f : α → ENNReal), μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.of_subset : ∀ {M : Type u_1} {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] {A B : Set X}, A ⊆ B → CovBySMul M 1 A B
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_toReal_atBot : Filter.Tendsto EReal.toReal (nhdsWithin ⊥ {⊥}ᶜ) Filter.atBot
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_bot : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] (c : ℝ) (f : α → E) (g : α → F),
  Asymptotics.IsBigOWith c ⊥ f g
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instSubtractionMonoidOfAddOpposite : {M : Type u_1} → [SubtractionMonoid Mᵃᵒᵖ] → SubtractionMonoid Mᵈᵃᵃ
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.unop_X' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  (φ : W.LeftFraction X Y), φ.unop.X' = Opposite.unop φ.Y'
-- Init.Omega.IntList
Lean.Omega.IntList.mul_cons_cons : ∀ {x : ℤ} {xs : List ℤ} {y : ℤ} {ys : List ℤ}, (x :: xs) * (y :: ys) = x * y :: xs * ys
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.IsTerminal.subsingleton_to : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C] {I : C}
  (hI : CategoryTheory.Limits.IsTerminal I) {A : C}, Subsingleton (I ⟶ A)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.eval.eq_10 : ∀ {w : ℕ} (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (n : ℕ) (rhs : Std.Tactic.BVDecide.BVExpr n)
  (lhs : Std.Tactic.BVDecide.BVExpr w),
  Std.Tactic.BVDecide.BVExpr.eval assign (lhs.arithShiftRight rhs) =
    (Std.Tactic.BVDecide.BVExpr.eval assign lhs).sshiftRight' (Std.Tactic.BVDecide.BVExpr.eval assign rhs)
-- Mathlib.Data.Multiset.Basic
Multiset.strongDownwardInduction.eq_def : ∀ {α : Type u_1} {p : Multiset α → Sort u_3} {n : ℕ}
  (H : (t₁ : Multiset α) → ({t₂ : Multiset α} → t₂.card ≤ n → t₁ < t₂ → p t₂) → t₁.card ≤ n → p t₁) (s : Multiset α),
  Multiset.strongDownwardInduction H s = H s fun {t} ht _h => Multiset.strongDownwardInduction H t ht
-- Mathlib.Order.Interval.Basic
Interval.bot_ne_pure : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, ⊥ ≠ Interval.pure a
-- Mathlib.Analysis.Convex.Intrinsic
subset_intrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, s ⊆ intrinsicClosure 𝕜 s
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- The region between two measurable functions on a measurable set is measurable;
a version for the region together with the graph of the lower function.  -/
measurableSet_region_between_co : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f g : α → ℝ} {s : Set α},
  Measurable f → Measurable g → MeasurableSet s → MeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Set.Ico (f p.1) (g p.1)}
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.instHasCountableLimits : CategoryTheory.Limits.HasCountableLimits LightProfinite
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCocircuit.subset_ground : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCocircuit C → C ⊆ M.E
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_le_one_of_one_le_of_nonpos : ∀ {x z : ℝ}, 1 ≤ x → z ≤ 0 → x ^ z ≤ 1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass.mk : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {γ : Type u_1}
  {op :
    γ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  [toFriendlyOperationClass : Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass op],
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_insertManyIfNewUnit_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α fun x => Unit} [EquivBEq α] [LawfulHashable α]
  {l : List α} {k : α},
  Std.DHashMap.Const.get? (Std.DHashMap.Const.insertManyIfNewUnit m l) k =
    if k ∈ m ∨ l.contains k = true then some () else none
-- Aesop.Search.Expansion
Aesop.addRapps : {Q : Type} →
  [inst : Aesop.Queue Q] →
    Aesop.GoalRef → Aesop.RegularRule → Array Aesop.RuleApplication → Aesop.SearchM Q Aesop.RuleResult
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.domain_mkSpanSingleton : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (x : E) (y : F)
  (H : ∀ (c : R), c • x = 0 → σ c • y = 0), (LinearPMap.mkSpanSingleton' x y H).domain = R ∙ x
-- Lean.Elab.App
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.getResultingTypeCore?.main' : Bool → Bool → ℕ → ℕ → ℕ → List Lean.Elab.Term.NamedArg → Lean.Expr → Lean.Elab.TermElabM (Option Lean.Expr)
-- Mathlib.Algebra.Category.MonCat.Adjunctions
AddCommMonCat.free_obj_coe : ∀ (α : Type u), ↑(AddCommMonCat.free.obj α) = (α →₀ ℕ)
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuousWithinAt.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {x : α} {s t : Set α},
  UpperSemicontinuousWithinAt f s x → t ⊆ s → UpperSemicontinuousWithinAt f t x
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- `affineCombination` gives the sum with any base point, when the
sum of the weights is 1.  -/
Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : ι → P),
  ∑ i ∈ s, w i = 1 → ∀ (b : P), (Finset.affineCombination k s p) w = (s.weightedVSubOfPoint p b) w +ᵥ b
-- Mathlib.Algebra.Homology.ExactSequence
CategoryTheory.ComposableArrows.Exact.δ₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 2)}, S.Exact → S.δ₀.Exact
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.abstractNestedProofs : Lean.Elab.PreDefinition → optParam Bool true → Lean.MetaM Lean.Elab.PreDefinition
-- Mathlib.Algebra.Group.Subgroup.Basic
MulAut.characteristic_apply_apply_coe : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Characteristic] (φ : MulAut G) (h : ↥H),
  ↑(((MulAut.characteristic H) φ) h) = φ ↑h
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokensOptions.toJson : Lean.Lsp.SemanticTokensOptions → Lean.Json