mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftEquiv_comp_apply : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing K] [inst_1 : CommRing L]
  [inst_2 : CommRing M] [inst_3 : CommRing N] (i : K →+* L) (j : K →+* M) (g : L →+* N) (p : ℕ) [inst_4 : ExpChar M p]
  [inst_5 : ExpChar K p] [inst_6 : PerfectRing M p] [inst_7 : IsPRadical i p] [inst_8 : ExpChar L p]
  [inst_9 : ExpChar N p] [inst_10 : IsPRadical g p] [inst_11 : IsPRadical (g.comp i) p],
  (PerfectRing.liftEquiv M g p) ((PerfectRing.liftEquiv M i p) j) = (PerfectRing.liftEquiv M (g.comp i) p) j
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sumInr_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  (F : CategoryTheory.PreZeroHypercover S) (val : F.I₀), (E.sumInr F).s₀ val = Sum.inr val
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The bottom-left `d × l` part of a `(u+d) × (l+r)` matrix.  -/
Matrix.subDownLeft : {α : Type v} → {d u l r : ℕ} → Matrix (Fin (u + d)) (Fin (l + r)) α → Matrix (Fin d) (Fin l) α
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
IsPrimitiveRoot.subOnePowerBasis_gen : ∀ {n : ℕ} [inst : NeZero n] (K : Type u) {L : Type v} [inst_1 : Field K] [inst_2 : CommRing L] [inst_3 : IsDomain L]
  [inst_4 : Algebra K L] [inst_5 : IsCyclotomicExtension {n} K L] {ζ : L} (hζ : IsPrimitiveRoot ζ n),
  (IsPrimitiveRoot.subOnePowerBasis K hζ).gen = ζ - 1
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Reified `rhs`  -/
Lean.Meta.Grind.Arith.CommRing.DiseqCnstr.rrhs : Lean.Meta.Grind.Arith.CommRing.DiseqCnstr → Lean.Meta.Grind.Arith.CommRing.RingExpr
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
AlgebraicIndependent.eq_1 : ∀ {ι : Type u_1} (R : Type u_3) {A : Type u_5} (x : ι → A) [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A], AlgebraicIndependent R x = Function.Injective ⇑(MvPolynomial.aeval x)
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_congr : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {S : Type u_3}
  [inst_3 : Semiring S] [inst_4 : LinearOrder S] [inst_5 : FloorSemiring S] {b : S},
  (∀ (n : ℕ), a ≤ ↑n ↔ b ≤ ↑n) → ⌈a⌉₊ = ⌈b⌉₊
