mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_polynomial : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W.baseChange B).polynomial = Polynomial.map (Polynomial.mapRingHom ↑f) (W.baseChange A).polynomial
-- Mathlib.Order.Defs.LinearOrder
/-- A linear order is reflexive, transitive, antisymmetric and total relation `≤`.
We assume that every linear ordered type has decidable `(≤)`, `(<)`, and `(=)`.  -/
LinearOrder : Type u_2 → Type u_2
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.neg_hom_apply : ∀ {X Y : AddSemigrp} (e : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) x) = x
-- Mathlib.Order.Atoms
exists_le_covBy_of_lt : ∀ {α : Type u_4} {a b : α} [inst : Preorder α] [IsStronglyCoatomic α], a < b → ∃ x, a ≤ x ∧ x ⋖ b
-- Mathlib.Algebra.Group.Action.Opposite
Semigroup.opposite_smulCommClass' : ∀ {α : Type u_3} [inst : Semigroup α], SMulCommClass α αᵐᵒᵖ α
-- Mathlib.AlgebraicTopology.DoldKan.Normalized
AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] [inst_1 : CategoryTheory.Abelian A]
  (X : CategoryTheory.SimplicialObject A) (n : ℕ),
  (AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex X).f n =
    (AlgebraicTopology.NormalizedMooreComplex.objX X n).factorThru (AlgebraicTopology.DoldKan.PInfty.f n) ⋯
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- A "left" subset of `card α` vertices and a "right" subset of `card β` vertices such that every
vertex in the "left" subset is adjacent to every vertex in the "right" subset gives rise to a copy
of a complete bipartite graph.  -/
SimpleGraph.Copy.completeBipartiteGraph : {V : Type u_1} →
  {G : SimpleGraph V} →
    {α : Type u_2} →
      {β : Type u_3} →
        [inst : Fintype α] →
          [inst_1 : Fintype β] →
            (left right : Finset V) →
              left.card = Fintype.card α →
                right.card = Fintype.card β → G.IsCompleteBetween ↑left ↑right → (completeBipartiteGraph α β).Copy G
-- Mathlib.Algebra.Group.Conj
AddConjClasses.carrier.eq_1 : ∀ {α : Type u} [inst : AddMonoid α], AddConjClasses.carrier = Quotient.lift addConjugatesOf ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) [inst_2 : S.HasHomology]
  {Z : C} (h : h₂.H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂) h =
    CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv (CategoryTheory.CategoryStruct.comp h₂.homologyIso.hom h)
-- Init.Data.Int.Order
Int.min_le_left : ∀ (a b : ℤ), min a b ≤ a
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullback.lift_π_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} {objs : J → C}
  (arrows : (j : J) → objs j ⟶ B) [inst_1 : CategoryTheory.Limits.HasWidePullback B objs arrows] {X : C} (f : X ⟶ B)
  (fs : (j : J) → X ⟶ objs j) (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp (fs j) (arrows j) = f) (j : J) {Z : C}
  (h : objs j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.lift f fs w)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π arrows j) h) =
    CategoryTheory.CategoryStruct.comp (fs j) h
-- Mathlib.Lean.Expr.Basic
/-- Update the value of a `ConstantInfo`, if it has one.  -/
Lean.ConstantInfo.updateValue : Lean.ConstantInfo → Lean.Expr → Lean.ConstantInfo
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.eq_1 : ∀ (x : ℝ), x.smoothTransition = expNegInvGlue x / (expNegInvGlue x + expNegInvGlue (1 - x))
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.fiber_map_injective_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  [CategoryTheory.LocallySmall.{w, v, u} C] {U T : C} (f : U ⟶ T) [CategoryTheory.Mono f],
  Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (Φ.fiber.map f))
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The ordinal-indexed sequence approximating the greatest fixed point greater than
an initial value `x`. It is defined in such a way that we have `gfpApprox 0 x = x` and
`gfpApprox a x = ⨅ b < a, f (lfpApprox b x)`.  -/
OrdinalApprox.gfpApprox : {α : Type u} → [inst : CompleteLattice α] → (α →o α) → α → Ordinal.{u} → α
-- Mathlib.Tactic.CongrExclamation
/-- A more insistent version of `Lean.MVarId.congrN`.
See the documentation on the `congr!` syntax.

