mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Hom.Open
ContinuousOpenMap.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : SizeOf α]
  [inst_3 : SizeOf β] (toContinuousMap : C(α, β)) (map_open' : IsOpenMap toContinuousMap.toFun),
  sizeOf { toContinuousMap := toContinuousMap, map_open' := map_open' } = 1 + sizeOf toContinuousMap
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.eq_zero_rpow_iff : ∀ {x a : ℝ}, a = 0 ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.δ_objEquiv_symm_apply : ∀ {n : ℕ} {m : SimplexCategory} (f : { len := n + 1 } ⟶ m) (i : Fin (n + 2)),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.δ (SSet.stdSimplex.obj m) i))
      (SSet.stdSimplex.objEquiv.symm f) =
    SSet.stdSimplex.objEquiv.symm (CategoryTheory.CategoryStruct.comp (SimplexCategory.δ i) f)
-- Mathlib.Order.CompleteLattice.Basic
iSup_emptyset : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α}, ⨆ x ∈ ∅, f x = ⊥
-- Lean.Meta.Match.MatcherApp.Transform
/-- All proper fvars in binding order, matching the lambdas that `transform` wraps around the alt result.  -/
Lean.Meta.MatcherApp.TransformAltFVars.all : Lean.Meta.MatcherApp.TransformAltFVars → Array Lean.Expr
-- Mathlib.Combinatorics.Quiver.Prefunctor
/-- An equality of prefunctors gives an equality on homs.  -/
Prefunctor.congr_hom : ∀ {U : Type u_1} {V : Type u_2} [inst : Quiver U] [inst_1 : Quiver V] {F G : U ⥤q V} (e : F = G) {X Y : U} (f : X ⟶ Y),
  Quiver.homOfEq (F.map f) ⋯ ⋯ = G.map f
-- Mathlib.Topology.EMetricSpace.Basic
/-- Expressing locally uniform convergence on a set using `edist`.  -/
EMetric.tendstoLocallyUniformlyOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] {ι : Type u_2} [inst_1 : TopologicalSpace β] {F : ι → β → α}
  {f : β → α} {p : Filter ι} {s : Set β},
  TendstoLocallyUniformlyOn F f p s ↔
    ∀ ε > 0, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (n : ι) in p, ∀ y ∈ t, edist (f y) (F n y) < ε
-- Init.Data.Repr
/-- Converts a natural number to its decimal string representation.
 -/
Nat.repr : ℕ → String
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.subtype.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G],
  ↑H = { toFun := Subtype.val, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.mk : {G : Type u} →
  [toAddMonoid : AddMonoid G] →
    [toNeg : Neg G] →
      [toSub : Sub G] →
        [toZSMul : ZSMul G] →
          autoParam (∀ (a b : G), a - b = a + -b) SubNegMonoid.sub_eq_add_neg._autoParam →
            autoParam (∀ (a : G), 0 • a = 0) SubNegMonoid.zsmul_zero'._autoParam →
              autoParam (∀ (n : ℕ) (a : G), ↑n.succ • a = ↑n • a + a) SubNegMonoid.zsmul_succ'._autoParam →
                autoParam (∀ (n : ℕ) (a : G), Int.negSucc n • a = -(↑n.succ • a)) SubNegMonoid.zsmul_neg'._autoParam →
                  SubNegMonoid G
-- Aesop.Script.Step
Aesop.Script.Step.uTactic : Aesop.Script.Step → Aesop.Script.UTactic
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (inner : Std.HashMap.Raw α Unit), sizeOf { inner := inner } = 1 + sizeOf inner
-- Mathlib.Algebra.Prime.Defs
Prime.dvd_mul : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p : M}, Prime p → ∀ {a b : M}, p ∣ a * b ↔ p ∣ a ∨ p ∣ b
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_zero : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), ↑0 = 0
-- Mathlib.RingTheory.PowerSeries.PiTopology
PowerSeries.WithPiTopology.tprod_one_sub_X_pow_ne_zero : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : TopologicalSpace R] [T2Space R] [Nontrivial R],
  ∏' (i : ℕ), (1 - PowerSeries.X ^ (i + 1)) ≠ 0
-- Mathlib.Data.Prod.Basic
Function.Injective.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ},
  Function.Injective f → Function.Injective g → Function.Injective (Prod.map f g)
