mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Partial assignment being constructed by linarith.  -/
Lean.Meta.Grind.Arith.Linear.Struct.assignment : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PArray ℚ
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.prod_map_mul : ∀ {ι : Type u_1} {M : Type u_8} [inst : CommMonoid M] {l : List ι} {f g : ι → M},
  (List.map (fun i => f i * g i) l).prod = (List.map f l).prod * (List.map g l).prod
-- Mathlib.GroupTheory.QuotientGroup.Finite
finite_iff_addSubgroup_quotient : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G), Finite G ↔ Finite ↥H ∧ Finite (G ⧸ H)
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instSMulIntHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → SMul ℤ (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.operation_bind_eq_operation_bind_mk : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] {x : Std.Iterators.PostconditionT m α}
  {f : Subtype x.Property → m β},
  x.operation >>= f = do
    let a ← x.operation
    f ⟨↑a, ⋯⟩
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.isCycle_swap_mul_aux₁ : ∀ {α : Type u_4} [inst : DecidableEq α] (n : ℕ) {b x : α} {f : Equiv.Perm α},
  (Equiv.swap x (f x) * f) b ≠ b → (f ^ n) (f x) = b → ∃ i, ((Equiv.swap x (f x) * f) ^ i) (f x) = b
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `Ring` instance along an injective function.  -/
Function.Injective.ring : {R : Type u_1} →
  {S : Type u_2} →
    (f : S → R) →
      Function.Injective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : One S] →
                [inst_4 : Neg S] →
                  [inst_5 : Sub S] →
                    [inst_6 : SMul ℕ S] →
                      [inst_7 : SMul ℤ S] →
                        [inst_8 : Pow S ℕ] →
                          [inst_9 : NatCast S] →
                            [inst_10 : IntCast S] →
                              [inst_11 : Ring R] →
                                f 0 = 0 →
                                  f 1 = 1 →
                                    (∀ (x y : S), f (x + y) = f x + f y) →
                                      (∀ (x y : S), f (x * y) = f x * f y) →
                                        (∀ (x : S), f (-x) = -f x) →
                                          (∀ (x y : S), f (x - y) = f x - f y) →
                                            (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                              (∀ (n : ℤ) (x : S), f (n • x) = n • f x) →
                                                (∀ (x : S) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                  (∀ (n : ℕ), f ↑n = ↑n) → (∀ (n : ℤ), f ↑n = ↑n) → Ring S
-- Mathlib.AlgebraicGeometry.Morphisms.Descent
/-- Let `P` be a morphism property associated with `affineAnd Q`. Suppose

- `P'` implies `Q'` on global sections on affine schemes,
- `P'` is satisfied for surjective, local isomorphisms,
- affine morphisms descend along `P''`, and
- `Q` codescends along `Q'`,

Then `P` descends along quasi-compact morphisms satisfying `P'`.

Note: The second condition is in particular satisfied for faithfully flat morphisms.
 -/
AlgebraicGeometry.HasAffineProperty.descendsAlong_of_affineAnd : ∀ (P P' : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  (Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) [P'.IsStableUnderBaseChange]
  [P'.IsStableUnderComposition] [P.IsStableUnderBaseChange],
  @AlgebraicGeometry.IsLocalIso ⊓ @AlgebraicGeometry.Surjective ≤ P' →
    (∀ {R S : CommRingCat} {f : R ⟶ S}, P' (AlgebraicGeometry.Spec.map f) → Q' (CommRingCat.Hom.hom f)) →
      AlgebraicGeometry.HasAffineProperty P (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) →
        ∀ [CategoryTheory.MorphismProperty.DescendsAlong (@AlgebraicGeometry.IsAffineHom) P'],
          (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
            (RingHom.CodescendsAlong (fun {R S} [CommRing R] [CommRing S] => Q) fun {R S} [CommRing R] [CommRing S] =>
                Q') →
              P.DescendsAlong (P' ⊓ @AlgebraicGeometry.QuasiCompact)
-- Aesop.Tree.UnsafeQueue
Aesop.PostponedSafeRule.mk.sizeOf_spec : ∀ (rule : Aesop.SafeRule) (output : Aesop.RuleTacOutput),
  sizeOf { rule := rule, output := output } = 1 + sizeOf rule + sizeOf output
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
/-- `f` is line-differentiable at the point `x` in the direction `v` in the set `s` if there
exists `f'` such that `f (x + t v) = f x + t • f' + o (t)` when `t` tends to `0` and `x + t v ∈ s`.
 -/
LineDifferentiableWithinAt : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {F : Type u_2} →
      [inst_1 : NormedAddCommGroup F] →
        [NormedSpace 𝕜 F] → {E : Type u_3} → [inst_3 : AddCommGroup E] → [Module 𝕜 E] → (E → F) → Set E → E → E → Prop
-- Mathlib.Algebra.Group.Conj
isAddConj_comm : ∀ {α : Type u} [inst : AddMonoid α] {g h : α}, IsAddConj g h ↔ IsAddConj h g
-- Mathlib.Algebra.NonAssoc.LieAdmissible.Defs
LieAdmissibleRing.toNonUnitalNonAssocRing : {L : Type u_1} → [self : LieAdmissibleRing L] → NonUnitalNonAssocRing L
-- Mathlib.GroupTheory.QuotientGroup.Defs
AddCon.addSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (c : AddCon G),
  c.addSubgroup = { carrier := {x | c x 0}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Analysis.Normed.Algebra.Exponential
/-- If a normed ring `𝔸` is a normed algebra over two fields, then they define the same
`expSeries` on `𝔸`.  -/
NormedSpace.expSeries_eq_expSeries : ∀ (𝕂 : Type u_1) (𝕂' : Type u_2) (𝔸 : Type u_3) [inst : Field 𝕂] [inst_1 : Field 𝕂'] [inst_2 : Ring 𝔸]
  [inst_3 : Algebra 𝕂 𝔸] [inst_4 : Algebra 𝕂' 𝔸] [inst_5 : TopologicalSpace 𝔸] [inst_6 : IsTopologicalRing 𝔸] (n : ℕ)
  (x : 𝔸), ((NormedSpace.expSeries 𝕂 𝔸 n) fun x_1 => x) = (NormedSpace.expSeries 𝕂' 𝔸 n) fun x_1 => x
-- Lean.Compiler.LCNF.PublicDeclsExt
Lean.Compiler.LCNF.setDeclPublic : Lean.Environment → Lean.Name → Lean.Environment
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.linearEquivFunOnFintype_symm_apply : ∀ {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : Fintype ι] (a : (i : ι) → M i),
  DFinsupp.linearEquivFunOnFintype.symm a = DFinsupp.equivFunOnFintype.symm a
-- Mathlib.Order.SupClosed
/-- A set `s` is a *sublattice* if `a ⊔ b ∈ s` and `a ⊓ b ∈ s` for all `a ∈ s`, `b ∈ s`.
Note: This is not the preferred way to declare a sublattice. One should instead use `Sublattice`.
TODO: Define `Sublattice`.  -/
IsSublattice : {α : Type u_3} → [Lattice α] → Set α → Prop
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.NPow.eq_1 : ∀ {α : Type u_2} [inst : One α] [inst_1 : Mul α], Set.NPow = { pow := fun s n => npowRec n s }
-- Mathlib.Algebra.CharP.Lemmas
add_pow_prime_pow_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ},
  Nat.Prime p →
    ∀ (x y : R) (n : ℕ),
      (x + y) ^ p ^ n =
        x ^ p ^ n + y ^ p ^ n +
          ↑p * x * y * ∑ k ∈ Finset.Ioo 0 (p ^ n), x ^ (k - 1) * y ^ (p ^ n - k - 1) * ↑((p ^ n).choose k / p)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A version of `Set.pi` for `Submonoid`s. Given an index set `I` and a family of `Submonoid`s
`s : Π i, Submonoid f i`, `pi I s` is the `Submonoid` of dependent functions `f : Π i, f i` such
that `f i` belongs to `Pi I s` whenever `i ∈ I`.  -/
Submonoid.pi : {ι : Type u_4} →
  {M : ι → Type u_5} →
    [inst : (i : ι) → MulOneClass (M i)] → Set ι → ((i : ι) → Submonoid (M i)) → Submonoid ((i : ι) → M i)
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.IsSubgraph.edgeSet_mono : ∀ {α : Type u_1} {β : Type u_2} {G H : Graph α β}, H ≤ G → H.edgeSet ⊆ G.edgeSet
-- Mathlib.GroupTheory.Coset.Basic
normal_of_eq_cosets : ∀ {α : Type u_1} [inst : Group α] (s : Subgroup α), (∀ (g : α), g • ↑s = MulOpposite.op g • ↑s) → s.Normal
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
/-- **Alias** of the reverse direction of `contMDiffAt_iff_contDiffAt`. -/
ContDiffAt.contMDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {x : E},
  ContDiffAt 𝕜 n f x → ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f x
-- Mathlib.Topology.PartitionOfUnity
/-- If `X` is a normal topological space and `U i`, `i : ι`, is a locally finite open covering of a
closed set `s`, then there exists a `BumpCovering ι X s` that is subordinate to `U`. If `X` is a
paracompact space, then the assumption `hf : LocallyFinite U` can be omitted, see
`BumpCovering.exists_isSubordinate`.  -/
BumpCovering.exists_isSubordinate_of_locallyFinite : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] {s : Set X} [NormalSpace X],
  IsClosed s → ∀ (U : ι → Set X), (∀ (i : ι), IsOpen (U i)) → LocallyFinite U → s ⊆ ⋃ i, U i → ∃ f, f.IsSubordinate U
-- Lean.Parser.Module
Lean.Parser.parseHeader : Lean.Parser.InputContext →
  IO (Lean.TSyntax `Lean.Parser.Module.header × Lean.Parser.ModuleParserState × Lean.MessageLog)
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.addCommute_iff_neg_add_cancel_assoc : ∀ {M : Type u_1} [inst : AddMonoid M] {u : AddUnits M} {a : M}, AddCommute (↑u) a ↔ ↑(-u) + (a + ↑u) = a
-- Mathlib.Algebra.BigOperators.Intervals
Finset.sum_Ico_eq_sum_range : ∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ → M) (m n : ℕ),
  ∑ k ∈ Finset.Ico m n, f k = ∑ k ∈ Finset.range (n - m), f (m + k)
-- Mathlib.Logic.Equiv.Multiset
Denumerable.raise.eq_2 : ∀ (x m : ℕ) (l : List ℕ), Denumerable.raise (m :: l) x = (m + x) :: Denumerable.raise l (m + x)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.erase0 : Lean.Meta.Grind.AC.DiseqCnstr → Lean.Meta.Grind.AC.DiseqCnstrProof
-- Mathlib.Topology.Inseparable
Specializes.not_disjoint : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y → ¬Disjoint (nhds x) (nhds y)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nndist_toLp_fst : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x₁ x₂ : α), nndist (WithLp.toLp p (x₁, 0)) (WithLp.toLp p (x₂, 0)) = nndist x₁ x₂
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.modularCharacterFun_map_mul : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : LocallyCompactSpace G] (g h : G),
  MeasureTheory.Measure.modularCharacterFun (g * h) =
    MeasureTheory.Measure.modularCharacterFun g * MeasureTheory.Measure.modularCharacterFun h
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : EquivBEq α] [inst_1 : LawfulHashable α] {f : (a : α) → β a → γ a} {k : α} {h' : k ∈ Std.ExtDHashMap.map f m},
  (Std.ExtDHashMap.map f m).getKey k h' = m.getKey k ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isEmpty_inter_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  (t₁ ∩ t₂).isEmpty = true ↔ ∀ k ∈ t₁, k ∉ t₂
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
AlgebraicGeometry.Scheme.Hom.injective : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.UniversallyInjective f], Function.Injective ⇑f
-- Mathlib.Algebra.GroupWithZero.Defs
CommGroupWithZero.toZPow : {G₀ : Type u_2} → [self : CommGroupWithZero G₀] → ZPow G₀
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.subtype.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M] (p : SubMulAction R M),
  p.subtype = { toFun := Subtype.val, map_smul' := ⋯ }
-- Mathlib.Algebra.Group.Prod
Prod.fst_mul_snd : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (p : M × N), (p.1, 1) * (1, p.2) = p
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, (t.alter k f).getKey? k = if (f t[k]?).isSome = true then some k else none
-- Mathlib.Data.Option.Defs
/-- An elimination principle for `Option`. It is a nondependent version of `Option.rec`.  -/
Option.elim' : {α : Type u_1} → {β : Type u_2} → β → (α → β) → Option α → β
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
SimplexCategory.σ_σ₀Iter'_assoc : ∀ (i : ℕ) {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : autoParam (n + i = m) SimplexCategory.σ_σ₀Iter'._auto_1),
  autoParam (↑j = ↑j' + i) SimplexCategory.σ_σ₀Iter'._auto_3 →
    ∀ {Z : SimplexCategory} (h : { len := n } ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter i hi) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategory.σ₀Iter i ⋯)
          (CategoryTheory.CategoryStruct.comp (SimplexCategory.σ j') h)
-- Lean.Meta.Match.Value
/-- Return true is `e` is a term that should be processed by the `match`-compiler using `casesValues`  -/
Lean.Meta.isMatchValue : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.compLeft_h₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₃ ⟶ S₁), (h.compLeft ψ).h₃ = CategoryTheory.CategoryStruct.comp ψ.τ₃ h.h₃
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.locallySmall : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C}
  [self : CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.LocallySmall.{w, v, u} C
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
/-- A variant of `Subtype.casesOn` that is not reduced by `simp`.  -/
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.Std.Internal.subtypeCasesOn' : {α : Sort u_1} →
  {p : α → Prop} →
    {motive : Subtype p → Sort u_2} →
      (t : Subtype p) → ((val : α) → (property : p val) → motive ⟨val, property⟩) → motive t
-- Lean.Meta.Sym.SymM
/-- `ShareCommon` (aka `Hash-consing`) state.  -/
Lean.Meta.Sym.State.share : Lean.Meta.Sym.State → Lean.Meta.Sym.AlphaShareCommon.State
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_neg : ∀ (z : Complex.UnitClosedDisc), ↑(-z) = -↑z
-- Std.Data.String.ToNat
String.Slice.isNat_of_isDigit : ∀ {s : String.Slice}, s.isEmpty = false → (∀ c ∈ s.copy.toList, c.isDigit = true) → s.isNat = true
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.diffHypotheses : Bool →
  Lean.LocalContext →
    Array Lean.Widget.InteractiveHypothesisBundle → Lean.MetaM (Array Lean.Widget.InteractiveHypothesisBundle)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_union : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α},
  Std.ExtDTreeMap.Const.get! (t₁.union t₂) k = Std.ExtDTreeMap.Const.getD t₂ k (Std.ExtDTreeMap.Const.get! t₁ k)
-- Batteries.Data.List.Lemmas
List.insertP_loop : ∀ {α : Type u_1} {p : α → Bool} (a : α) (l r : List α), List.insertP.loop p a l r = r.reverseAux (List.insertP p a l)
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_comap : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {H : Subgroup N} [nH : H.Normal] (f : G →* N),
  (Subgroup.comap f H).Normal
-- Init.Data.UInt.Lemmas
UInt16.toNat_toUInt8 : ∀ (x : UInt16), x.toUInt8.toNat = x.toNat % 2 ^ 8
-- Mathlib.NumberTheory.NumberField.House
NumberField.house_sum_le_sum_house : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {ι : Type u_2} (s : Finset ι) (α : ι → K),
  NumberField.house (∑ i ∈ s, α i) ≤ ∑ i ∈ s, NumberField.house (α i)
-- Batteries.Data.Vector.Basic
/-- Fold an effectful function `f` over the array from the right, returning the list of partial results.
 -/
Vector.scanrM : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → {n : ℕ} → [Monad m] → (α → β → m β) → β → Vector α n → m (Vector β (n + 1))
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.coeff_tensorEquiv_apply : ∀ (R : Type u_1) {M : Type u_2} {N : Type u_3} [inst : CommSemiring R]
  (x : TensorProduct R (AddMonoidAlgebra R M) (AddMonoidAlgebra R N)),
  ((AddMonoidAlgebra.tensorEquiv R) x).coeff =
    (finsuppTensorFinsupp' R M N)
      ((TensorProduct.congr (AddMonoidAlgebra.coeffLinearEquiv R) (AddMonoidAlgebra.coeffLinearEquiv R)) x)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.all_char_iff : ∀ {c : Char} {s : String.Slice}, s.all c = true ↔ s.copy.toList = List.replicate s.copy.toList.length c
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.any_eq_false_iff_forall_mem_getElem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  {p : α → β → Bool}, m.WF → (m.any p = false ↔ ∀ (a : α) (h : a ∈ m), p a m[a] = false)
-- Mathlib.Topology.Defs.Filter
LocallyCompactSpace.mk : ∀ {X : Type u_3} [inst : TopologicalSpace X],
  (∀ (x : X), ∀ n ∈ nhds x, ∃ s ∈ nhds x, s ⊆ n ∧ IsCompact s) → LocallyCompactSpace X
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instCoeHead.eq_1 : ∀ {α : Type u} [inst : AddMonoid α], AddUnits.instCoeHead = { coe := AddUnits.val }
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.wfImp_insertMany : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w}
  [inst_4 : ForIn Id ρ (α × β)] {m : Std.DHashMap.Internal.Raw₀ α fun x => β} {l : ρ},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    Std.DHashMap.Internal.Raw.WFImp ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq_const : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [hE : CompleteSpace E] [MeasureTheory.IsProbabilityMeasure μ] {f : α → E} {c : E},
  (∀ᵐ (x : α) ∂μ, f x = c) → ∫ (x : α), f x ∂μ = c
-- Mathlib.Order.Irreducible
SupPrime.eq_1 : ∀ {α : Type u_2} [inst : SemilatticeSup α] (a : α), SupPrime a = (¬IsMin a ∧ ∀ ⦃b c : α⦄, a ≤ b ⊔ c → a ≤ b ∨ a ≤ c)
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
/-- The covariant involution of the category of simplicial objects
that is induced by the involution
`SimplexCategory.rev : SimplexCategory ⥤ SimplexCategory`.
This functor is purposely not made `implicit_reducible` so as to avoid
confusion between `(opFunctor.obj X) _⦋n⦌` and `X _⦋n⦌`: use the
isomorphism `opObjIso`.  -/
SimplicialObject.opFunctor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    CategoryTheory.Functor (CategoryTheory.SimplicialObject C) (CategoryTheory.SimplicialObject C)
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.congr_left : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {g : α → F} {l : Filter α}
  {f₁ f₂ : α → E}, f₁ =o[l] g → (∀ (x : α), f₁ x = f₂ x) → f₂ =o[l] g
-- Mathlib.Algebra.Order.UpperLower
IsLowerSet.neg : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {s : Set α},
  IsLowerSet s → IsUpperSet (-s)
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instIsStableUnderShiftBot : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A], ⊥.IsStableUnderShift A
-- Init.Data.Bool
Bool.le_antisymm : ∀ {x y : Bool}, x ≤ y → y ≤ x → x = y
-- Mathlib.RingTheory.MvPowerSeries.Equiv
_private.Mathlib.RingTheory.MvPowerSeries.Equiv.0.MvPowerSeries.isNoetherianRing_fin : ∀ (S : Type u_3) [inst : CommRing S] [IsNoetherianRing S] (n : ℕ), IsNoetherianRing (MvPowerSeries (Fin n) S)
-- Mathlib.MeasureTheory.Function.AEEqOfIntegral
MeasureTheory.AEFinStronglyMeasurable.ae_eq_of_forall_setIntegral_eq : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f g : α → E},
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn f s μ) →
    (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → MeasureTheory.IntegrableOn g s μ) →
      (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = ∫ (x : α) in s, g x ∂μ) →
        MeasureTheory.AEFinStronglyMeasurable f μ → MeasureTheory.AEFinStronglyMeasurable g μ → f =ᵐ[μ] g
-- Mathlib.Algebra.Order.Monoid.Defs
one_lt_mul_self_iff : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, 1 < a * a ↔ 1 < a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.not_mem_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t.isEmpty = true → a ∉ t
-- Mathlib.Algebra.Group.Defs
CancelMonoid.toLeftCancelMonoid : {M : Type u} → [self : CancelMonoid M] → LeftCancelMonoid M
-- Std.Do.SPred.Notation.Basic
/-- An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
 -/
Std.Do.«termSpred(_)» : Lean.ParserDescr
-- Init.Data.String.Basic
/-- Given a position in `s.slice! p₀ p₁`, obtain the corresponding position in `s`, or panic if
taking `s.slice! p₀ p₁` already panicked.  -/
String.Slice.Pos.ofSlice! : {s : String.Slice} → {p₀ p₁ : s.Pos} → (s.slice! p₀ p₁).Pos → s.Pos
-- Mathlib.Analysis.InnerProductSpace.OfNorm
/-- Predicate for the parallelogram identity to hold in a normed group. This is a scalar-less
version of `InnerProductSpace`. If you have an `InnerProductSpaceable` assumption, you can
locally upgrade that to `InnerProductSpace 𝕜 E` using `casesI nonempty_innerProductSpace 𝕜 E`.
 -/
InnerProductSpaceable : (E : Type u_2) → [NormedAddCommGroup E] → Prop
-- Mathlib.Data.Pi.Interval
Pi.card_Ioo : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : Fintype ι] [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → DecidableEq (α i)]
  [inst_3 : (i : ι) → PartialOrder (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)] (a b : (i : ι) → α i),
  (Finset.Ioo a b).card = ∏ i, (Finset.Icc (a i) (b i)).card - 2
-- Mathlib.Algebra.Order.GroupWithZero.Basic
mul_pos_iff_of_pos_right : ∀ {α : Type u_1} [inst : MulZeroClass α] {a b : α} [inst_1 : Preorder α] [MulPosStrictMono α] [MulPosReflectLT α],
  0 < b → (0 < a * b ↔ 0 < a)
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- The function `log⁺` is zero in the interval [-1,1].  -/
Real.posLog_eq_zero_iff : ∀ (x : ℝ), x.posLog = 0 ↔ |x| ≤ 1
-- Lean.Meta.Sym.SymM
/-- Opaque extension state type used to store type-erased extension values.  -/
Lean.Meta.Sym.SymExtensionStateSpec : (α : Type) × Inhabited α
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.card_boundaries_eq_succ_length : ∀ {n : ℕ} (c : Composition n), c.boundaries.card = c.length + 1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.spanExt_hom_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Y} {g : X ⟶ Z} {f' : X' ⟶ Y'} {g' : X' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iY.hom)
  (wg : CategoryTheory.CategoryStruct.comp iX.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.spanExt iX iY iZ wf wg).hom.app CategoryTheory.Limits.WalkingSpan.left = iY.hom
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_ge' : ∀ {x : ℝ}, 0 ≤ x → (x - 1) * Real.log 2 - Real.log (x + 2) ≤ Chebyshev.psi x
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mk_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y : T} (f : Y ⟶ X), (CategoryTheory.Over.mk f).left = Y