-- Init.Data.List.Basic
List.elem.eq_def : ∀ {α : Type u} [inst : BEq α] (a : α) (x : List α),
  List.elem a x =
    match x with
    | [] => false
    | b :: bs =>
      match a == b with
      | true => true
      | false => List.elem a bs
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_natAdd_Ioo : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (Fin.natAdd m) (Finset.Ioo i j) = Finset.Ioo (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.RingTheory.Binomial
Ring.choose_eq_smul : ∀ {R : Type u_1} [inst : Field R] [inst_1 : CharZero R] {a : R} {n : ℕ},
  Ring.choose a n = (↑n.factorial)⁻¹ • (descPochhammer ℤ n).smeval a
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
extDerivWithin_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (ω : E → E [⋀^Fin n]→L[𝕜] F), extDerivWithin ω Set.univ = extDeriv ω
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_ssubset_coe : ∀ {α : Type u_1} [inst : LE α] {s t : LowerSet α}, ↑s ⊂ ↑t ↔ s < t
-- Std.Sync.RecursiveMutex
/-- Locks a `BaseRecursiveMutex`. Waits until no other thread has locked the mutex.
If the current thread already holds the mutex this function doesn't block.
 -/
Std.BaseRecursiveMutex.lock : Std.BaseRecursiveMutex → BaseIO Unit
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.mk.inj : ∀ {β : Type u_1} {α : Type u_2} {toBallPackage : Besicovitch.BallPackage β α} {τ : ℝ} {one_lt_tau : 1 < τ}
  {toBallPackage_1 : Besicovitch.BallPackage β α} {τ_1 : ℝ} {one_lt_tau_1 : 1 < τ_1},
  { toBallPackage := toBallPackage, τ := τ, one_lt_tau := one_lt_tau } =
      { toBallPackage := toBallPackage_1, τ := τ_1, one_lt_tau := one_lt_tau_1 } →
    toBallPackage = toBallPackage_1 ∧ τ = τ_1
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.WalkingMultispan.instSubsingletonHomRight : ∀ {J : CategoryTheory.Limits.MultispanShape} (a b : J.R),
  Subsingleton (CategoryTheory.Limits.WalkingMultispan.right a ⟶ CategoryTheory.Limits.WalkingMultispan.right b)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
/-- This term gives an alternative infinite sum for G2 which is absolutely convergent.  -/
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform.0.EisensteinSeries.G2Term : UpperHalfPlane → (Fin 2 → ℤ) → ℂ
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_iSup_le : ∀ {ι : Type u_1} {f : ι → Ordinal.{u_1}}, (∀ (i : ι), f i < iSup f) → (iSup f).cof ≤ Cardinal.mk ι
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.map_epi : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [CategoryTheory.Epi f] [CategoryTheory.Epi g]
  [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct W X] [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct Y Z],
  CategoryTheory.Epi (CategoryTheory.Limits.biprod.map f g)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_inter : ∀ {V : Type u} (s t : Set (Sym2 V)),
  SimpleGraph.fromEdgeSet (s ∩ t) = SimpleGraph.fromEdgeSet s ⊓ SimpleGraph.fromEdgeSet t
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousSub.mk : ∀ {G : Type u_4} [inst : TopologicalSpace G] [inst_1 : Sub G], (Continuous fun p => p.1 - p.2) → ContinuousSub G
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}}
  (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
  (⇑(Profinite.NobelingProof.Linear_CC' C hsC ho) ∘ fun l => Profinite.NobelingProof.Products.eval C ↑l) = fun l =>
    Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) (↑l).Tail
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.comap_iInf_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F},
  Function.Injective ⇑f → ∀ (S : ι → Submonoid M), Submonoid.comap f (⨅ i, Submonoid.map f (S i)) = iInf S
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierInv_zero : ∀ {E : Type u_3} {F : Type u_4} [inst : AddCommGroup E] [inst_1 : AddCommGroup F] [inst_2 : FourierTransformInv E F]
  [FourierInvAdd E F], FourierTransformInv.fourierInv 0 = 0
-- Lean.Expr
/-- Return `true` if the given expression is a forall-expression aka (dependent) arrow.  -/
Lean.Expr.isForall : Lean.Expr → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiableWithinAt_const_sub_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E} (c : F), DifferentiableWithinAt 𝕜 (fun y => c - f y) s x ↔ DifferentiableWithinAt 𝕜 f s x
-- Init.Data.Dyadic.Basic
Dyadic.instHShiftRightNat : HShiftRight Dyadic ℕ Dyadic
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_roo_eq_some : ∀ {m n : ℤ} {i : ℕ}, i < (n - (m + 1)).toNat → (m<...n).toArray[i]? = some (m + 1 + ↑i)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Icc_iff_integrableOn_Ioc : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α} [MeasureTheory.NullSingletonClass μ],
  autoParam (‖f a‖ₑ ≠ ⊤) integrableOn_Icc_iff_integrableOn_Ioc._auto_1 →
    (MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ)
-- Mathlib.Order.Preorder.Chain
Flag.bot_mem : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderBot α] (s : Flag α), ⊥ ∈ s
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.tacticStatesEqualUpToIdsCore : Array Lean.MVarId → Array Lean.MVarId → Aesop.EqualUpToIdsM Bool
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasLimit.isoOfNatIso_inv_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasLimit F]
  [inst_3 : CategoryTheory.Limits.HasLimit G] (w : F ≅ G) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasLimit.isoOfNatIso w).inv
      (CategoryTheory.Limits.limit.π F j) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π G j) (w.inv.app j)