-- Mathlib.Order.Interval.Set.LinearOrder
Set.notMem_Iio : ∀ {α : Type u_1} [inst : LinearOrder α] {a c : α}, c ∉ Set.Iio a ↔ a ≤ c
-- Mathlib.RingTheory.Noetherian.Defs
isNoetherian_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsNoetherian R M ↔ WellFounded fun x1 x2 => x1 > x2
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.snd_mul : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : Mul α] [inst_2 : MulLeftMono α] [inst_3 : MulRightMono α]
  (s t : NonemptyInterval α), (s * t).toProd.2 = s.toProd.2 * t.toProd.2
-- Mathlib.Algebra.Polynomial.Div
Polynomial.sum_modByMonic_coeff : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R},
  q.Monic → ∀ {n : ℕ}, q.degree ≤ ↑n → ∑ i, (Polynomial.monomial ↑i) ((p %ₘ q).coeff ↑i) = p %ₘ q
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.instEpiOpcyclesMapOfF : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i] [CategoryTheory.Epi (φ.f i)], CategoryTheory.Epi (HomologicalComplex.opcyclesMap φ i)
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
/-- The projection `c.pt ⟶ F.obj j` for `c : WeightedCone W F`
and `x : W.obj j`.  -/
CategoryTheory.Limits.WeightedCone.π : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {W : CategoryTheory.Functor J (Type w)} →
          {F : CategoryTheory.Functor J C} →
            (c : CategoryTheory.Limits.WeightedCone W F) → {j : J} → W.obj j → (c.pt ⟶ F.obj j)
-- Init.Data.Nat.Lemmas
Nat.sub_one : ∀ (n : ℕ), n - 1 = n.pred
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for monotonicity of addition on the left,
namely `b₁ ≤ b₂ → a + b₁ ≤ a + b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedAddMonoid`.  -/
AddLeftMono : (M : Type u_1) → [Add M] → [LE M] → Prop
-- Mathlib.Data.Set.Insert
Set.singleton_ne_empty : ∀ {α : Type u_1} (a : α), {a} ≠ ∅
-- Mathlib.Topology.EMetricSpace.Defs
Metric.mem_eball : ∀ {α : Type u} [inst : EDist α] {x y : α} {ε : ENNReal}, y ∈ Metric.eball x ε ↔ edist y x < ε
-- Mathlib.Data.Fin.Tuple.NatAntidiagonal
_private.Mathlib.Data.Fin.Tuple.NatAntidiagonal.0.List.Nat.antidiagonalTuple.match_1.eq_3 : ∀ (motive : ℕ → ℕ → Sort u_1) (k n : ℕ) (h_1 : Unit → motive 0 0) (h_2 : (n : ℕ) → motive 0 n.succ)
  (h_3 : (k n : ℕ) → motive k.succ n),
  (match k.succ, n with
    | 0, 0 => h_1 ()
    | 0, n.succ => h_2 n
    | k.succ, n => h_3 k n) =
    h_3 k n
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableOn_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {s : Set E} (n : ℕ) [inst_7 : OfNat F n], DifferentiableOn 𝕜 (OfNat.ofNat n) s
-- Mathlib.Order.Concept
Concept.instMin : {α : Type u_2} → {β : Type u_3} → {r : α → β → Prop} → Min (Concept α β r)
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.col_submatrix : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {m₀ : Type u_10} {n₀ : Type u_11} (A : Matrix m n α) (r : m₀ → m)
  (c : n₀ → n) (j : n₀), (A.submatrix r c).col j = (A.submatrix r id).col (c j)
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- A family of units is of maximal rank iff the index of the subgroup it generates has finite index.
 -/
NumberField.Units.isMaxRank_iff_closure_finiteIndex : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  {u : Fin (NumberField.Units.rank K) → (NumberField.RingOfIntegers K)ˣ},
  NumberField.Units.IsMaxRank u ↔ (Subgroup.closure (Set.range u)).FiniteIndex
-- Mathlib.Algebra.Module.LinearMap.End
Module.End.isUnit_inv_apply_apply_of_isUnit : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {f : Module.End R M} (h : IsUnit f) (x : M), h.unit.inv (f x) = x
-- Mathlib.SetTheory.Cardinal.ENat
/-- Projection from cardinals to `ℕ∞`. Sends all infinite cardinals to `⊤`.

We define this function as a bundled monotone ring homomorphism.  -/
Cardinal.toENat : Cardinal.{u} →+*o ℕ∞
-- Aesop.RulePattern
/-- Discrimination tree keys for `p`.
 -/
