mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.slope_lt_of_hasDerivAt : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y f' : ℝ},
  StrictConcaveOn ℝ S f → x ∈ S → y ∈ S → x < y → HasDerivAt f f' x → slope f x y < f'
-- Mathlib.GroupTheory.Coset.Defs
/-- **Alias** of `QuotientGroup.induction_on`. -/
QuotientGroup.induction_on' : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} {C : α ⧸ s → Prop} (x : α ⧸ s), (∀ (z : α), C ↑z) → C x
-- Mathlib.FieldTheory.SeparableDegree
/-- If a polynomial splits over `E`, then its separable degree is equal to
the number of distinct roots of it over `E`.  -/
Polynomial.natSepDegree_eq_of_splits : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (f : Polynomial F)
  [inst_3 : DecidableEq E], (Polynomial.map (algebraMap F E) f).Splits → f.natSepDegree = (f.aroots E).toFinset.card
-- Mathlib.Topology.Homotopy.HSpaces
unitInterval.qRight_one_right : ∀ (t : ↑unitInterval), unitInterval.qRight (t, 1) = t
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.isoSpec_hom : ∀ (X : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine X], X.isoSpec.hom = X.toSpecΓ
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.Continuous.mul_log : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℝ}, Continuous f → Continuous fun a => f a * Real.log (f a)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.of.injective_of_degree_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [IsDomain R],
  f.degree ≠ 0 → Function.Injective ⇑(AdjoinRoot.of f)
-- Mathlib.RingTheory.PicardGroup
Module.Invertible.bijective_of_surjective : ∀ {R : Type u} {M : Type v} {N : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N] [Module.Invertible R M] [Module.Invertible R N] {f : M →ₗ[R] N},
  Function.Surjective ⇑f → Function.Bijective ⇑f
-- Aesop.Tree.ExtractScript
Aesop.ExtractScriptM.State.proofHasMVar : Aesop.ExtractScriptM.State → Bool
-- Mathlib.RingTheory.Derivation.DifferentialRing
algebraMap.coe_deriv : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : Differential A] [inst_4 : Differential B] [DifferentialAlgebra A B] (a : A), ↑a′ = (↑a)′
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObj.mul_add : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (R : C) [self : CategoryTheory.RingObj R],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R CategoryTheory.AddMonObj.add)
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.SemiCartesianMonoidalCategory.fst R R))
          CategoryTheory.MonObj.mul)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft R (CategoryTheory.SemiCartesianMonoidalCategory.snd R R))
          CategoryTheory.MonObj.mul))
      CategoryTheory.AddMonObj.add
-- Mathlib.Data.Fin.Basic
Fin.castLE_natCast : ∀ {m n : ℕ} [inst : NeZero m] (h : m ≤ n) (a : ℕ), Fin.castLE h ↑a = ↑(a % m)
-- Mathlib.Data.List.Shortlex
List.not_shortlex_nil_right : ∀ {α : Type u_1} {r : α → α → Prop} {s : List α}, ¬List.Shortlex r s []
-- Mathlib.Algebra.BigOperators.Expect
Fintype.expect_dite_eq : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : AddCommMonoid M] [inst_2 : Module ℚ≥0 M]
  [inst_3 : DecidableEq ι] (i : ι) (f : (j : ι) → i = j → M),
  (Finset.univ.expect fun j => if h : i = j then f j h else 0) = (↑(Fintype.card ι))⁻¹ • f i ⋯
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The **Banach-Alaoglu theorem**: the polar set of a neighborhood `s` of the origin in a
normed space `E` is a compact subset of `WeakDual 𝕜 E`.  -/
WeakDual.isCompact_polar : ∀ (𝕜 : Type u_1) {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [ProperSpace 𝕜] {s : Set E}, s ∈ nhds 0 → IsCompact (WeakDual.polar 𝕜 s)
-- Init.Data.Array.Lemmas
Array.append_eq_map_iff : ∀ {α : Type u_1} {β : Type u_2} {xs ys : Array β} {zs : Array α} {f : α → β},
  xs ++ ys = Array.map f zs ↔ ∃ as bs, zs = as ++ bs ∧ Array.map f as = xs ∧ Array.map f bs = ys
-- Aesop.Script.UScriptToSScript
Aesop.Script.StepTree.node.injEq : ∀ (step : Aesop.Script.Step) (index : ℕ) (children : Array Aesop.Script.StepTree) (step_1 : Aesop.Script.Step)
  (index_1 : ℕ) (children_1 : Array Aesop.Script.StepTree),
  (Aesop.Script.StepTree.node step index children = Aesop.Script.StepTree.node step_1 index_1 children_1) =
    (step = step_1 ∧ index = index_1 ∧ children = children_1)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasKernel f]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.Limits.HasKernel (G.map f)
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
Measurable.cosh : ∀ {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ}, Measurable f → Measurable fun x => Real.cosh (f x)
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_vecMul_kronecker : ∀ {l : Type u_2} {m : Type u_1} {n : Type u_4} {p : Type u_5} {R : Type u_3} [inst : NonUnitalCommSemiring R]
  [inst_1 : Fintype m] [inst_2 : Fintype n] (A : Matrix m l R) (X : Matrix m n R) (B : Matrix n p R),
  Matrix.vecMul X.vec (Matrix.kroneckerMap (fun x1 x2 => x1 * x2) B A) = (A.transpose * X * B).vec