-- Std.Http.Data.URI.Basic
Std.Http.URI.mk.inj : ∀ {scheme : Std.Http.URI.Scheme} {authority : Option Std.Http.URI.Authority} {path : Std.Http.URI.Path}
  {query : Std.Http.URI.Query} {fragment : Option String} {scheme_1 : Std.Http.URI.Scheme}
  {authority_1 : Option Std.Http.URI.Authority} {path_1 : Std.Http.URI.Path} {query_1 : Std.Http.URI.Query}
  {fragment_1 : Option String},
  { scheme := scheme, authority := authority, path := path, query := query, fragment := fragment } =
      { scheme := scheme_1, authority := authority_1, path := path_1, query := query_1, fragment := fragment_1 } →
    scheme = scheme_1 ∧ authority = authority_1 ∧ path = path_1 ∧ query = query_1 ∧ fragment = fragment_1
-- Init.Data.Int.Compare
Int.compare_eq_ite_le : ∀ (a b : ℤ), compare a b = if a ≤ b then if b ≤ a then Ordering.eq else Ordering.lt else Ordering.gt
-- Mathlib.Algebra.FreeAbelianGroup.UniqueSums
instTwoUniqueSumsFreeAbelianGroup : ∀ {σ : Type u_1}, TwoUniqueSums (FreeAbelianGroup σ)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.retract_i_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.Idempotents.Karoubi C),
  X.retract.i.f = X.p
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj.congr_simp : ∀ (J : Type u_2) [inst : Countable J] [inst_1 : Preorder J] [inst_2 : CategoryTheory.IsFiltered J] (a a_1 : ℕ),
  a = a_1 →
    CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj J a =
      CategoryTheory.Limits.IsFiltered.sequentialFunctor_obj J a_1
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.abs_moebius_eq_one_of_squarefree : ∀ {l : ℕ}, Squarefree l → |ArithmeticFunction.moebius l| = 1
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Scalar multiplication by the scalar `0` is `0`.  -/
MulActionWithZero.zero_smul : ∀ {M₀ : Type u_2} {A : Type u_7} {inst : MonoidWithZero M₀} {inst_1 : Zero A} [self : MulActionWithZero M₀ A] (m : A),
  0 • m = 0
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_subtype_val : ∀ {α : Type ua} {p : α → Prop} [inst : UniformSpace α], UniformContinuous Subtype.val
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.CliqueFreeOn.anti : ∀ {α : Type u_1} (G H : SimpleGraph α) {s : Set α} {n : ℕ}, G ≤ H → H.CliqueFreeOn s n → G.CliqueFreeOn s n
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isRefl_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.BilinForm.IsRefl 0
-- Lean.DocString.Parser
/-- Parses as `ifVerso` if the option `doc.verso` is `true`, or as `ifNotVerso` otherwise.
 -/
Lean.Doc.Parser.ifVersoFn : Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.Order.GroupWithZero.Bounds
/-- A variant of `BddAbove.range_comp_left` that assumes that `f` is nonnegative and `g` is monotone
on nonnegative values.  -/
BddAbove.range_comp_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Nonempty α] [inst : Preorder β] [inst_1 : Zero β] [inst_2 : Preorder γ]
  {f : α → β} {g : β → γ},
  BddAbove (Set.range f) → 0 ≤ f → MonotoneOn g {x | 0 ≤ x} → BddAbove (Set.range fun x => g (f x))
-- Std.Data.TreeSet.Basic
/-- Internal implementation detail of the tree map  -/
Std.TreeSet.Equiv.inner : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet α cmp}, m₁.Equiv m₂ → m₁.inner.Equiv m₂.inner
-- Mathlib.Order.Circular
sbtw_irrefl_left : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b : α}, ¬sbtw a a b
-- Lean.Elab.Tactic.RCases
/-- Expand a `rintroPat` into an equivalent list of `rcasesPat` patterns.  -/
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.expandRIntroPat : Lean.TSyntax `rintroPat →
  optParam (Array (Lean.TSyntax `rcasesPat)) #[] → optParam (Option Lean.Term) none → Array (Lean.TSyntax `rcasesPat)
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.map_smulₛₗ₂ : ∀ {R : Type u_1} {R₂ : Type u_2} {S : Type u_3} {S₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : Semiring S] [inst_3 : Semiring S₂] {M : Type u_5} {N : Type u_7} {P : Type u_9} [inst_4 : AddCommMonoid M]
  [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P] [inst_7 : Module R M] [inst_8 : Module S N]
  [inst_9 : Module R₂ P] [inst_10 : Module S₂ P] [inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂}
  (f : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P) (r : R) (x : M) (y : N), (f (r • x)) y = ρ₁₂ r • (f x) y