Aesop.RulePattern.discrTreeKeys : Aesop.RulePattern → Array Lean.Meta.DiscrTree.Key
-- Init.Control.Lawful.Instances
OptionT.ext : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {x y : OptionT m α}, x.run = y.run → x = y
-- Init.Data.UInt.Bitwise
UInt8.toBitVec_or : ∀ (a b : UInt8), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Mathlib.Algebra.Lie.Basic
/-- The composition of morphisms is a morphism.  -/
LieHom.comp : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      {L₃ : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L₁] →
            [inst_2 : LieAlgebra R L₁] →
              [inst_3 : LieRing L₂] →
                [inst_4 : LieAlgebra R L₂] →
                  [inst_5 : LieRing L₃] → [inst_6 : LieAlgebra R L₃] → (L₂ →ₗ⁅R⁆ L₃) → (L₁ →ₗ⁅R⁆ L₂) → L₁ →ₗ⁅R⁆ L₃
-- Mathlib.Data.List.Perm.Lattice
List.Perm.inter_append : ∀ {α : Type u_1} [inst : DecidableEq α] {l t₁ t₂ : List α}, t₁.Disjoint t₂ → (l ∩ (t₁ ++ t₂)).Perm (l ∩ t₁ ++ l ∩ t₂)
-- Mathlib.LinearAlgebra.TensorProduct.Basis
Module.Basis.baseChange_repr_tmul : ∀ {R : Type u_1} {M : Type u_3} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (S : Type u_7) [inst_3 : Semiring S] [inst_4 : Algebra R S] (b : Module.Basis ι R M) (x : S) (y : M) (i : ι),
  ((Module.Basis.baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i • x
-- Mathlib.LinearAlgebra.BilinearForm.Hom
LinearMap.BilinForm.congr_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {M' : Type u_7}
  [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (e : M ≃ₗ[R] M') (B : LinearMap.BilinForm R M) (x y : M'),
  (((LinearMap.BilinForm.congr e) B) x) y = (B (e.symm x)) (e.symm y)
-- Mathlib.Topology.Category.CompHaus.Basic
/-- The limit cone `CompHaus.limitCone F` is indeed a limit cone.  -/
CompHaus.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CompHaus) → CategoryTheory.Limits.IsLimit (CompHaus.limitCone F)
-- Mathlib.Order.Notation
/-- The top (`⊤`, `\top`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊤` in identifiers is `top`. -/
«term⊤» : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.prodMkLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (γ : Type u_5)
  [inst : MeasurableSpace γ] (κ : ProbabilityTheory.Kernel α β),
  ProbabilityTheory.Kernel.prodMkLeft γ κ = κ.comap Prod.snd ⋯
-- Lean.Elab.Attributes
Lean.Elab.Attribute.mk.inj : ∀ {kind : Lean.AttributeKind} {name : Lean.Name} {stx : Lean.Syntax} {kind_1 : Lean.AttributeKind} {name_1 : Lean.Name}
  {stx_1 : Lean.Syntax},
  { kind := kind, name := name, stx := stx } = { kind := kind_1, name := name_1, stx := stx_1 } →
    kind = kind_1 ∧ name = name_1 ∧ stx = stx_1
-- Std.Time.DateTime
/-- Returns the week of the month for the given `DateTime`, where weeks start on `firstDay`.
The first partial week containing day 1 is week 1, so weeks may span fewer than 7 days.
 -/
Std.Time.DateTime.weekOfMonth : Std.Time.DateTime → optParam Std.Time.Weekday Std.Time.Weekday.monday → Std.Time.Week.Ordinal
-- Std.Net.Addr
Std.Net.SocketAddressV4.mk.inj : ∀ {addr : Std.Net.IPv4Addr} {port : UInt16} {addr_1 : Std.Net.IPv4Addr} {port_1 : UInt16},
  { addr := addr, port := port } = { addr := addr_1, port := port_1 } → addr = addr_1 ∧ port = port_1
-- Mathlib.CategoryTheory.Adjunction.Additive
/-- If we have an adjunction `adj : F ⊣ G` of functors between preadditive categories,
and if `F` is additive, then the hom set equivalence upgrades to an isomorphism between
`G ⋙ preadditiveYoneda` and `preadditiveYoneda ⋙ F`, once we throw in the necessary
universe lifting functors.
Note that `F` is additive if and only if `G` is, by `Adjunction.right_adjoint_additive` and
`Adjunction.left_adjoint_additive`.
 -/
CategoryTheory.Adjunction.compPreadditiveYonedaIso : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (F ⊣ G) →
                  [F.Additive] →
                    G.comp
                        (CategoryTheory.preadditiveYoneda.comp
                          ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj
                            AddCommGrpCat.uliftFunctor)) ≅
                      CategoryTheory.preadditiveYoneda.comp
                        (((CategoryTheory.Functor.whiskeringLeft Cᵒᵖ Dᵒᵖ AddCommGrpCat).obj F.op).comp
                          ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ AddCommGrpCat AddCommGrpCat).obj
                            AddCommGrpCat.uliftFunctor))
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.limitIsoLimitCurryCompLim_inv_π : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)]
  {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitIsoLimitCurryCompLim G).inv
      (CategoryTheory.Limits.limit.π G (j, k)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim) j)
      (CategoryTheory.Limits.limit.π ((CategoryTheory.Functor.curry.obj G).obj j) k)
-- Mathlib.Topology.EMetricSpace.Defs
/-- ε-δ characterization of uniform continuity on a set for pseudoemetric spaces  -/
EMetric.uniformContinuousOn_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {s : Set α},
  UniformContinuousOn f s ↔
    ∀ ε > 0, ∃ δ > 0, ∀ {a : α}, a ∈ s → ∀ {b : α}, b ∈ s → edist a b < δ → edist (f a) (f b) < ε
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
/-- A `AddEquiv` version of `Equiv.withTopCongr`.  -/
AddEquiv.withTopCongr : {α : Type u} → {β : Type v} → [inst : Add α] → [inst_1 : Add β] → α ≃+ β → WithTop α ≃+ WithTop β
-- Mathlib.Topology.EMetricSpace.Weak
/-- `ℝ≥0∞` is a weak extended metric space with its usual distance function.  -/
instWeakEMetricSpaceENNReal : WeakEMetricSpace ENNReal
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableOn.sum_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B}
  {ι : Type u_9} {s : Finset ι} {t : ι → (x : B) → E x},
  (∀ i ∈ s, MDiff[u] (T% t)) → MDiff[u] fun x => ⟨x, ∑ i ∈ s, t i x⟩
-- Mathlib.Order.Filter.CardinalInter
/-- Every CardinalInterFilter with c > ℵ₀ is a CountableInterFilter  -/
CardinalInterFilter.toCountableInterFilter : ∀ {α : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c], Cardinal.aleph0 < c → CountableInterFilter l
-- Mathlib.RepresentationTheory.Rep.Basic
/-- Given `f : α → A`, the natural representation morphism `(α →₀ k[G]) ⟶ A` sending
`single a (single g r) ↦ r • A.ρ g (f a)`.  -/
Rep.freeLift : (k : Type u) →
  (G : Type v) →
    [inst : CommRing k] →
      [inst_1 : Monoid G] → {α : Type u'} → (A : Rep.{max (max u u') v, u, v} k G) → (α → ↑A) → (Rep.free k G α ⟶ A)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.mul_card_image_le_card : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] {f : α → β} (s : Finset α) (n : ℕ),
  (∀ b ∈ Finset.image f s, n ≤ {a ∈ s | f a = b}.card) → n * (Finset.image f s).card ≤ s.card
-- Mathlib.Analysis.Rat.NatSqrt.Real
Nat.ratSqrt_le_realSqrt : ∀ (x : ℕ) {prec : ℕ}, 0 < prec → ↑(x.ratSqrt prec) ≤ √↑x
-- Mathlib.Analysis.Normed.Module.Normalize
NormedSpace.normalize_smul : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (r : ℝ) (x : V),
  NormedSpace.normalize (r • x) = ↑(SignType.sign r) • NormedSpace.normalize x
-- Init.Notation
/-- `#check_simp t ~> r` checks `simp` reduces `t` to `r`.
 -/
Lean.Parser.checkSimp : Lean.ParserDescr
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
ArithmeticFunction.IsMultiplicative.ppow : ∀ {R : Type u_1} [inst : CommSemiring R] {f : ArithmeticFunction R},
  f.IsMultiplicative → ∀ {k : ℕ}, (f.ppow k).IsMultiplicative
-- Mathlib.Algebra.Module.LinearMap.Basic
LinearMap.mulRight_inj : ∀ {R : Type u_6} {A : Type u_7} [inst : Semiring R] [inst_1 : NonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] {a b : A}, LinearMap.mulRight R a = LinearMap.mulRight R b ↔ a = b
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
/-- The quadratic version of `_root_.map_finsupp_sum`.  -/
QuadraticMap.map_finsuppSum : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  (Q : QuadraticMap R M N) (f : ι →₀ R) (g : ι → R → M),
  Q (f.sum g) =
    (f.sum fun i r => Q (g i r)) +
      ∑ p ∈ f.support.sym2 with ¬p.IsDiag, QuadraticMap.polarSym2 (⇑Q) (Sym2.map (fun i => g i (f i)) p)
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftFunction : {m : Type u → Type v} → {n : Type u → Type w} → [Monad m] → [Monad n] → (⦃α : Type u⦄ → m α → n α) → Prop
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a MonoidHom `f : M →* N` and Submonoid `S ⊆ M` such that `f(S) ⊆ Nˣ`, for all
`y ∈ S`, `(f y)⁻¹` is unique.  -/
Submonoid.LocalizationMap.inv_unique : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
  (h : ∀ (y : ↥S), IsUnit (f ↑y)) {y : ↥S} {z : N}, f ↑y * z = 1 → ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_add_left : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] {x y z : E}, inner A (x + y) z = inner A x z + inner A y z
-- Mathlib.GroupTheory.Exponent
Subgroup.exponent_toSubmonoid : ∀ {G : Type u} [inst : Group G] (H : Subgroup G), Monoid.exponent ↥H.toSubmonoid = Monoid.exponent ↥H
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.sup_span : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M)
  {s : Set M}, p ⊔ Submodule.span R s = Submodule.span R (↑p ∪ s)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.mapIso_counitIso_inv_app_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T T' : D} {S : CategoryTheory.Functor C D} (i : T ≅ T')
  (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T')),
  ((CategoryTheory.CostructuredArrow.mapIso i).counitIso.inv.app X).left = CategoryTheory.CategoryStruct.id X.left
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.lift_left_mul_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.GrpObj B] {f g : A ⟶ B} (i : A ⟶ B),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f i) CategoryTheory.MonObj.mul =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g i) CategoryTheory.MonObj.mul →
    f = g