The `depth?` argument controls the depth of the recursion. If `none`, then it uses a reasonably
large bound that is linear in the expression depth.  -/
Lean.MVarId.congrN! : Lean.MVarId →
  optParam (Option ℕ) none →
    optParam Congr!.Config { } → optParam (List (Lean.TSyntax `rintroPat)) [] → Lean.MetaM (List Lean.MVarId)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.contains_of_contains_insertMany_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k : α},
      (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).contains k = true →
        (List.map Prod.fst l).contains k = false → m.contains k = true
-- Mathlib.Algebra.Group.Hom.Basic
/-- Multiplication by an integer `n` on a commutative additive group,
considered as an additive group homomorphism.  -/
zsmulAddGroupHom : {α : Type u_1} → [inst : SubtractionCommMonoid α] → ℤ → α →+ α
-- Lean.Elab.MutualDef
Lean.Elab.Term.warn.exposeOnPrivate : Lean.Option Bool
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
IsTranscendenceBasis.eq_1 : ∀ {ι : Type u_1} (R : Type u_3) {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (x : ι → A),
  IsTranscendenceBasis R x =
    (AlgebraicIndependent R x ∧ ∀ (s : Set A), AlgebraicIndepOn R id s → Set.range x ⊆ s → Set.range x = s)
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
/-- If `v : M → TM` is a vector field on `M`, `IsMIntegralCurve γ v` means `γ : ℝ → M` is a global
integral curve of `v`. That is, `γ t` is tangent to `v (γ t)` for all `t : ℝ`.  -/
IsMIntegralCurve : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type u_3} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] → (ℝ → M) → ((x : M) → TangentSpace I x) → Prop
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  t.WF → (Std.DTreeMap.Raw.filter f t).get? k = Option.filter (f k) (t.get? k)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.filter_eq_self_iff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool},
  Std.ExtDTreeMap.filter f t = t ↔ ∀ (k : α) (h : k ∈ t), f k (t.get k h) = true
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.mk.injEq : ∀ (label : String) (detail? : Option String) (documentation? : Option Lean.Lsp.MarkupContent)
  (kind? : Option Lean.Lsp.CompletionItemKind) (textEdit? : Option Lean.Lsp.InsertReplaceEdit)
  (sortText? : Option String) (data? : Option Lean.Json) (tags? : Option (Array Lean.Lsp.CompletionItemTag))
  (label_1 : String) (detail?_1 : Option String) (documentation?_1 : Option Lean.Lsp.MarkupContent)
  (kind?_1 : Option Lean.Lsp.CompletionItemKind) (textEdit?_1 : Option Lean.Lsp.InsertReplaceEdit)
  (sortText?_1 : Option String) (data?_1 : Option Lean.Json) (tags?_1 : Option (Array Lean.Lsp.CompletionItemTag)),
  ({ label := label, detail? := detail?, documentation? := documentation?, kind? := kind?, textEdit? := textEdit?,
        sortText? := sortText?, data? := data?, tags? := tags? } =
      { label := label_1, detail? := detail?_1, documentation? := documentation?_1, kind? := kind?_1,
        textEdit? := textEdit?_1, sortText? := sortText?_1, data? := data?_1, tags? := tags?_1 }) =
    (label = label_1 ∧
      detail? = detail?_1 ∧
        documentation? = documentation?_1 ∧
          kind? = kind?_1 ∧ textEdit? = textEdit?_1 ∧ sortText? = sortText?_1 ∧ data? = data?_1 ∧ tags? = tags?_1)
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
/-- Given a positive integer `n`, `modularCyclotomicCharacter' n` is a
multiplicative homomorphism from the automorphisms of a field `L` to `(ℤ/dℤ)ˣ`,
where `d` is the number of `n`-th roots of unity in `L`. It is uniquely
characterised by the property that `g(ζ)=ζ^(modularCyclotomicCharacter n g)`
for `g` an automorphism of `L` and `ζ` an `n`th root of unity.  -/
modularCyclotomicCharacter' : (L : Type u) →
  [inst : CommRing L] → [IsDomain L] → (n : ℕ) → [NeZero n] → (L ≃+* L) →* (ZMod (Nat.card ↥(rootsOfUnity n L)))ˣ
-- Mathlib.Tactic.ComputeDegree
Mathlib.Tactic.ComputeDegree.coeff_sub_of_eq : ∀ {R : Type u_1} [inst : Ring R] {n : ℕ} {a b : R} {f g : Polynomial R},
  f.coeff n = a → g.coeff n = b → (f - g).coeff n = a - b
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
/-- The transvection `1 + b · E_{i,j}` (the identity plus `b` in position `(i, j)`)
as an element of `SL ι F`, when `i ≠ j`.  -/
Matrix.SpecialLinearGroup.transvection : {ι : Type u_1} →
  {F : Type u_2} →
    [inst : DecidableEq ι] →
      [inst_1 : Fintype ι] → [inst_2 : CommRing F] → {i j : ι} → i ≠ j → F → Matrix.SpecialLinearGroup ι F
-- Mathlib.GroupTheory.Torsion
AddCommGroup.torsion.eq_1 : ∀ (G : Type u_1) [inst : AddCommGroup G],
  AddCommGroup.torsion G = { toAddSubmonoid := AddCommMonoid.addTorsion G, neg_mem' := ⋯ }
-- Mathlib.CategoryTheory.Sites.Sieves
/-- A convenient constructor for a refinement of a presieve of the form `Presieve.ofArrows`.
This contains a sieve obtained by `Sieve.bind` and `Sieve.ofArrows`, see
`Presieve.bind_ofArrows_le_bindOfArrows`, but has better definitional properties.  -/
CategoryTheory.Presieve.bindOfArrows : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {ι : Type u_1} →
      {X : C} →
        (Y : ι → C) → ((i : ι) → Y i ⟶ X) → ((i : ι) → CategoryTheory.Presieve (Y i)) → CategoryTheory.Presieve X
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_const : ∀ {ps : Std.Do.PostShape} {α : Type u} (p : Std.Do.Assertion ps) (Q : Std.Do.PostCond α ps),
  (Std.Do.PredTrans.const p).apply Q = p
-- Mathlib.Order.Category.BddOrd
BddOrd.hom_ext_iff : ∀ {X Y : BddOrd} {f g : X ⟶ Y}, f = g ↔ BddOrd.Hom.hom f = BddOrd.Hom.hom g
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- The functor going from the underlying category of the enriched category `Cᵒᵖ`
to the opposite of the underlying category of the enriched category `C`.  -/
CategoryTheory.forgetEnrichmentOppositeEquivalence.functor : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      [inst_2 : CategoryTheory.BraidedCategory V] →
        (C : Type u) →
          [inst_3 : CategoryTheory.EnrichedCategory V C] →
            CategoryTheory.Functor (CategoryTheory.ForgetEnrichment V Cᵒᵖ) (CategoryTheory.ForgetEnrichment V C)ᵒᵖ
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.Transition.mk.injEq : ∀ (time : Std.Time.Second.Offset) (localTimeType : Std.Time.TimeZone.LocalTimeType) (time_1 : Std.Time.Second.Offset)
  (localTimeType_1 : Std.Time.TimeZone.LocalTimeType),
  ({ time := time, localTimeType := localTimeType } = { time := time_1, localTimeType := localTimeType_1 }) =
    (time = time_1 ∧ localTimeType = localTimeType_1)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Iio₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {c : G₀} (a : G₀),
  0 < c → (fun x => c * x) ⁻¹' Set.Iio a = Set.Iio (a / c)
-- Mathlib.Algebra.Field.Opposite
AddOpposite.instNNRatCast : {α : Type u_1} → [NNRatCast α] → NNRatCast αᵃᵒᵖ
-- Mathlib.Logic.Function.Basic
Function.Bijective.piMap : ∀ {ι : Sort u_1} {α : ι → Sort u_2} {β : ι → Sort u_3} {f : (i : ι) → α i → β i},
  (∀ (i : ι), Function.Bijective (f i)) → Function.Bijective (Pi.map f)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.checkKind : Lean.SyntaxNodeKind → Lean.PrettyPrinter.FormatterM Unit
-- Init.Data.Fin.Lemmas
Fin.eq_succ_of_ne_zero : ∀ {n : ℕ} {i : Fin (n + 1)}, i ≠ 0 → ∃ j, i = j.succ
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- A subgroupoid is thin (`CategoryTheory.Subgroupoid.IsThin`) if it has at most one arrow between
any two vertices.  -/
CategoryTheory.Subgroupoid.IsThin : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → Prop
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.quotIntNorm_apply : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  NumberField.mixedEmbedding.fundamentalCone.quotIntNorm ⟦a⟧ = NumberField.mixedEmbedding.fundamentalCone.intNorm a
-- Mathlib.GroupTheory.Perm.Fin
/-- The set of all permutations of `Fin (n + 1)` can be constructed by augmenting the set of
permutations of `Fin n` by each element of `Fin (n + 1)` in turn.  -/
Finset.univ_perm_fin_succ : ∀ {n : ℕ}, Finset.univ = Finset.map Equiv.Perm.decomposeFin.symm.toEmbedding Finset.univ
-- Init.Notation
/-- `p1 <|> p2` is shorthand for `orelse(p1, p2)`, and parses either `p1` or `p2`.
It does not backtrack, meaning that if `p1` consumes at least one token then
`p2` will not be tried. Therefore, the parsers should all differ in their first
token. The `atomic(p)` parser combinator can be used to locally backtrack a parser.
(For full backtracking, consider using extensible syntax classes instead.)

On success, if the inner parser does not generate exactly one node, it will be
automatically wrapped in a `group` node, so the result will always be arity 1.

The `<|>` combinator does not generate a node of its own, and in particular
does not tag the inner parsers to distinguish them, which can present a problem
when reconstructing the parse. A well formed `<|>` parser should use disjoint
node kinds for `p1` and `p2`.
 -/
«stx_<|>_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.zero_right : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M} (x : M), (B x) 0 = 0
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.mk : {G : Type u_1} →
  [inst : Group G] →
    (toSubgroup : Subgroup G) →
      autoParam toSubgroup.Normal FiniteIndexNormalSubgroup.isNormal'._autoParam →
        autoParam toSubgroup.FiniteIndex FiniteIndexNormalSubgroup.isFiniteIndex'._autoParam →
          FiniteIndexNormalSubgroup G
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- The 0th face of a 2-simplex, as a morphism in the 2-truncated simplex category.  -/
SSet.Truncated.δ0₂ : { obj := { len := 1 }, property := SSet.Truncated.ι0₂._proof_5 } ⟶
  { obj := { len := 2 }, property := SSet.Truncated.ι0₂._proof_3 }
-- Mathlib.Topology.NhdsKer
IsOpen.nhdsKer_subset : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, IsOpen t → (nhdsKer s ⊆ t ↔ s ⊆ t)
-- Mathlib.Algebra.Group.Hom.Defs
instInhabitedAddMonoidHom : {M : Type u_4} → {N : Type u_5} → [inst : AddZero M] → [inst_1 : AddZeroClass N] → Inhabited (M →+ N)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eq_getEntry? : ∀ {α : Type u} {β : Type v} [inst : BEq α] {l : List ((_ : α) × β)} {a : α},
  Std.Internal.List.getValue? a l = Option.map (fun x => x.snd) (Std.Internal.List.getEntry? a l)
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function, then the kernel of
`seminormFromBounded' f` equals the kernel of `f`.  -/
seminormFromBounded_ker : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f → (∀ (x y : R), f (x * y) ≤ c * f x * f y) → seminormFromBounded' f ⁻¹' {0} = f ⁻¹' {0}
-- Mathlib.Algebra.Group.Action.Defs
VAddAssocClass.left : ∀ (M : Type u_1) {α : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M α], VAddAssocClass M M α
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_rco_eq_nil : ∀ {m n : ℤ}, n ≤ m → (m...n).toList = []
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitMul.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  MonCat.FilteredColimits.colimitMul F =
    { mul := fun x y => Quot.lift₂ (MonCat.FilteredColimits.colimitMulAux F) ⋯ ⋯ x y }
-- Mathlib.MeasureTheory.Measure.Dirac
/-- The sum of scaled Dirac measures applied to a singleton is the coefficient of that singleton.  -/
MeasureTheory.Measure.sum_smul_dirac_singleton : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {f : α → ENNReal} {a : α},
  (MeasureTheory.Measure.sum fun b => f b • MeasureTheory.Measure.dirac b) {a} = f a
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
/-- See `eLpNorm_smul_measure_of_ne_top'` for a version with scalar multiplication by `ℝ≥0`.  -/
MeasureTheory.eLpNorm_smul_measure_of_ne_top : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ContinuousENorm ε] {p : ENNReal},
  p ≠ ⊤ →
    ∀ (f : α → ε) (c : ENNReal), MeasureTheory.eLpNorm f p (c • μ) = c ^ (1 / p).toReal • MeasureTheory.eLpNorm f p μ
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.Nondegenerate.ofSeparatingRight : ∀ {R₂ : Type u_3} {M₂ : Type u_4} [inst : CommRing R₂] [inst_1 : AddCommGroup M₂] [inst_2 : Module R₂ M₂] [IsDomain R₂]
  [Module.Free R₂ M₂] [Module.Finite R₂ M₂] {B : LinearMap.BilinForm R₂ M₂},
  LinearMap.SeparatingRight B → B.Nondegenerate
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_erase! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF →
    ∀ {k a : α},
      Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.erase! k t) a =
        if compare k a = Ordering.eq then default else Std.DTreeMap.Internal.Impl.Const.get! t a
