mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.tensorTensorTensorComm_tmul : ∀ {R : Type uR} {R' : Type u_1} {S : Type uS} {T : Type u_2} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD}
  [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A]
  [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B]
  [inst_9 : Semiring C] [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C]
  [inst_13 : Semiring D] [inst_14 : Algebra R D] [inst_15 : CommSemiring T] [inst_16 : Algebra R T]
  [inst_17 : Algebra T A] [inst_18 : IsScalarTower R T A] [inst_19 : SMulCommClass S T A] [inst_20 : Algebra S T]
  [inst_21 : IsScalarTower S T A] [inst_22 : CommSemiring R'] [inst_23 : Algebra R R'] [inst_24 : Algebra R' T]
  [inst_25 : Algebra R' A] [inst_26 : Algebra R' B] [inst_27 : IsScalarTower R R' A] [inst_28 : SMulCommClass S R' A]
  [inst_29 : SMulCommClass R' S A] [inst_30 : IsScalarTower R' T A] [inst_31 : IsScalarTower R R' B] (m : A) (n : B)
  (p : C) (q : D),
  (Algebra.TensorProduct.tensorTensorTensorComm R R' S T A B C D) (m ⊗ₜ[R'] n ⊗ₜ[S] (p ⊗ₜ[R] q)) =
    m ⊗ₜ[S] p ⊗ₜ[R'] (n ⊗ₜ[R] q)
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Bound.lt.inj : ∀ {n n_1 : ℤ}, Mathlib.Tactic.IntervalCases.Bound.lt n = Mathlib.Tactic.IntervalCases.Bound.lt n_1 → n = n_1
-- Lean.Meta.Constructions.NoConfusion
_private.Lean.Meta.Constructions.NoConfusion.0.Lean.mkNoConfusionEnum.mkNoConfusion : Lean.Name → Lean.MetaM Unit
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.norm_sub_one_sq_eq : ∀ {A : Type u_1} [inst : CStarAlgebra A] {u : A},
  u ∈ unitary A → ∀ {x : ℝ}, IsLeast (Complex.re '' spectrum ℂ u) x → ‖u - 1‖ ^ 2 = 2 * (1 - x)
-- Mathlib.Probability.Process.Adapted
/-- **Alias** of `MeasureTheory.IsStronglyProgressive.finsetSum`. -/
MeasureTheory.IsStronglyProgressive.finset_sum : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} [inst_1 : TopologicalSpace β] [inst_2 : MeasurableSpace ι] {γ : Type u_4} [inst_3 : AddCommMonoid β]
  [ContinuousAdd β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsStronglyProgressive f (U c)) →
    MeasureTheory.IsStronglyProgressive f fun i a => ∑ c ∈ s, U c i a
-- Init.Data.SInt.Bitwise
instAssociativeInt8HAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Lean.Parser.Types
/-- Returns the character position prior to `pos`  -/
Lean.Parser.InputContext.prev : Lean.Parser.InputContext → String.Pos.Raw → String.Pos.Raw
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR.loop.eq_1 : ∀ {α : Type u} (n : ℕ) (f : (i : ℕ) → i < n → α → α) (a : α) (h : 0 ≤ n), Nat.foldTR.loop✝ n f 0 h a = a
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_ofSeq : ∀ {α : Type u} (s : Stream'.Seq α), (↑s).destruct = Computation.pure (Option.map (fun a => (a, ↑s.tail)) s.head)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {cc : CategoryTheory.Limits.CokernelCofork S.f}
  (hcc : CategoryTheory.Limits.IsColimit cc),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π cc) (S.isoOpcyclesOfIsColimit hcc).hom =
    S.pOpcycles
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_insert_le : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).size ≤ t.size + 1
-- Lean.Parser.Basic
/-- Define parser for `$e` (if `anonymous == true`) and `$e:name`.
`kind` is embedded in the antiquotation's kind, and checked at syntax `match` unless `isPseudoKind` is true.
Antiquotations can be escaped as in `$$e`, which produces the syntax tree for `$e`.  -/
Lean.Parser.mkAntiquot : String → Lean.SyntaxNodeKind → optParam Bool true → optParam Bool false → Lean.Parser.Parser
-- Mathlib.Analysis.Normed.Module.WeakDual
NormedSpace.Dual.toWeakDual_continuous : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E], Continuous fun x' => StrongDual.toWeakDual x'
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLTLTGELT a b h).map φ).hom₃ = (t.truncGE a).map ((t.truncLT b).map φ)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.algebraMap_eq : ∀ {R : Type u} [inst : CommSemiring R], algebraMap R (Polynomial R) = Polynomial.C
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.GrindCnstr.maxInsts : Lean.Parser.Parser
-- Init.Data.UInt.Lemmas
UInt32.ofBitVec_lt_iff_lt : ∀ {a b : BitVec 32}, { toBitVec := a } < { toBitVec := b } ↔ a < b
-- Mathlib.NumberTheory.Cyclotomic.Gal
/-- `IsPrimitiveRoot.autToPow` is injective in the case that it's considered over a cyclotomic
field extension.  -/
IsPrimitiveRoot.autToPow_injective : ∀ {n : ℕ} [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] {L : Type u_2} {μ : L} [inst_2 : CommRing L]
  [inst_3 : IsDomain L] (hμ : IsPrimitiveRoot μ n) [inst_4 : Algebra K L] [IsCyclotomicExtension {n} K L],
  Function.Injective ⇑(IsPrimitiveRoot.autToPow K hμ)
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
/-- If we take the path along the spine of the `j`th face of a `spineToSimplex`,
the common vertices will agree with those of the original path `f`. In particular,
a vertex `i` with `i < j` can be identified with the same vertex in `f`.  -/
SSet.Truncated.StrictSegal.spine_δ_vertex_lt : ∀ {n : ℕ} {X : SSet.Truncated (n + 1)} (sx : X.StrictSegal) (m : ℕ) (h : m ≤ n) (f : X.Path (m + 1)) {i : Fin (m + 1)}
  {j : Fin (m + 2)},
  i.castSucc < j →
    (X.spine m ⋯
            ((CategoryTheory.ConcreteCategory.hom
                (X.map (SimplexCategory.Truncated.Hom.tr (SimplexCategory.δ j) ⋯ ⋯).op))
              (sx.spineToSimplex (m + 1) ⋯ f))).vertex
        i =
      f.vertex i.castSucc