-- Mathlib.Analysis.Real.Sqrt
NNReal.sqrt_le_one : ∀ {x : NNReal}, NNReal.sqrt x ≤ 1 ↔ x ≤ 1
-- Mathlib.SetTheory.Cardinal.Order
Function.Embedding.cardinal_le : ∀ {α β : Type u} (f : α ↪ β), Cardinal.mk α ≤ Cardinal.mk β
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.OneLine.State.line : Lean.PrettyPrinter.OneLine.State → Std.Format
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.neg_add_cancel : ∀ {α : Type u} [inst : SubtractionMonoid α] {a : α}, IsAddUnit a → -a + a = 0
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNonAssocRing : {Γ : Type u_1} →
  {R : Type u_3} →
    [inst : AddCommMonoid Γ] →
      [inst_1 : PartialOrder Γ] → [IsOrderedCancelAddMonoid Γ] → [inst : NonAssocRing R] → NonAssocRing (HahnSeries Γ R)
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.one_sub_inv : ∀ {p q : ℝ}, p.HolderConjugate q → 1 - p⁻¹ = q⁻¹
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_inv_of_pos : ∀ {x : ℝ}, 0 < x → Real.arctan x⁻¹ = Real.pi / 2 - Real.arctan x
-- Std.Tactic.BVDecide.LRAT.Internal.Entails
Std.Tactic.BVDecide.LRAT.Internal.Liff.trans : ∀ {α : Type u} {σ1 : Type v} {σ2 : Type w} {σ3 : Type x} [inst : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ1]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ2] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ3]
  (f1 : σ1) (f2 : σ2) (f3 : σ3),
  Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f2 →
    Std.Tactic.BVDecide.LRAT.Internal.Liff α f2 f3 → Std.Tactic.BVDecide.LRAT.Internal.Liff α f1 f3
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constToList_perm : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.DHashMap.Raw α fun x => β},
  m₁.Equiv m₂ → (Std.DHashMap.Raw.Const.toList m₁).Perm (Std.DHashMap.Raw.Const.toList m₂)
-- Mathlib.AlgebraicTopology.DoldKan.FunctorGamma
AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : ChainComplex C ℕ) {Δ' Δ : SimplexCategory} (i i_1 : Δ' ⟶ Δ) (e_i : i = i_1) [inst_2 : CategoryTheory.Mono i],
  AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i = AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono K i_1
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet.eq_1 : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) (s : ι → Set Ω) (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
  ProbabilityTheory.iCondIndepSet m' hm' s μ =
    ProbabilityTheory.Kernel.iIndepSet s (ProbabilityTheory.condExpKernel μ m') (μ.trim hm')
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_of_isEmpty : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {a : α},
  t.isEmpty = true → t.contains a = false
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.lift_ι_apply : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = 0) (x : M),
  ((ExteriorAlgebra.lift R) ⟨f, cond⟩) ((ExteriorAlgebra.ι R) x) = f x