-- Init.Data.UInt.Lemmas
UInt8.toUInt16_neg : ∀ (a : UInt8), (-a).toUInt16 = -a.toUInt16 % 256
-- Mathlib.RingTheory.FiniteType
/-- Any commutative ring `R` satisfies the `OrzechProperty`, that is, for any finitely generated
`R`-module `M`, any surjective homomorphism `f : N →ₗ[R] M` from a submodule `N` of `M` to `M`
is injective.

This is a consequence of Noetherian case
(`IsNoetherian.injective_of_surjective_of_injective`), which requires that `M` is a
Noetherian module, but allows `R` to be non-commutative. The reduction of this result to
Noetherian case is adapted from <https://math.stackexchange.com/a/1066110>:
suppose `{ m_j }` is a finite set of generators of `M`, for any `n : N` one can write
`i n = ∑ j, b_j * m_j` for `{ b_j }` in `R`, here `i : N →ₗ[R] M` is the standard inclusion.
We can choose `{ n_j }` which are preimages of `{ m_j }` under `f`, and can choose
`{ c_jl }` in `R` such that `i n_j = ∑ l, c_jl * m_l` for each `j`.
Now let `A` be the subring of `R` generated by `{ b_j }` and `{ c_jl }`, then it is
Noetherian. Let `N'` be the `A`-submodule of `N` generated by `n` and `{ n_j }`,
`M'` be the `A`-submodule of `M` generated by `{ m_j }`,
then it's easy to see that `i` and `f` restrict to `N' →ₗ[A] M'`,
and the restricted version of `f` is surjective, hence by Noetherian case,
it is also injective, in particular, if `f n = 0`, then `n = 0`.