-- Std.Sync.CancellationContext
/-- Checks if the context is cancelled.
 -/
Std.CancellationContext.isCancelled : Std.CancellationContext → BaseIO Bool
-- Init.PropLemmas
exists_eq_or_imp' : ∀ {α : Sort u_1} {p q : α → Prop} {a' : α}, (∃ a, (a' = a ∨ q a) ∧ p a) ↔ p a' ∨ ∃ a, q a ∧ p a
-- Mathlib.Order.GaloisConnection.Basic
GaloisCoinsertion.liftOrderBot.eq_1 : ∀ {α : Type u} {β : Type v} {l : α → β} {u : β → α} [inst : PartialOrder β] [inst_1 : Preorder α] [inst_2 : OrderBot α]
  (gi : GaloisCoinsertion u l), gi.liftOrderBot = { bot := gi.choice ⊥ ⋯, bot_le := ⋯ }
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.instBEqExtraTheorem.beq : Lean.Elab.Tactic.Grind.ExtraTheorem → Lean.Elab.Tactic.Grind.ExtraTheorem → Bool
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCodetector_unop_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (G : Cᵒᵖ),
  CategoryTheory.IsCodetector (Opposite.unop G) ↔ CategoryTheory.IsDetector G
-- Mathlib.Topology.Sheaves.SheafOfFunctions
/-- We show that the presheaf of functions to a type `T`
(no continuity assumptions, just plain functions)
form a sheaf.

In fact, the proof is identical when we do this for dependent functions to a type family `T`,
so we do the more general case.
 -/
TopCat.Presheaf.toTypes_isSheaf : ∀ (X : TopCat) (T : ↑X → Type u_1), (X.presheafToTypes T).IsSheaf
-- Mathlib.Analysis.SpecialFunctions.Complex.Log
Complex.two_pi_I_ne_zero : 2 * ↑Real.pi * Complex.I ≠ 0
-- Mathlib.MeasureTheory.Function.SimpleFuncDense
MeasureTheory.SimpleFunc.edist_approxOn_le : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : PseudoEMetricSpace α]
  [inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] {f : β → α} (hf : Measurable f) {s : Set α} {y₀ : α}
  (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s] (x : β) (n : ℕ),
  edist ((MeasureTheory.SimpleFunc.approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x)
-- Std.Http.Server.Handler
/-- Builds a `StatelessHandler` from all three callback functions.
 -/
Std.Http.Server.Handler.ofFns : (Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any)) →
  (optParam (IO.Error → Std.Async.Async Unit) fun x => pure ()) →
    (optParam (Std.Http.Request.Head → Std.Async.Async Bool) fun x => pure true) → Std.Http.Server.StatelessHandler
-- Mathlib.Combinatorics.Matroid.Basic
/-- Any two sets `B₁`, `B₂` in a family with the exchange property have the same
`ℕ∞`-cardinality.  -/
Matroid.ExchangeProperty.encard_isBase_eq : ∀ {α : Type u_1} {IsBase : Set α → Prop} {B₁ B₂ : Set α},
  Matroid.ExchangeProperty IsBase → IsBase B₁ → IsBase B₂ → B₁.encard = B₂.encard
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.image_linearMap : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} {Y : Type u_3} [inst_2 : Fintype X]
  [inst_3 : Fintype Y] [IsOrderedRing S] (f : X → Y), ⇑(FunOnFinite.linearMap S S f) '' stdSimplex S X ⊆ stdSimplex S Y