-- Lean.Meta.Tactic.Simp.Rewrite
Lean.Meta.Simp.postDefault : Lean.Meta.Simp.SimprocsArray → Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Group.Irreducible.Defs
not_addIrreducible_zero : ∀ {M : Type u_1} [inst : AddMonoid M], ¬AddIrreducible 0
-- Mathlib.Algebra.TrivSqZeroExt.Basic
_private.Mathlib.Algebra.TrivSqZeroExt.Basic.0.termTsze : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- The integral of an almost-everywhere strongly measurable function over `AddCircle T` is equal
to the integral over an interval $(t, t + T]$ in `ℝ` of its lift to `ℝ`.  -/
AddCircle.intervalIntegral_preimage : ∀ (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (t : ℝ)
  (f : AddCircle T → E), ∫ (a : ℝ) in t..t + T, f ↑a = ∫ (b : AddCircle T), f b
-- Init.Data.Nat.Lemmas
Nat.pow_lt_pow_of_lt : ∀ {a n m : ℕ}, 1 < a → n < m → a ^ n < a ^ m
-- Mathlib.Data.Int.CardIntervalMod
Nat.Ioc_filter_modEq_cast : ∀ (a b : ℕ) {r v : ℕ},
  Finset.map Nat.castEmbedding ({x ∈ Finset.Ioc a b | x ≡ v [MOD r]}) = {x ∈ Finset.Ioc ↑a ↑b | x ≡ ↑v [ZMOD ↑r]}
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.piCongrRight_symm : ∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} {A₂ : ι → Type u_6} [inst : CommSemiring R]
  [inst_1 : (i : ι) → Semiring (A₁ i)] [inst_2 : (i : ι) → Semiring (A₂ i)] [inst_3 : (i : ι) → Algebra R (A₁ i)]
  [inst_4 : (i : ι) → Algebra R (A₂ i)] (e : (i : ι) → A₁ i ≃ₐ[R] A₂ i),
  (AlgEquiv.piCongrRight e).symm = AlgEquiv.piCongrRight fun i => (e i).symm
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.measurableSet_preimage : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] (f : MeasureTheory.SimpleFunc α β) (s : Set β),
  MeasurableSet (⇑f ⁻¹' s)
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.toReal_klDiv_smul_right_eq_smul_left : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [MeasureTheory.IsFiniteMeasure ν],
  μ.AbsolutelyContinuous ν →
    MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ →
      ∀ (c : NNReal), (InformationTheory.klDiv μ (c • ν)).toReal = ↑c * (InformationTheory.klDiv (c⁻¹ • μ) ν).toReal
-- Mathlib.Algebra.Polynomial.Identities
/-- For any polynomial `f`, `f.eval x - f.eval y` can be expressed as `z * (x - y)`
for some `z` in the ring.
 -/
Polynomial.evalSubFactor : {R : Type u} →
  [inst : CommRing R] →
    (f : Polynomial R) → (x y : R) → { z // Polynomial.eval x f - Polynomial.eval y f = z * (x - y) }
-- Mathlib.Algebra.Order.Star.Basic
/-- characterization of the order in terms of the `StarRing` structure.  -/
StarOrderedRing.le_iff : ∀ {R : Type u_3} {inst : NonUnitalSemiring R} {inst_1 : PartialOrder R} {inst_2 : StarRing R} [self : StarOrderedRing R]
  (x y : R), x ≤ y ↔ ∃ p ∈ AddSubmonoid.closure (Set.range fun s => star s * s), y = x + p
-- Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
Set.natCard_smul_set₀ : ∀ {G₀ : Type u_1} {M₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : Zero M₀] [inst_2 : MulActionWithZero G₀ M₀]
  {a : G₀}, a ≠ 0 → ∀ (s : Set M₀), Nat.card ↑(a • s) = Nat.card ↑s
-- Mathlib.Data.Finset.Empty
Finset.empty_val : ∀ {α : Type u_1}, ∅.val = 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxoIterator.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (iter : Std.DTreeMap.Internal.Zipper α β) (upper : α),
  sizeOf { iter := iter, upper := upper } = 1 + sizeOf iter + sizeOf upper
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.Center.tensorObj_snd_β : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X Y : CategoryTheory.Center C) (U : C),
  (X.tensorObj Y).snd.β U =
    CategoryTheory.MonoidalCategoryStruct.associator X.fst Y.fst U ≪≫
      CategoryTheory.MonoidalCategory.whiskerLeftIso X.fst (Y.snd.β U) ≪≫
        (CategoryTheory.MonoidalCategoryStruct.associator X.fst U Y.fst).symm ≪≫
          CategoryTheory.MonoidalCategory.whiskerRightIso (X.snd.β U) Y.fst ≪≫
            CategoryTheory.MonoidalCategoryStruct.associator U X.fst Y.fst
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
one_le_div' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α}, 1 ≤ a / b ↔ b ≤ a
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.toFun_eq_coe : ∀ {R : Type u_1} [inst : NonUnitalRing R] (p : RingSeminorm R), ⇑p.toAddGroupSeminorm = ⇑p
-- Mathlib.Control.Traversable.Lemmas
Traversable.traverse_map : ∀ {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] {F : Type u → Type u} [inst_2 : Applicative F]
  [LawfulApplicative F] {α β γ : Type u} (f : β → F γ) (g : α → β) (x : t α), traverse f (g <$> x) = traverse (f ∘ g) x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.map_induce_induceHomOfLE : ∀ {V : Type u} {G : SimpleGraph V} {s s' : Set V} (hs : s ⊆ s') {u v : V} (w : G.Walk u v)
  (hw : ∀ x ∈ w.support, x ∈ s),
  SimpleGraph.Walk.map (G.induceHomOfLE hs).toHom (SimpleGraph.Walk.induce s w hw) = SimpleGraph.Walk.induce s' w ⋯
-- Lean.Meta.AbstractMVars
Lean.Meta.AbstractMVars.State : Type
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.IsPositive.adjoint_conj : ∀ {𝕜 : 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 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] {T : E →ₗ[𝕜] E},
  T.IsPositive → ∀ (S : F →ₗ[𝕜] E), (LinearMap.adjoint S ∘ₗ T ∘ₗ S).IsPositive
-- Mathlib.Analysis.Convex.Body
ConvexBody.isClosed : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] [T2Space V]
  (K : ConvexBody V), IsClosed ↑K
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.ext.sizeOf_spec : sizeOf Lean.Meta.Grind.AttrKind.ext = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α}, k ∉ t₁ → (t₁ ∩ t₂).get? k = none
-- Mathlib.Topology.AlexandrovDiscrete
IndiscreteTopology.toAlexandrovDiscrete : ∀ {α : Type u_3} [inst : TopologicalSpace α] [IndiscreteTopology α], AlexandrovDiscrete α
-- Mathlib.FieldTheory.Finiteness
/-- A module over a division ring is Noetherian if and only if it is finitely generated.  -/
IsNoetherian.iff_fg : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  IsNoetherian K V ↔ Module.Finite K V
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.lieSpan_eq : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (K : LieSubalgebra R L),
  LieSubalgebra.lieSpan R L ↑K = K