See also Orzech's original paper: *Onto endomorphisms are isomorphisms* [orzech1971].

This implies that nontrivial commutative rings satisfy the strong rank condition:
see `strongRankCondition_of_orzechProperty` in `Mathlib.LinearAlgebra.InvariantBasisNumber`.
A shortcut instance `commRing_strongRankCondition` is also provided.
 -/
CommRing.orzechProperty : ∀ (R : Type u_1) [inst : CommRing R], OrzechProperty R
-- Mathlib.Topology.UniformSpace.Cauchy
Filter.TotallyBounded.totallyBounded_setOfPred_clusterPt : ∀ {α : Type u} [uniformSpace : UniformSpace α] {f : Filter α}, f.TotallyBounded → TotallyBounded {x | ClusterPt x f}
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.head_cons : ∀ {α : Type u} (a : α) (s : Stream'.WSeq α), (Stream'.WSeq.cons a s).head = Computation.pure (some a)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.pointReflection_self : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (x : P₁), (AffineEquiv.pointReflection k x) x = x
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Functor.Monoidal.whiskeringLeft_η_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u_1) [inst_2 : CategoryTheory.Category.{v_1, u_1} E] [inst_3 : CategoryTheory.MonoidalCategory E]
  (F : CategoryTheory.Functor C D) (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.η ((CategoryTheory.Functor.whiskeringLeft C D E).obj F)).app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit E)
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- Eta-expanded form of `DifferentiableOn.const_smul` -/
DifferentiableOn.fun_const_smul : ∀ {𝕜 : 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}
  {s : Set E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F], DifferentiableOn 𝕜 f s → ∀ (c : R), DifferentiableOn 𝕜 (fun i => c • f i) s
-- Mathlib.Data.Set.Finite.Basic
Set.finite_def : ∀ {α : Type u} {s : Set α}, s.Finite ↔ Nonempty (Fintype ↑s)
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.bot_ringCon : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R], ⊥.ringCon = ⊥
-- Mathlib.Topology.MetricSpace.Basic
/-- A metric space induces an emetric space  -/
MetricSpace.toEMetricSpace : {γ : Type w} → [MetricSpace γ] → EMetricSpace γ
-- Lean.Language.Basic
/-- Runs a tree of snapshots to conclusion and incrementally report messages on stdout. Messages are
reported in tree preorder. Returns whether any errors were reported.
This function is used by the cmdline driver; see `Lean.Server.FileWorker.reportSnapshots` for how
the language server reports snapshots asynchronously.   -/
Lean.Language.SnapshotTree.runAndReport : Lean.Language.SnapshotTree →
  Lean.Options → optParam Bool false → optParam (Lean.NameMap Lean.MessageSeverity) ∅ → IO Bool