-- Mathlib.Data.Set.Card
Set.encard_le_one_iff : ∀ {α : Type u_1} {s : Set α}, s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
-- Mathlib.Data.Real.Basic
Real.lt_cauchy : ∀ {f g : CauSeq ℚ abs}, { cauchy := ⟦f⟧ } < { cauchy := ⟦g⟧ } ↔ f < g
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonSemanticTokensParams : Lean.FromJson Lean.Lsp.SemanticTokensParams
-- Mathlib.Order.Disjoint
Codisjoint.of_codisjoint_sup_of_le' : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderTop α] {a b c : α},
  Codisjoint (a ⊔ b) c → c ≤ b → Codisjoint a b
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.restrictScalars_one : ∀ (R : Type u) (A : Type w) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A), Submodule.restrictScalars R 1 = Subalgebra.toSubmodule S
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.zip_lt_size_of_lt_aig_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len x : ℕ} (aig : Std.Sat.AIG α)
  (input : aig.BinaryRefVec len) (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func]
  [inst_3 : Std.Sat.AIG.RefVec.LawfulZipOperator α func],
  x < aig.decls.size → x < (Std.Sat.AIG.RefVec.zip aig input func).aig.decls.size
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.laverage_zero : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α), ⨍⁻ (_x : α), 0 ∂μ = 0
-- Mathlib.Analysis.InnerProductSpace.SingularValues
/-- 7.68(b) from [axler2024]. See also `LinearMap.support_singularValues` for a stronger statement.
 -/
LinearMap.card_support_singularValues : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F), T.singularValues.support.card = Module.finrank 𝕜 ↥T.range
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.mk : {𝕜 : Type u_4} →
  {E : Type u_5} →
    [inst : RCLike 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [toNormedSpace : NormedSpace 𝕜 E] →
          [toInner : Inner 𝕜 E] →
            (∀ (x : E), ‖x‖ ^ 2 = RCLike.re (inner 𝕜 x x)) →
              (∀ (x y : E), (starRingEnd 𝕜) (inner 𝕜 y x) = inner 𝕜 x y) →
                (∀ (x y z : E), inner 𝕜 (x + y) z = inner 𝕜 x z + inner 𝕜 y z) →
                  (∀ (x y : E) (r : 𝕜), inner 𝕜 (r • x) y = (starRingEnd 𝕜) r * inner 𝕜 x y) → InnerProductSpace 𝕜 E
-- Init.Prelude
/-- `Inhabited α` is a typeclass that says that `α` has a designated element,
called `(default : α)`. This is sometimes referred to as a "pointed type".

This class is used by functions that need to return a value of the type
when called "out of domain". For example, `Array.get! arr i : α` returns
a value of type `α` when `arr : Array α`, but if `i` is not in range of
the array, it reports a panic message, but this does not halt the program,
so it must still return a value of type `α` (and in fact this is required
for logical consistency), so in this case it returns `default`.
 -/
Inhabited : Sort u → Sort (max 1 u)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.proj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (S : CategoryTheory.Functor C D) (T : D) {X Y : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)}
  (f : X ⟶ Y), (CategoryTheory.CostructuredArrow.proj S T).map f = f.left
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Variant where the image of `g` is a `SkewMonoidAlgebra`.  -/
SkewMonoidAlgebra.coeff_sum' : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [inst_1 : AddCommMonoid k']
  (f : SkewMonoidAlgebra k G) (g : G → k → SkewMonoidAlgebra k' G'),
  (f.sum g).coeff = f.coeff.sum fun x1 x2 => (g x1 x2).coeff
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.reorder : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey_erase_le_maxKey : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {he : (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false},
  (compare ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.maxKey he) (t.maxKey ⋯)).isLE = true
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.op_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h : S.RightHomologyData), h.op.f' = h.g'.op
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasFDerivWithinAt.comp_hasDerivAt_of_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type w} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f : 𝕜 → F}
  {f' : F} (x : 𝕜) {l : F → E} {l' : F →L[𝕜] E} {y : F} {t : Set F},
  HasFDerivWithinAt l l' t y →
    HasDerivAt f f' x → (∀ᶠ (x' : 𝕜) in nhds x, f x' ∈ t) → y = f x → HasDerivAt (l ∘ f) (l' f') x
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.Pos.skip?_prop_eq_none_iff : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice} {pos : s.Pos},
  pos.skip? P = none ↔ ∀ (h : pos ≠ s.endPos), ¬P (pos.get h)