-- Mathlib.Topology.Sets.Opens
Homeomorph.opensCongr_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  ⇑f.opensCongr = ⇑(TopologicalSpace.Opens.comap ↑f.symm)
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivFunctor_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {e f : C ≌ D} (α : e ⟶ f),
  (CategoryTheory.Equivalence.symmEquivFunctor C D).map α =
    (CategoryTheory.Equivalence.mkHom
        ((CategoryTheory.conjugateEquiv f.toAdjunction e.toAdjunction) (CategoryTheory.Equivalence.asNatTrans α))).op
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_mul_right : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : Group G] [inst_2 : MulSemiringAction G k]
  (f g : SkewMonoidAlgebra k G) (x : G), (f * g).coeff x = g.sum fun a b => f.coeff (x * a⁻¹) * (x * a⁻¹) • b
-- Mathlib.Order.Monotone.Basic
StrictAntiOn.injOn : ∀ {α : Type u} {β : Type v} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  StrictAntiOn f s → Set.InjOn f s
-- Mathlib.Topology.Algebra.UniformMulAction
UniformContinuous.const_vadd : ∀ {M : Type v} {X : Type x} {Y : Type y} [inst : UniformSpace X] [inst_1 : UniformSpace Y] [inst_2 : VAdd M X]
  [UniformContinuousConstVAdd M X] {f : Y → X}, UniformContinuous f → ∀ (c : M), UniformContinuous (c +ᵥ f)
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.IsProper.instRespectsIsoScheme : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsProper
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzWith.dist_lt_mul_of_lt : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β}
  {x y : α} {r : ℝ}, LipschitzWith K f → K ≠ 0 → dist x y < r → dist (f x) (f y) < ↑K * r
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.Φ_one : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.Φ 1 = Polynomial.X
-- Init.Data.Int.Pow
Int.negSucc_pow : ∀ (m n : ℕ), Int.negSucc m ^ n = if n % 2 = 0 then Int.ofNat (m.succ ^ n) else Int.negOfNat (m.succ ^ n)
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.contsAux.eq_3 : ∀ {K : Type u_2} [inst : DivisionRing K] (g : GenContFract K) (n : ℕ),
  g.contsAux n.succ.succ =
    match g.s.get? n with
    | none => g.contsAux (n + 1)
    | some gp => GenContFract.nextConts gp.a gp.b (g.contsAux n) (g.contsAux (n + 1))