-- Mathlib.Data.Finsupp.Interval
Finsupp.rangeIcc_apply : ∀ {ι : Type u_1} {α : Type u_2} [inst : Zero α] [inst_1 : PartialOrder α] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : DecidableEq ι] (f g : ι →₀ α) (i : ι), (f.rangeIcc g) i = Finset.Icc (f i) (g i)
-- Mathlib.AlgebraicTopology.DoldKan.GammaCompN
AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctor.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C],
  AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctor =
    CategoryTheory.NatIso.ofComponents AlgebraicTopology.DoldKan.Γ₀NondegComplexIso ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.mul_lt_one_of_lt_of_le`.

---

Assumes left covariance.
The lemma assuming right covariance is `Right.mul_lt_one_of_lt_of_le`.  -/
mul_lt_one_of_lt_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, a < 1 → b ≤ 1 → a * b < 1
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.id_commShiftIso_hom_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_4} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (x : A) (X : C),
  (CategoryTheory.Functor.commShiftIso (CategoryTheory.Functor.id C) x).hom.app X =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.shiftFunctor C x).obj X)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Some `Nat` variables encode nested terms such as `b+1`.
This is a mapping from this kind of variable to the integer variable
representing `natCast (b+1)`.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.natDef : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr Int.Internal.Linear.Var
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.mul_const : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ {a : α}, a ≠ 0 → Function.Antiperiodic (fun x => f (x * a)) (c * a⁻¹)
-- Mathlib.Combinatorics.Additive.Energy
Finset.mulEnergy_eq_sum_sq' : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Mul α] (s t : Finset α),
  s.mulEnergy t = ∑ a ∈ s * t, {xy ∈ s ×ˢ t | xy.1 * xy.2 = a}.card ^ 2
-- Lean.Meta.Sym.IsClass
_private.Lean.Meta.Sym.IsClass.0.Lean.Meta.Sym.isClass?.go : Lean.Environment → Lean.Expr → Option Lean.Name
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.supported_union : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s t : Set α), Finsupp.supported M R (s ∪ t) = Finsupp.supported M R s ⊔ Finsupp.supported M R t
-- Mathlib.Computability.Reduce
/-- `p` is many-one reducible to `q` if there is a computable function translating questions about `p`
to questions about `q`.
 -/
ManyOneReducible : {α : Type u_1} → {β : Type u_2} → [Primcodable α] → [Primcodable β] → (α → Prop) → (β → Prop) → Prop
-- Mathlib.RingTheory.Valuation.LocalSubring
instIsIntegrallyClosedSubtypeMemValuationSubring : ∀ {K : Type u_3} [inst : Field K] (V : ValuationSubring K), IsIntegrallyClosed ↥V
-- Lean.Parser.Attr
Lean.Parser.Attr.export.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.Float.Float
/-- Computes the hyperbolic sine of a floating-point number.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`sinh`.
 -/
Float.sinh : Float → Float
-- Mathlib.Data.ZMod.Units
ZMod.unitsMap.eq_1 : ∀ {n m : ℕ} (hm : n ∣ m), ZMod.unitsMap hm = Units.map ↑(ZMod.castHom hm (ZMod n))
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.mk.sizeOf_spec : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] [inst_2 : SizeOf Γ] [inst_3 : SizeOf A] (val : ↥v.integer)
  (valuation_gt_one : v.IsUniformizer ↑val),
  sizeOf { val := val, valuation_gt_one := valuation_gt_one } = 1 + sizeOf val + sizeOf valuation_gt_one
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- Multiplication on the left by `m` tends to `𝓝 m` if and only if multiplication on the right
does, provided the elements are eventually selfadjoint along the filter `l`.  -/
CStarAlgebra.tendsto_mul_left_iff_tendsto_mul_right : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] {l : Filter A},
  (∀ᶠ (x : A) in l, IsSelfAdjoint x) →
    ((∀ (m : A), Filter.Tendsto (fun x => m * x) l (nhds m)) ↔ ∀ (m : A), Filter.Tendsto (fun x => x * m) l (nhds m))
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.toMono_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : OmegaCompletePartialOrder α] [inst_1 : OmegaCompletePartialOrder β]
  (f : α →𝒄 β), OmegaCompletePartialOrder.ContinuousHom.toMono f = ↑f
-- Std.Do.Triple.SpecLemmas
List.Cursor.mk.sizeOf_spec : ∀ {α : Type u} {l : List α} [inst : SizeOf α] («prefix» suffix : List α) (property : «prefix» ++ suffix = l),
  sizeOf { «prefix» := «prefix», suffix := suffix, property := property } =
    1 + sizeOf «prefix» + sizeOf suffix + sizeOf property
-- Mathlib.Data.TypeVec
/-- projection on `Subtype_`  -/
TypeVec.subtypeVal : {n : ℕ} → {α : TypeVec.{u} n} → (p : α.Arrow (TypeVec.repeat n Prop)) → (TypeVec.Subtype_ p).Arrow α
-- Mathlib.GroupTheory.Nilpotent
/-- An auxiliary type-theoretic definition defining both the upper central series of
a group, and a proof that it is characteristic, all in one go.  -/
Subgroup.upperCentralSeriesAux : (G : Type u_1) → [inst : Group G] → ℕ → (H : Subgroup G) ×' H.Characteristic
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.addHom_ext : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_5} [inst_1 : AddMonoid M] {f g : SkewPolynomial R →+ M},
  (∀ (n : ℕ) (a : R), f ((SkewPolynomial.monomial n) a) = g ((SkewPolynomial.monomial n) a)) → f = g
-- Lean.Parser.Term
Lean.Parser.Term.noImplicitLambda : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Pi.Lemmas
AddCommute.pi : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {x y : (i : I) → f i},
  (∀ (i : I), AddCommute (x i) (y i)) → AddCommute x y
-- Mathlib.Analysis.Calculus.Deriv.Support
tsupport_deriv_subset : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E}, tsupport (deriv f) ⊆ tsupport f
-- Mathlib.Geometry.Euclidean.Altitude
Affine.Simplex.altitudeFoot.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  s.altitudeFoot i = ↑((s.faceOpposite i).orthogonalProjectionSpan (s.points i))
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.norm_neg : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ‖-f‖ = ‖f‖
-- Mathlib.Util.CodeActions.BinderPlicity
/-- A code action to switch between explicit and implicit binders  -/
Mathlib.CodeAction.binderPlicity : Lean.Server.CodeActionProvider
-- Init.Data.Queue
Std.Queue.mk.inj : ∀ {α : Type u} {eList dList eList_1 dList_1 : List α},
  { eList := eList, dList := dList } = { eList := eList_1, dList := dList_1 } → eList = eList_1 ∧ dList = dList_1
-- Mathlib.Data.Sum.Order
Sum.Lex.inr_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], StrictMono (⇑toLex ∘ Sum.inr)
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t) (j : J),
  CategoryTheory.CategoryStruct.comp (s.ι.app j) (P.coconePointUniqueUpToIso Q).hom = t.ι.app j
-- Mathlib.AlgebraicGeometry.Morphisms.Proper
AlgebraicGeometry.isProper_eq : @AlgebraicGeometry.IsProper =
  @AlgebraicGeometry.IsSeparated ⊓ @AlgebraicGeometry.UniversallyClosed ⊓ @AlgebraicGeometry.LocallyOfFiniteType
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.coe_sup : ∀ (μ ν : YoungDiagram), ↑(μ ⊔ ν) = ↑μ ∪ ↑ν
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ofCompletion.injEq : ∀ {K : Type u_1} [inst : Field K] {v : NumberField.InfinitePlace K} (toCompletion toCompletion_1 : (↑v).Completion),
  ({ toCompletion := toCompletion } = { toCompletion := toCompletion_1 }) = (toCompletion = toCompletion_1)
-- Lean.Data.KVMap
Lean.KVMap.instValueNat : Lean.KVMap.Value ℕ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k a : α} {v : β k},
      (Std.DTreeMap.Internal.Impl.insert! k v t).getKey! a = if compare k a = Ordering.eq then k else t.getKey! a
-- Mathlib.CategoryTheory.Bicategory.Coherence
_private.Mathlib.CategoryTheory.Bicategory.Coherence.0.CategoryTheory.FreeBicategory.normalizeAux.match_1.eq_2 : ∀ {B : Type u_2} [inst : Quiver B] {a : B}
  (motive : (x x_1 : B) → Quiver.Path a x → CategoryTheory.FreeBicategory.Hom x x_1 → Sort u_3) (x : B)
  (p : Quiver.Path a x)
  (h_1 : (x x_1 : B) → (p : Quiver.Path a x) → (f : x ⟶ x_1) → motive x x_1 p (CategoryTheory.FreeBicategory.Hom.of f))
  (h_2 : (x : B) → (p : Quiver.Path a x) → motive x x p (CategoryTheory.FreeBicategory.Hom.id x))
  (h_3 :
    (x x_1 : B) →
      (p : Quiver.Path a x) →
        (b : B) →
          (f : CategoryTheory.FreeBicategory.Hom x b) →
            (g : CategoryTheory.FreeBicategory.Hom b x_1) → motive x x_1 p (f.comp g)),
  (match x, x, p, CategoryTheory.FreeBicategory.Hom.id x with
    | x, x_1, p, CategoryTheory.FreeBicategory.Hom.of f => h_1 x x_1 p f
    | x, .(x), p, CategoryTheory.FreeBicategory.Hom.id .(x) => h_2 x p
    | x, x_1, p, f.comp g => h_3 x x_1 p b f g) =
    h_2 x p
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.algebraMap_left_apply : ∀ {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] {R : Type u_3} {T : Type u_4} [inst_2 : CommSemiring R]
  [inst_3 : Semiring T] [inst_4 : Algebra R T] {v : AbsoluteValue R S} (x : WithAbs v),
  (algebraMap (WithAbs v) T) x = (algebraMap R T) x.ofAbs
-- Mathlib.GroupTheory.Subsemigroup.Centralizer
Subsemigroup.centralizer.eq_1 : ∀ {M : Type u_1} (S : Set M) [inst : Semigroup M],
  Subsemigroup.centralizer S = { carrier := S.centralizer, mul_mem' := ⋯ }
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.ext_iff : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] {f g : M ≃ₜ* N}, f = g ↔ ∀ (x : M), f x = g x
-- Mathlib.Dynamics.FixedPoints.Support
Function.fixedSupport_def : ∀ {X : Type u_1} [inst : TopologicalSpace X] (f : X → X), Function.fixedSupport f = closure (Function.fixedPoints f)ᶜ
-- Mathlib.Algebra.Order.Ring.GeomSum
geom_sum_pos_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {n : ℕ} {x : R},
  n ≠ 0 → (0 < ∑ i ∈ Finset.range n, x ^ i ↔ Odd n ∨ 0 < x + 1)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Star
CliffordAlgebra.star_algebraMap : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (r : R), star ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r
-- Mathlib.FieldTheory.LinearDisjoint
IntermediateField.LinearDisjoint.bot_left : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (L : Type w) [inst_3 : Field L]
  [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E], ⊥.LinearDisjoint L
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.CodeBlock.mk.sizeOf_spec : ∀ (code : Lean.Elab.Term.Do.Code) (uvars : Lean.Elab.Term.Do.VarSet),
  sizeOf { code := code, uvars := uvars } = 1 + sizeOf code + sizeOf uvars
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.map_comap_eq_of_surjective : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {g : β → α},
  Function.Surjective g → MeasurableSpace.map g (MeasurableSpace.comap g m) = m
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_set_eq_one_iff : ∀ {α : Type u} {s : Set α}, Cardinal.mk ↑s = 1 ↔ ∃ x, s = {x}
-- Lean.Meta.Match.SimpH
/-- Customized `contradiction` tactic for `simpH?`  -/
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.contradiction : Lean.MVarId → Lean.MetaM Bool
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits
PresheafOfModules.limitCone_π_app_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [inst_2 :
    ∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections]
  (j : J) (X : Cᵒᵖ),
  ((PresheafOfModules.limitCone F).π.app j).app X =
    CategoryTheory.Limits.limit.π (F.comp (PresheafOfModules.evaluation R X)) j
-- Init.Control.Lawful.Instances
OptionT.run_seqLeft : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [LawfulMonad m] (x : OptionT m α) (y : OptionT m β),
  (x <* y).run = Option.elimM x.run (pure none) fun x => Option.map (Function.const β x) <$> y.run
-- Mathlib.Probability.Process.Predictable
/-- **Alias** of `MeasureTheory.IsStronglyPredictable.of_measurable_add_one`. -/
MeasureTheory.IsPredictable.of_measurable_add_one : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {E : Type u_3} [inst : TopologicalSpace E] {𝓕 : MeasureTheory.Filtration ℕ m}
  {u : ℕ → Ω → E},
  MeasureTheory.StronglyMeasurable (u 0) →
    (∀ (n : ℕ), MeasureTheory.StronglyMeasurable (u (n + 1))) → MeasureTheory.IsStronglyPredictable 𝓕 u
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_insertIfNew_self : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {v : β k}, (m.insertIfNew k v).contains k = true
-- Mathlib.RingTheory.Grassmannian
Module.Grassmannian.rankAtStalk_eq : ∀ {R : Type u} [inst : CommRing R] {M : Type v} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {k : ℕ}
  (self : Module.Grassmannian R M k) (p : PrimeSpectrum R), Module.rankAtStalk (M ⧸ self.toSubmodule) p = k
-- Mathlib.Data.Fin.Tuple.BubbleSortInduction
/-- *Bubble sort induction*: Prove that the sorted version of `f` has some property `P`
if `f` satisfies `P` and `P` is preserved on permutations of `f` when swapping two
antitone values.  -/
Tuple.bubble_sort_induction' : ∀ {n : ℕ} {α : Type u_1} [inst : LinearOrder α] {f : Fin n → α} {P : (Fin n → α) → Prop},
  P f →
    (∀ (σ : Equiv.Perm (Fin n)) (i j : Fin n),
        i < j → (f ∘ ⇑σ) j < (f ∘ ⇑σ) i → P (f ∘ ⇑σ) → P (f ∘ ⇑σ ∘ ⇑(Equiv.swap i j))) →
      P (f ∘ ⇑(Tuple.sort f))
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
Algebra.TensorProduct.includeRight.eq_1 : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B],
  Algebra.TensorProduct.includeRight =
    { toFun := (↑((TensorProduct.AlgebraTensorModule.mk R R A B) 1).toAddMonoidHom).toFun, map_one' := ⋯, map_mul' := ⋯,
      map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }
-- Std.Time.DateTime
/-- Subtract `Day.Offset` from a `DateTime`.
 -/
Std.Time.DateTime.subDays : Std.Time.DateTime → Std.Time.Day.Offset → Std.Time.DateTime
-- Mathlib.Algebra.Quaternion
Quaternion.imI_coe : ∀ {R : Type u_3} [inst : CommRing R] (x : R), (↑x).imI = 0
-- Mathlib.Probability.Distributions.Gaussian.Multivariate
ProbabilityTheory.covarianceBilin_stdGaussian : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E],
  ProbabilityTheory.covarianceBilin (ProbabilityTheory.stdGaussian E) = innerSL ℝ
-- Mathlib.Algebra.Group.Shrink
Shrink.instMulOneClass.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : MulOneClass α],
  Shrink.instMulOneClass = (equivShrink α).symm.mulOneClass
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.hasSmallestLimitsOfHasLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasLimitsOfSize.{0, 0, v, u} C
-- Lean.Meta.Sym.AlphaShareCommon
Lean.Meta.Sym.AlphaKey : Type
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.tensorμ_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ W X Y Z)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z)) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.SemiCartesianMonoidalCategory.fst W X)
      (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z)
-- Init.Data.List.Perm
List.Perm.eq_singleton : ∀ {α : Type u_1} {l : List α} {a : α}, l.Perm [a] → l = [a]
-- Mathlib.Data.ENNReal.Basic
ENNReal.toReal_zero : ENNReal.toReal 0 = 0
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.mk_inf_mk : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} (a b : α) (ha : a ∈ L) (hb : b ∈ L),
  ⟨a, ha⟩ ⊓ ⟨b, hb⟩ = ⟨a ⊓ b, ⋯⟩