-- Mathlib.Analysis.Normed.Group.Constructions
norm_ofMul : ∀ {E : Type u_2} [inst : Norm E] (x : E), ‖Additive.ofMul x‖ = ‖x‖
-- Mathlib.Algebra.Group.Submonoid.Saturation
SaturatedSubmonoid.ext : ∀ {M : Type u_1} [inst : MulOneClass M] {s₁ s₂ : SaturatedSubmonoid M}, s₁.toSubmonoid = s₂.toSubmonoid → s₁ = s₂
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, k ∈ m.insert k v
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.ext : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} {x y : SSet.relativeCellComplexOfMono.Cell i d}, x.simplex = y.simplex → x = y
-- Mathlib.Topology.UniformSpace.Completion
_private.Mathlib.Topology.UniformSpace.Completion.0.CauchyFilter.comp_gen : ∀ {α : Type u} [inst : UniformSpace α],
  (((uniformity α).lift' CauchyFilter.gen).lift' fun s => SetRel.comp s s) ≤ (uniformity α).lift' CauchyFilter.gen
-- Mathlib.MeasureTheory.Integral.Bochner.FundThmCalculus
/-- Fundamental theorem of calculus for set integrals, `nhdsWithin` version: if `μ` is a locally
finite measure and `f` is an almost everywhere measurable function that is continuous at a point `a`
within a measurable set `t`, then `∫ x in s i, f x ∂μ = μ (s i) • f a + o(μ (s i))` at a filter `li`
provided that `s i` tends to `(𝓝[t] a).smallSets` along `li`.  Since `μ (s i)` is an `ℝ≥0∞`
number, we use `μ.real (s i)` in the actual statement.

Often there is a good formula for `μ.real (s i)`, so the formalization can take an optional
argument `m` with this formula and a proof of `(fun i => μ.real (s i)) =ᶠ[li] m`. Without these
arguments, `m i = μ.real (s i)` is used in the output.  -/
ContinuousWithinAt.integral_sub_linear_isLittleO_ae : ∀ {X : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : MeasurableSpace X] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [CompleteSpace E] [inst_4 : TopologicalSpace X] [OpensMeasurableSpace X]
  {μ : MeasureTheory.Measure X} [MeasureTheory.IsLocallyFiniteMeasure μ] {x : X} {t : Set X} {f : X → E},
  ContinuousWithinAt f t x →
    MeasurableSet t →
      StronglyMeasurableAtFilter f (nhdsWithin x t) μ →
        ∀ {s : ι → Set X} {li : Filter ι},
          Filter.Tendsto s li (nhdsWithin x t).smallSets →
            ∀ (m : optParam (ι → ℝ) fun i => μ.real (s i)),
              autoParam ((fun i => μ.real (s i)) =ᶠ[li] m) ContinuousWithinAt.integral_sub_linear_isLittleO_ae._auto_1 →
                (fun i => ∫ (x : X) in s i, f x ∂μ - m i • f x) =o[li] m
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.card_vonNeumann : ∀ (o : Ordinal.{u}), (ZFSet.vonNeumann o).card = Cardinal.preBeth o
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_fun_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.MemLp X 2 μ →
    MeasureTheory.MemLp Y 2 μ →
      ProbabilityTheory.variance (fun ω => X ω - Y ω) μ =
        ProbabilityTheory.variance X μ - 2 * ProbabilityTheory.covariance X Y μ + ProbabilityTheory.variance Y μ
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.coe_toWeakDualBCNN : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  (μ : MeasureTheory.FiniteMeasure Ω), ⇑μ.toWeakDualBCNN = μ.testAgainstNN
-- Mathlib.Analysis.Normed.Group.AddCircle
UnitAddCircle.norm_eq : ∀ {x : ℝ}, ‖↑x‖ = |x - ↑(round x)|
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.free_map_coe : ∀ {α β : Type u} {f : α ⟶ β},
  ⇑(CategoryTheory.ConcreteCategory.hom (CommRingCat.free.map f)) =
    ⇑(MvPolynomial.rename ⇑(CategoryTheory.ConcreteCategory.hom f))
-- Init.Data.List.ToArray
Array.setIfInBounds.eq_1 : ∀ {α : Type u_1} (xs : Array α) (i : ℕ) (v : α), xs.setIfInBounds i v = if h : i < xs.size then xs.set i v h else xs
-- Mathlib.Analysis.Complex.Trigonometric
Complex.exp_ofReal_mul_I_im : ∀ (x : ℝ), (Complex.exp (↑x * Complex.I)).im = Real.sin x
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.mem_jacobson_iff : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} {x : R}, x ∈ I.jacobson ↔ ∀ (y : R), ∃ z, z * y * x + z - 1 ∈ I
-- Init.Data.Order.Lemmas
Std.not_le_of_gt : ∀ {α : Type u} [inst : LT α] [inst_1 : LE α] [Std.LawfulOrderLT α] {a b : α}, a < b → ¬b ≤ a
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.bot : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] (𝒜 : ι → σ) [inst_5 : GradedRing 𝒜], Ideal.IsHomogeneous 𝒜 ⊥
-- Mathlib.Analysis.Convex.Intrinsic
affineSpan_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),
  affineSpan 𝕜 (intrinsicClosure 𝕜 s) = affineSpan 𝕜 s
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.eLpNorm'_eq : ∀ {α : Type u_1} {F : Type u_5} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup F] {p : ℝ}
  (f : MeasureTheory.SimpleFunc α F) (μ : MeasureTheory.Measure α),
  MeasureTheory.eLpNorm' (⇑f) p μ = (∑ y ∈ f.range, ‖y‖ₑ ^ p * μ (⇑f ⁻¹' {y})) ^ (1 / p)