-- Mathlib.Condensed.Discrete.Basic
Condensed.underlying_map : ∀ (C : Type w) [inst : CategoryTheory.Category.{u + 1, w} C]
  {X Y : CategoryTheory.Sheaf (CategoryTheory.coherentTopology CompHaus) C} (f : X ⟶ Y),
  (Condensed.underlying C).map f = f.hom.app (Opposite.op (CompHaus.of PUnit.{u + 1}))
-- Mathlib.Analysis.Convex.Segment
segment_inter_eq_endpoint_of_linearIndependent_of_ne : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : CommRing 𝕜] [inst_1 : PartialOrder 𝕜] [IsOrderedRing 𝕜] [IsDomain 𝕜]
  [inst_4 : AddCommGroup E] [inst_5 : Module 𝕜 E] {x y : E},
  LinearIndependent 𝕜 ![x, y] →
    ∀ {s t : 𝕜}, s ≠ t → ∀ (c : E), segment 𝕜 (c + x) (c + t • y) ∩ segment 𝕜 (c + x) (c + s • y) = {c + x}
-- Init.Data.UInt.Bitwise
instLawfulCommIdentityUSizeHOrOfNat : Std.LawfulCommIdentity (fun x1 x2 => x1 ||| x2) 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
max_add_add_le_max_add_max : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LinearOrder α] [AddLeftMono α] [AddRightMono α] {a b c d : α},
  max (a + b) (c + d) ≤ max a c + max b d
-- Mathlib.Control.Fold
Traversable.foldl.ofFreeMonoid_comp_of : ∀ {α β : Type u} (f : α → β → α), ⇑(Monoid.Foldl.ofFreeMonoid f) ∘ FreeMonoid.of = Monoid.Foldl.mk ∘ flip f
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instHasForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteAddGrpCatAddMonoidHomCarrier : CategoryTheory.HasForget₂ ProfiniteAddGrp.{u_1} AddGrpCat