mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_const : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] {C : ε'},
  autoParam (μ s ≠ ⊤) MeasureTheory.integrableOn_const._auto_1 →
    autoParam (‖C‖ₑ ≠ ⊤) MeasureTheory.integrableOn_const._auto_3 → MeasureTheory.IntegrableOn (fun x => C) s μ
-- Mathlib.RingTheory.TensorProduct.Maps
/-- The natural `A`-algebra homomorphism $A ⊗ (\text{End}_R M) → \text{End}_A (A ⊗ M)$,
where `M` is an `R`-module, and `A` an `R`-algebra.  -/
LinearMap.tensorProductEnd : (R : Type u_1) →
  (A : Type u_2) →
    (M : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module R M] → TensorProduct R A (Module.End R M) →ₐ[A] Module.End A (TensorProduct R A M)
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- The restriction of a continuous intertwining map along a monoid homomorphism.  -/
ContIntertwiningMap.restrict : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {H : Type u_6} →
                              [inst_10 : Monoid H] →
                                {π : ContRepresentation R G V} →
                                  {π' : ContRepresentation R G W} →
                                    (φ : H →* G) →
                                      ContIntertwiningMap π π' → ContIntertwiningMap (π.restrict φ) (π'.restrict φ)
-- Init.Tactics
/-- `simp?` takes the same arguments as `simp`, but reports an equivalent call to `simp only`
that would be sufficient to close the goal. This is useful for reducing the size of the simp
set in a local invocation to speed up processing.
```
example (x : Nat) : (if True then x + 2 else 3) = x + 2 := by
  simp? -- prints "Try this: simp only [ite_true]"
```

This command can also be used in `simp_all` and `dsimp`.
 -/
Lean.Parser.Tactic.tacticSimp?!_ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.mem_sSup_of_mem : ∀ {G : Type u_1} [inst : Group G] {S : Set (Subgroup G)} {s : Subgroup G}, s ∈ S → ∀ {x : G}, x ∈ s → x ∈ sSup S
-- Mathlib.CategoryTheory.Quotient.Linear
/-- Auxiliary definition for `Quotient.Linear.module`.  -/
CategoryTheory.Quotient.Linear.module' : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear R C] →
            (r : HomRel C) →
              [CategoryTheory.Congruence r] →
                (∀ (a : R) ⦃X Y : C⦄ (f₁ f₂ : X ⟶ Y), r f₁ f₂ → r (a • f₁) (a • f₂)) →
                  [inst_5 : CategoryTheory.Preadditive (CategoryTheory.Quotient r)] →
                    [(CategoryTheory.Quotient.functor r).Additive] →
                      (X Y : C) →
                        Module R ((CategoryTheory.Quotient.functor r).obj X ⟶ (CategoryTheory.Quotient.functor r).obj Y)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F : C ⥤ D` preserves
limits of `K : J ⥤ C`.  -/
CategoryTheory.Limits.preservesLimit_of_op : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesColimit K.op F.op],
  CategoryTheory.Limits.PreservesLimit K F
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_mul_cancel : ∀ {a b : Ordinal.{u_4}}, a ≠ 0 → a ∣ b → a * (b / a) = b
-- Lean.Parser.Basic
Lean.Parser.sepByFn : Bool → Lean.Parser.ParserFn → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Init.Data.String.Lemmas.Splits
_private.Init.Data.String.Lemmas.Splits.0.String.Pos.Splits.rotateLeft.eq_1 : ∀ {s : String} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits (t₁ ++ t₂) t₃),
  h.rotateLeft = String.Pos.ofToSlice ⋯.rotateLeft
-- Init.Data.Iterators.Basic
Std.Iter.isPlausibleSuccessorOf_eq_invImage : ∀ {α β : Type w} [inst : Std.Iterator α Id β],
  Std.Iter.IsPlausibleSuccessorOf = InvImage Std.IterM.IsPlausibleSuccessorOf Std.Iter.toIterM
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.rankFinite_or_rankInfinite : ∀ {α : Type u_1} (M : Matroid α), M.RankFinite ∨ M.RankInfinite
-- Std.Data.HashMap.Lemmas
Std.HashMap.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {a : α}, (m.getKey? a).isSome = m.contains a
-- Init.Data.String.Basic
String.Pos.get_toSlice : ∀ {s : String} {p : s.Pos} {h : p.toSlice ≠ s.toSlice.endPos}, p.toSlice.get h = p.get ⋯
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- The Gelfand─Naimark─Segal (GNS) space constructed from a positive linear functional on a
non-unital C⋆-algebra. This is a type synonym of `A`.

This space is only a pre-inner product space. Its Hilbert space completion is
`PositiveLinearMap.GNS`.  -/
PositiveLinearMap.PreGNS : {A : Type u_1} → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → (A →ₚ[ℂ] ℂ) → Type u_1
-- Mathlib.Order.WithBot
WithBot.unbotD_bot : ∀ {α : Type u_5} (d : α), WithBot.unbotD d ⊥ = d
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
MulEquiv.toHomeomorph_toContinuousMulEquiv : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Mul G] [inst_3 : Mul H]
  {e : G ≃* H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s), ↑(e.toContinuousMulEquiv he) = e.toHomeomorph he
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_union_of_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Mathlib.Algebra.Order.Group.Abs
abs_sub_nonpos : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G}, |a - b| ≤ 0 ↔ a = b
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.Measure.le_mkMetric : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (m : ENNReal → ENNReal)
  (μ : MeasureTheory.Measure X) (ε : ENNReal),
  0 < ε → (∀ (s : Set X), Metric.ediam s ≤ ε → μ s ≤ m (Metric.ediam s)) → μ ≤ MeasureTheory.Measure.mkMetric m
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit_log2 : ∀ {n : ℕ}, n ≠ 0 → n.testBit n.log2 = true
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.restrictNonposSeq.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.List.Lemmas
List.append_eq_singleton_iff : ∀ {α : Type u_1} {a b : List α} {x : α}, a ++ b = [x] ↔ a = [] ∧ b = [x] ∨ a = [x] ∧ b = []
-- Mathlib.Order.Types.Defs
OrderType.not_lt_zero : ∀ {o : OrderType.{u_1}}, ¬o < 0
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.hasProjectiveDimensionLT_of_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X X' : C} (e : X ≅ X')
  (n : ℕ) [CategoryTheory.HasProjectiveDimensionLT X n], CategoryTheory.HasProjectiveDimensionLT X' n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.exp_pi_mul_I : Complex.exp (↑Real.pi * Complex.I) = -1
-- Mathlib.FieldTheory.Separable
Polynomial.separable_X : ∀ {R : Type u} [inst : CommSemiring R], Polynomial.X.Separable
-- Mathlib.RingTheory.MvPolynomial.Localization
_private.Mathlib.RingTheory.MvPolynomial.Localization.0.IsLocalization.Away.auxInv_auxHom : ∀ {R : Type u_2} [inst : CommRing R] (S : Type u_3) [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S],
  (IsLocalization.Away.auxInv✝ S r).comp (IsLocalization.Away.auxHom✝ S r).toRingHom =
    RingHom.id (MvPolynomial Unit R ⧸ Ideal.span {MvPolynomial.C r * MvPolynomial.X () - 1})
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.hom_comp_ι : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s t : CategoryTheory.Limits.Fork f g}
  (f_1 : s ⟶ t), CategoryTheory.CategoryStruct.comp f_1.hom t.ι = s.ι
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {X : C} →
          [toBimonObj : CategoryTheory.BimonObj X] →
            (antipode : X ⟶ X) →
              autoParam
                  (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                      (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerRight antipode X) CategoryTheory.MonObj.mul) =
                    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one)
                  CategoryTheory.HopfObj.antipode_left._autoParam →
                autoParam
                    (CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
                        (CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X antipode) CategoryTheory.MonObj.mul) =
                      CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one)
                    CategoryTheory.HopfObj.antipode_right._autoParam →
                  CategoryTheory.HopfObj X
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.mk.injEq : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (toSubmodule : Submodule R L)
  (lie_mem' : ∀ {x y : L}, x ∈ toSubmodule.carrier → y ∈ toSubmodule.carrier → ⁅x, y⁆ ∈ toSubmodule.carrier)
  (toSubmodule_1 : Submodule R L)
  (lie_mem'_1 : ∀ {x y : L}, x ∈ toSubmodule_1.carrier → y ∈ toSubmodule_1.carrier → ⁅x, y⁆ ∈ toSubmodule_1.carrier),
  ({ toSubmodule := toSubmodule, lie_mem' := lie_mem' } = { toSubmodule := toSubmodule_1, lie_mem' := lie_mem'_1 }) =
    (toSubmodule = toSubmodule_1)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Nat.iterate.match_1.eq_2 : ∀ {α : Sort u_2} (motive : ℕ → α → Sort u_1) (k : ℕ) (a : α) (h_1 : (a : α) → motive 0 a)
  (h_2 : (k : ℕ) → (a : α) → motive k.succ a),
  (match k.succ, a with
    | 0, a => h_1 a
    | k.succ, a => h_2 k a) =
    h_2 k a
-- Mathlib.Order.Lattice
Prod.instLattice : (α : Type u) → (β : Type v) → [Lattice α] → [Lattice β] → Lattice (α × β)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.instIsIsoAppToRightDerivedZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasInjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C), CategoryTheory.IsIso (F.toRightDerivedZero.app X)
-- Mathlib.Combinatorics.Enumerative.DyckWord
instDecidableEqDyckStep : DecidableEq DyckStep
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.const.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.CategoryTheory.HomCongr
CategoryTheory.Functor.map_isoCongr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  (F : CategoryTheory.Functor C D) {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (f : X ≅ Y),
  F.mapIso ((α.isoCongr β) f) = ((F.mapIso α).isoCongr (F.mapIso β)) (F.mapIso f)
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgString : Lean.Doc.FromDocArg String
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X₀ : C) (succ : C → C) (toSucc : (X : C) → X ⟶ succ X)
  (X₀_1 : C) (succ_1 : C → C) (toSucc_1 : (X : C) → X ⟶ succ_1 X),
  ({ X₀ := X₀, succ := succ, toSucc := toSucc } = { X₀ := X₀_1, succ := succ_1, toSucc := toSucc_1 }) =
    (X₀ = X₀_1 ∧ succ = succ_1 ∧ toSucc ≍ toSucc_1)
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_sup_right : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q₁ q₂ : Submodule R N),
  Submodule.map₂ f p (q₁ ⊔ q₂) = Submodule.map₂ f p q₁ ⊔ Submodule.map₂ f p q₂
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.lhom_ext'_iff : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  {α : Type u_6} [inst_3 : Module R M] [inst_4 : Module R N] {φ ψ : SkewMonoidAlgebra M α →ₗ[R] N},
  φ = ψ ↔ ∀ (a : α), φ ∘ₗ SkewMonoidAlgebra.lsingle R a = ψ ∘ₗ SkewMonoidAlgebra.lsingle R a
-- Lean.Parser.Command
Lean.Parser.Command.coinductive.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Elab.DeclModifiers
Lean.Elab.RecKind.partial : Lean.Elab.RecKind
-- Init.Data.Range.Polymorphic.Basic
Std.Roi.lower_le_of_mem : ∀ {α : Type u} {r : Std.Roi α} {a : α} [inst : LT α], a ∈ r → r.lower < a
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_mul_monomial : ∀ {R : Type u} [inst : Semiring R] (n m : ℕ) (r s : R),
  (Polynomial.monomial n) r * (Polynomial.monomial m) s = (Polynomial.monomial (n + m)) (r * s)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.embDomain_mk_coeff : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  {f : Γ → Γ'} (hfi : Function.Injective f) (hf : ∀ (g g' : Γ), f g ≤ f g' ↔ g ≤ g') {x : HahnSeries Γ R} {a : Γ},
  (HahnSeries.embDomain { toFun := f, inj' := hfi, map_rel_iff' := ⋯ } x).coeff (f a) = x.coeff a
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_eq_false_of_isEmpty_erase_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).isEmpty = false → t.isEmpty = false
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeRevM?.find.eq_2 : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m (Option β)) (as : Array α) (i_1 : ℕ)
  (h : i_1 + 1 ≤ as.size),
  Array.findSomeRevM?.find✝ f as i_1.succ h = do
    let r ← f as[i_1]
    match r with
      | some val => pure r
      | none =>
        have this := ⋯;
        Array.findSomeRevM?.find✝ f as i_1 this
-- Lean.Parser.Do
/-- `dbg_trace e` prints `e` (which can be an interpolated string literal) to stderr.
It should only be used for debugging.
 -/
Lean.Parser.Term.doDbgTrace : Lean.Parser.Parser
-- Lean.Parser.Command
/-- `declModifiers` is the collection of modifiers on a declaration:
* a doc comment `/-- ... -/`
* a list of attributes `@[attr1, attr2]`
* a visibility specifier, `private` or `public`
* `protected`
* `noncomputable`
* `unsafe`
* `partial` or `nonrec`

All modifiers are optional, and have to come in the listed order.

`nestedDeclModifiers` is the same as `declModifiers`, but attributes are printed
on the same line as the declaration. It is used for declarations nested inside other syntax,
such as inductive constructors, structure projections, and `let rec` / `where` definitions.  -/
Lean.Parser.Command.declModifiersF : Lean.Parser.Parser
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.localizationAway_σ : ∀ {R : Type u} (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (r : R)
  [inst_3 : IsLocalization.Away r S] (s : S),
  (Algebra.Generators.localizationAway S r).σ s =
    MvPolynomial.C (IsLocalization.Away.sec r s).1 * MvPolynomial.X () ^ (IsLocalization.Away.sec r s).2
-- Lean.Elab.MutualDef
/-- If `body` allows for incremental tactic reporting and reuse, creates a snapshot task out of the
passed promise with appropriate range, otherwise immediately resolves the promise to a dummy
value.
 -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.elabHeaders.mkTacTask : Lean.Syntax →
  IO.Promise Lean.Elab.Tactic.TacticParsedSnapshot →
    Lean.Elab.TermElabM (Option Lean.Syntax × Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot))
-- Mathlib.MeasureTheory.Function.ConditionalLExpectation
/-- Conditional (Lebesgue) expectation of a function, with notation `P⁻[X|mΩ]`.

It is defined as `0` if either `¬ mΩ ≤ mΩ₀` or `hm : mΩ ≤ mΩ₀` but `¬ SigmaFinite (P.trim hm)`.

One should typically not use the definition directly.
 -/
MeasureTheory.«term__⁻[_|_]» : Lean.TrailingParserDescr
-- Mathlib.Data.Matrix.Basic
Matrix.transposeAlgEquiv_apply : ∀ (m : Type u_2) (R : Type u_7) (α : Type u_11) [inst : CommSemiring R] [inst_1 : CommSemiring α] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] [inst_4 : Algebra R α] (a : Matrix m m α),
  (Matrix.transposeAlgEquiv m R α) a = MulOpposite.op a.transpose
-- Mathlib.Analysis.Complex.Norm
Complex.norm_pow : ∀ (z : ℂ) (n : ℕ), ‖z ^ n‖ = ‖z‖ ^ n
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.instUniqueOfIsEmpty : {α : Type u_1} → [inst : TopologicalSpace α] → [IsEmpty α] → Unique (TopologicalSpace.Compacts α)
-- Lean.DocString.Extension
_private.Lean.DocString.Extension.0.Lean.VersoModuleDocs.DocContext.close : Lean.VersoModuleDocs.DocContext✝ → Except String Lean.VersoModuleDocs.DocContext✝
-- Lean.Expr
/-- Maps `f` on each immediate child of the given expression.  -/
Lean.Expr.traverseChildren : {M : Type → Type u_1} → [Applicative M] → (Lean.Expr → M Lean.Expr) → Lean.Expr → M Lean.Expr
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_ofReal_pow : ∀ {K : Type u_1} [inst : RCLike K] (a : ℝ) (n : ℕ), RCLike.re (↑a ^ n) = a ^ n
-- Aesop.RuleSet
/-- The simp theorems used by the builtin norm simp rule.
 -/
Aesop.LocalRuleSet.simpTheoremsArray : Aesop.LocalRuleSet → Array (Lean.Name × Lean.Meta.SimpTheorems)
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.opensRange.eq_1 : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f],
  AlgebraicGeometry.Scheme.Hom.opensRange f = { carrier := Set.range ⇑f, is_open' := ⋯ }
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.one_mem_valueMonoid : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B), 1 ∈ f.valueMonoid
-- Init.Data.String.Defs
String.instDecidableLtPos : {s : String} → (l r : s.Pos) → Decidable (l < r)
-- Mathlib.Analysis.Convex.StrictConvexSpace
StrictConvexSpace.of_norm_combo_ne_one : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ (x y : E), ‖x‖ = 1 → ‖y‖ = 1 → x ≠ y → ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ ‖a • x + b • y‖ ≠ 1) →
    StrictConvexSpace ℝ E
-- Mathlib.Geometry.Manifold.Notation
/-- `CMDiffAt[s] n f x` elaborates to `ContMDiffWithinAt I J n f s x`,
trying to determine `I` and `J` from the local context.
`n` is coerced to `WithTop ℕ∞` if necessary (so passing a `ℕ`, `∞` or `ω` are all supported).
The argument `x` can be omitted.  -/
Manifold.«termCMDiffAt[_]____» : Lean.ParserDescr
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R),
  p.support =
    Finset.map { toFun := ⇑Multiplicative.toAdd, inj' := SkewPolynomial.support._proof_1 } (SkewMonoidAlgebra.support p)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- The spectral value of `p` equals zero if and only if `p` is of the form `X ^ n`.  -/
spectralValue_eq_zero_iff : ∀ {R : Type u_1} [inst : NormedRing R] [Nontrivial R] {p : Polynomial R},
  p.Monic → (spectralValue p = 0 ↔ p = Polynomial.X ^ p.natDegree)
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_hasFDerivAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G} {f' : G →L[𝕜] E},
  HasFDerivAt (⇑iso ∘ f) (↑iso ∘SL f') x ↔ HasFDerivAt f f' x
-- Mathlib.CategoryTheory.Simple
/-- A nonzero monomorphism to a simple object is an isomorphism.  -/
CategoryTheory.isIso_of_mono_of_nonzero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  [CategoryTheory.Simple Y] {f : X ⟶ Y} [CategoryTheory.Mono f], f ≠ 0 → CategoryTheory.IsIso f
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.val_mk' : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  (x : Invertible A.det), ↑(Matrix.GeneralLinearGroup.mk' A x) = A
-- Init.Grind.Ring.CommSemiringAdapter
_private.Init.Grind.Ring.CommSemiringAdapter.0.Lean.Grind.CommRing.Expr.denoteS.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (k : ℕ) (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (v : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var v))
  (h_4 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b))
  (h_6 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k))
  (h_7 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b)) (h_8 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_9 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k)),
  (match Lean.Grind.CommRing.Expr.natCast k with
    | Lean.Grind.CommRing.Expr.num k => h_1 k
    | Lean.Grind.CommRing.Expr.natCast k => h_2 k
    | Lean.Grind.CommRing.Expr.var v => h_3 v
    | a.add b => h_4 a b
    | a.mul b => h_5 a b
    | a.pow k => h_6 a k
    | a.sub b => h_7 a b
    | a.neg => h_8 a
    | Lean.Grind.CommRing.Expr.intCast k => h_9 k) =
    h_2 k
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
/-- The **Gagliardo-Nirenberg-Sobolev inequality**.  Let `u` be a continuously differentiable
function `u` supported in a bounded set `s` in a normed space `E` of finite dimension
`n`, equipped with Haar measure, and let `1 < p < n`.
Then the `Lᵖ` norm of `u` is bounded above by a constant times the `Lᵖ` norm of
the Fréchet derivative of `u`.

Note: The codomain of `u` needs to be a finite-dimensional normed space.
 -/
MeasureTheory.eLpNorm_le_eLpNorm_fderiv : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {E : Type u_4} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E] [inst_6 : FiniteDimensional ℝ E]
  (μ : MeasureTheory.Measure E) [inst_7 : μ.IsAddHaarMeasure] [inst_8 : FiniteDimensional ℝ F] {u : E → F} {s : Set E},
  ContDiff ℝ 1 u →
    Function.support u ⊆ s →
      ∀ {p : NNReal},
        1 ≤ p →
          p < ↑(Module.finrank ℝ E) →
            Bornology.IsBounded s →
              MeasureTheory.eLpNorm u (↑p) μ ≤
                ↑(MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ s p p) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