-- Mathlib.Algebra.Group.Units.Hom
IsUnit.coe_liftRight : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) (hf : ∀ (x : M), IsUnit (f x))
  (x : M), ↑((IsUnit.liftRight f hf) x) = f x
-- Mathlib.Algebra.Group.Hom.Defs
/-- `AddHomClass F M N` states that `F` is a type of addition-preserving homomorphisms.
You should declare an instance of this typeclass when you extend `AddHom`.
 -/
AddHomClass : (F : Type u_10) → (M : outParam (Type u_11)) → (N : outParam (Type u_12)) → [Add M] → [Add N] → [FunLike F M N] → Prop
-- Mathlib.RingTheory.Localization.LocalizationLocalization
/-- Given submonoids `M ≤ N` of `R`, this is the canonical algebra structure
of `M⁻¹S` acting on `N⁻¹S`.  -/
IsLocalization.localizationAlgebraOfSubmonoidLe : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Type u_2) →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          (T : Type u_3) →
            [inst_3 : CommSemiring T] →
              [inst_4 : Algebra R T] →
                (M N : Submonoid R) → M ≤ N → [IsLocalization M S] → [IsLocalization N T] → Algebra S T
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.equiv.symm : ∀ {X Y : AlgebraicGeometry.Scheme} {f g : X.PartialMap Y}, f.equiv g → g.equiv f
-- Mathlib.Analysis.Analytic.CPolynomial
CPolynomialAt.neg : ∀ {𝕜 : 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] {f : E → F} {x : E},
  CPolynomialAt 𝕜 f x → CPolynomialAt 𝕜 (-f) x
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.leadingCoeff g ∈ nonZeroDivisors R → m.leadingCoeff (f * g) = m.leadingCoeff f * m.leadingCoeff g
-- Mathlib.FieldTheory.IsAlgClosed.Spectrum
/-- A specialization of `spectrum.map_polynomial_aeval_of_nonempty` to monic monomials for
convenience.  -/
spectrum.map_pow_of_nonempty : ∀ {𝕜 : Type u} {A : Type v} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] [IsAlgClosed 𝕜] {a : A},
  (spectrum 𝕜 a).Nonempty → ∀ (n : ℕ), spectrum 𝕜 (a ^ n) = (fun x => x ^ n) '' spectrum 𝕜 a
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union_null_iff : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s₁ s₂ : Set α},
  autoParam (μ s₁ ≠ ⊤) MeasureTheory.measureReal_union_null_iff._auto_1 →
    autoParam (μ s₂ ≠ ⊤) MeasureTheory.measureReal_union_null_iff._auto_3 →
      (μ.real (s₁ ∪ s₂) = 0 ↔ μ.real s₁ = 0 ∧ μ.real s₂ = 0)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.unop_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.HomologyData), h.unop.iso = h.iso.unop
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.map.match_1.splitter : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    (motive : (X Y : CategoryTheory.WithTerminal C) → (X ⟶ Y) → Sort u_3) →
      (X Y : CategoryTheory.WithTerminal C) →
        (f : X ⟶ Y) →
          ((a a_1 : C) →
              (f : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.of a_1) →
                motive (CategoryTheory.WithTerminal.of a) (CategoryTheory.WithTerminal.of a_1) f) →
            ((a : C) →
                (x : CategoryTheory.WithTerminal.of a ⟶ CategoryTheory.WithTerminal.star) →
                  motive (CategoryTheory.WithTerminal.of a) CategoryTheory.WithTerminal.star x) →
              ((x : CategoryTheory.WithTerminal.star ⟶ CategoryTheory.WithTerminal.star) →
                  motive CategoryTheory.WithTerminal.star CategoryTheory.WithTerminal.star x) →
                motive X Y f
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.unzeroD.eq_1 : ∀ {α : Type u} (d : α) (x : WithZero α), WithZero.unzeroD d x = WithZero.recZeroCoe d id x