mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_comp_add_left : ∀ {𝕜 : 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}
  {x : E} {s : Set E} (a : E), fderivWithin 𝕜 (fun x => f (a + x)) s x = fderivWithin 𝕜 f (a +ᵥ s) (a + x)
-- Mathlib.Algebra.BigOperators.Ring.Finset
/-- `∏ i, (f i - g i) = (∏ i, f i) - ∑ i, g i * (∏ j < i, f j - g j) * (∏ j > i, f j)`.  -/
Finset.prod_sub_ordered : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommRing R] [inst_1 : LinearOrder ι] (s : Finset ι) (f g : ι → R),
  ∏ i ∈ s, (f i - g i) = ∏ i ∈ s, f i - ∑ i ∈ s, (g i * ∏ j ∈ s with j < i, (f j - g j)) * ∏ j ∈ s with i < j, f j
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
map_le_nonZeroDivisors_of_injective : ∀ {F : Type u_1} {M₀ : Type u_2} {M₀' : Type u_3} [inst : MonoidWithZero M₀] [inst_1 : MonoidWithZero M₀']
  [inst_2 : FunLike F M₀ M₀'] [NoZeroDivisors M₀'] [inst_4 : MonoidWithZeroHomClass F M₀ M₀'] (f : F),
  Function.Injective ⇑f → ∀ {S : Submonoid M₀}, S ≤ nonZeroDivisors M₀ → Submonoid.map f S ≤ nonZeroDivisors M₀'
-- Mathlib.Order.Filter.Basic
Filter.GenerateSets.below : {α : Type u} →
  {g : Set (Set α)} →
    {motive : (a : Set α) → Filter.GenerateSets g a → Prop} → {a : Set α} → Filter.GenerateSets g a → Prop
-- Mathlib.SetTheory.Lists
/-- Converts a ZFA prelist to a `List` of ZFA lists. Atoms are sent to `[]`.  -/
Lists'.toList : {α : Type u_1} → {b : Bool} → Lists' α b → List (Lists α)
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.LaxBraidedFunctor.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {D : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} D] →
            [inst_4 : CategoryTheory.MonoidalCategory D] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (toFunctor : CategoryTheory.Functor C D) →
                  autoParam toFunctor.LaxBraided CategoryTheory.LaxBraidedFunctor.laxBraided._autoParam →
                    CategoryTheory.LaxBraidedFunctor C D
-- Mathlib.Analysis.InnerProductSpace.ProdL2
/-- If a subspace `K` of an inner product space `E` admits an orthogonal projection, then `E` is
isometrically isomorphic to the `L²` product of `K` and `Kᗮ`.  -/
Submodule.orthogonalDecomposition : {𝕜 : Type u_1} →
  {E : Type u_4} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          (K : Submodule 𝕜 E) → [K.HasOrthogonalProjection] → E ≃ₗᵢ[𝕜] WithLp 2 (↥K × ↥Kᗮ)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
/-- The second inclusion into the pushout of `f` and `g`.  -/
CategoryTheory.Limits.pushout.inr : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) → [inst_1 : CategoryTheory.Limits.HasPushout f g] → Z ⟶ CategoryTheory.Limits.pushout f g
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.restrict_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N) (V : Submodule R M) (v : ↥V),
  (Q.restrict V) v = Q ↑v
-- Mathlib.RingTheory.Congruence.Defs
/-- Two ring congruence relations are equal iff their underlying binary
relations are equal.  -/
RingCon.coe_inj : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {c d : RingCon R}, ⇑c = ⇑d ↔ c = d
-- Mathlib.Data.NNRat.Lemmas
NNRat.coe_indicator : ∀ {α : Type u_1} (s : Set α) (f : α → ℚ≥0) (a : α), ↑(s.indicator f a) = s.indicator (fun x => ↑(f x)) a
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getCast! : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [LawfulBEq α] → (a : α) → [Inhabited (β a)] → Std.DHashMap.Internal.AssocList α β → β a
-- Mathlib.Analysis.FunctionalSpaces.SobolevInequality
ContinuousLinearEquiv.ofFinrankEq.congr_simp : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F : Type w}
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜 F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousSMul 𝕜 F] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : T2Space F]
  [inst_13 : FiniteDimensional 𝕜 E] [inst_14 : FiniteDimensional 𝕜 F] (cond : Module.finrank 𝕜 E = Module.finrank 𝕜 F),
  ContinuousLinearEquiv.ofFinrankEq cond = ContinuousLinearEquiv.ofFinrankEq cond
-- Lean.Elab.DefView
Lean.Elab.DefsParsedSnapshot.mk : Lean.Language.Snapshot → Array Lean.Elab.DefParsed → Lean.Elab.DefsParsedSnapshot
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.natTrans_hcomp_injective : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] {F G : CategoryTheory.Functor W.Localization D} {τ₁ τ₂ : F ⟶ G},
  CategoryTheory.CategoryStruct.id W.Q ◫ τ₁ = CategoryTheory.CategoryStruct.id W.Q ◫ τ₂ → τ₁ = τ₂
-- Std.Data.DTreeMap.Internal.Operations
/-- Transforms an array of mappings into a tree map.  -/
Std.DTreeMap.Internal.Impl.Const.unitOfList : {α : Type u} → [Ord α] → List α → Std.DTreeMap.Internal.Impl α fun x => Unit
-- Mathlib.CategoryTheory.Square
/-- The functor `Arrow (Arrow C) ⥤ Square C` which sends
a morphism `Arrow.mk f ⟶ Arrow.mk g` to the commutative square
with `f` on the left side and `g` on the right side.  -/
CategoryTheory.Square.fromArrowArrowFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor (CategoryTheory.Arrow (CategoryTheory.Arrow C)) (CategoryTheory.Square C)
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The inclusion functor
`HomotopyCategory.ι C : HomotopyCategory.Plus C ⥤ HomotopyCategory C (.up ℤ)` is fully faithful.  -/
HomotopyCategory.Plus.fullyFaithfulι : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (HomotopyCategory.Plus.ι C).FullyFaithful
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.one_lt_rpow_of_pos_of_lt_one_of_neg : ∀ {x : NNReal} {z : ℝ}, 0 < x → x < 1 → z < 0 → 1 < x ^ z
-- Mathlib.RingTheory.Valuation.Integers
Valuation.Integers.le_of_dvd : ∀ {R : Type u} {Γ₀ : Type v} [inst : CommRing R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀] {v : Valuation R Γ₀}
  {O : Type w} [inst_2 : CommRing O] [inst_3 : Algebra O R],
  v.Integers O → ∀ {x y : O}, x ∣ y → v ((algebraMap O R) y) ≤ v ((algebraMap O R) x)
-- Mathlib.AlgebraicTopology.SimplicialSet.Splitting
SSet.splitting_ι : ∀ (X : SSet) (n : ℕ), X.splitting.ι n = TypeCat.ofHom Subtype.val
-- Mathlib.Order.Hom.Basic
OrderHom.fst_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (self : α × β), OrderHom.fst self = self.1
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat.inj : ∀ {e : Lean.Expr} {natStructId : ℕ} {lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr} {e_1 : Lean.Expr}
  {natStructId_1 : ℕ} {lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat e natStructId lhs rhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCoreOfNat e_1 natStructId_1 lhs_1 rhs_1 →
    e = e_1 ∧ natStructId = natStructId_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Tactic.Tauto
/-- Config for the `tauto` tactic. Currently empty. TODO: add `closer` option.  -/
Mathlib.Tactic.Tauto.Config : Type
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `IsSubApply.sub_apply`. -/
sub_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Sub β}
  {inst_2 : Sub F} [self : IsSubApply F α β] (f g : F) (x : α), (f - g) x = f x - g x
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Whisker a 1-morphism to an extension.
```
  b
  △ \
  |   \ extension  △
f |     \          | unit
  |       ◿
  a - - - ▷ c - - - ▷ x
      g         h
```
 -/
CategoryTheory.Bicategory.LeftExtension.whisker : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          CategoryTheory.Bicategory.LeftExtension f g →
            {x : B} → (h : c ⟶ x) → CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Algebra.Group.Action.Defs
Function.Injective.smulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul N α] [inst_2 : SMul M β]
  [inst_3 : SMul N β] [SMulCommClass M N β] {f : α → β},
  Function.Injective f →
    (∀ (c : M) (x : α), f (c • x) = c • f x) → (∀ (c : N) (x : α), f (c • x) = c • f x) → SMulCommClass M N α
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `Cardinal.exists_ord_eq`.

---

There exists a well-order on `α` whose order type is exactly `ord #α`.  -/
Cardinal.ord_eq : ∀ (α : Type u_1), ∃ r, ∃ (x : IsWellOrder α r), (Cardinal.mk α).ord = Ordinal.type r
-- Mathlib.Algebra.Polynomial.HasseDeriv
Polynomial.hasseDeriv_mul : ∀ {R : Type u_1} [inst : Semiring R] (k : ℕ) (f g : Polynomial R),
  (Polynomial.hasseDeriv k) (f * g) =
    ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal k, (Polynomial.hasseDeriv ij.1) f * (Polynomial.hasseDeriv ij.2) g
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.Equivalent.refl : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Q : LinearMap.BilinForm R M), Q.Equivalent Q
-- Mathlib.Analysis.Fourier.Notation
FourierTransform.fourierEquiv_symm_apply : ∀ {R : Type u_5} {E : Type u_6} {F : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid E] [inst_2 : AddCommMonoid F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : FourierTransform E F] [inst_6 : FourierAdd E F]
  [inst_7 : FourierSMul R E F] [inst_8 : FourierTransformInv F E] [inst_9 : FourierPair E F]
  [inst_10 : FourierInvPair F E] (f : F), (FourierTransform.fourierEquiv R E).symm f = FourierTransformInv.fourierInv f
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.comp_toHom : ∀ {X Y Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).toHom = CategoryTheory.CategoryStruct.comp f.toHom g.toHom
-- Std.Time.Format.Modifier
Std.Time.ZoneName.noConfusionType : Sort v✝ → Std.Time.ZoneName → Std.Time.ZoneName → Sort v✝
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.size_filter_eq_size_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Bool},
  (Std.DHashMap.filter f m).size = m.size ↔
    ∀ (a : α) (h : a ∈ m), f (m.getKey a h) (Std.DHashMap.Const.get m a h) = true
-- Lean.Util.SCC
Lean.SCC.State.mk : {α : Type} →
  [inst : BEq α] → [inst_1 : Hashable α] → List α → ℕ → Std.HashMap α Lean.SCC.Data → List (List α) → Lean.SCC.State α
-- Batteries.Data.Float.Lemmas
_private.Batteries.Data.Float.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.eq_4 : ∀ (motive : Float.Model.UnpackedFloat → Sort u_1) (s : Float.Model.UnpackedFloat.Sign) (m : ℕ) (e : ℤ)
  (mantissa_pos : 0 < m) (h_1 : Unit → motive Float.Model.UnpackedFloat.notANumber)
  (h_2 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s))
  (h_3 : (s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s))
  (h_4 :
    (s : Float.Model.UnpackedFloat.Sign) →
      (m : ℕ) → (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)),
  (match Float.Model.UnpackedFloat.finite s m e mantissa_pos with
    | Float.Model.UnpackedFloat.notANumber => h_1 ()
    | Float.Model.UnpackedFloat.infinity s => h_2 s
    | Float.Model.UnpackedFloat.zero s => h_3 s
    | Float.Model.UnpackedFloat.finite s m e mantissa_pos => h_4 s m e mantissa_pos) =
    h_4 s m e mantissa_pos
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.laxMonoidalPi_ε : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  (F : (i : I) → CategoryTheory.Functor (D i) (C i)) [inst_4 : (i : I) → (F i).LaxMonoidal] (i : I),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Functor.pi F) i = CategoryTheory.Functor.LaxMonoidal.ε (F i)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.isRegular_of_smul_left_injective : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f]
  {m : M'}, (Function.Injective fun r => r • m) → ∀ (s : ↥S), IsRegular ↑s
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In an additive commutative monoid with multiplication,
`∑ i ∈ I, x i`, where each `x i` is a square, is a sum of squares.
 -/
IsSumSq.sum_isSquare : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Mul R] {ι : Type u_2} (I : Finset ι) {x : ι → R},
  (∀ i ∈ I, IsSquare (x i)) → IsSumSq (∑ i ∈ I, x i)
-- Lean.Setup
/-- Whether the module, by default, participates in the module system.
  Even if `false`, a module can still choose to participate by using
  `module` in its header.
   -/
Lean.ModuleSetup.isModule : Lean.ModuleSetup → Bool
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.coeff_mul_antidiag : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Add M] (x y : AddMonoidAlgebra R M) (m : M)
  (s : Finset (M × M)), (∀ {p : M × M}, p ∈ s ↔ p.1 + p.2 = m) → (x * y).coeff m = ∑ p ∈ s, x.coeff p.1 * y.coeff p.2
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.congr_set : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, ContinuousWithinAt f s x → s =ᶠ[nhds x] t → ContinuousWithinAt f t x
-- Init.Data.Range.Polymorphic.SInt
Int8.instRxcLawfulHasSize : Std.Rxc.LawfulHasSize Int8
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The odd kernel is continuous on `Ioi 0`.  -/
HurwitzZeta.continuousOn_oddKernel : ∀ (a : UnitAddCircle), ContinuousOn (HurwitzZeta.oddKernel a) (Set.Ioi 0)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Fintype.prod_strictMono' : ∀ {ι : Type u_1} {M : Type u_4} [inst : Fintype ι] [inst_1 : CommMonoid M] [inst_2 : PartialOrder M]
  [IsOrderedCancelMonoid M], StrictMono fun f => ∏ x, f x
-- Lean.ExtraModUses
/-- Dependency's module name.  -/
Lean.ExtraModUse.module : Lean.ExtraModUse → Lean.Name
-- Mathlib.Algebra.Group.Hom.Basic
/-- Given two monoid morphisms `f`, `g` to a commutative monoid, `f * g` is the monoid morphism
sending `x` to `f x * g x`.  -/
MonoidHom.mul : {M : Type u_2} → {N : Type u_3} → [inst : MulOneClass M] → [inst_1 : CommMonoid N] → Mul (M →* N)
-- Mathlib.RingTheory.Etale.Basic
/-- An `R`-algebra `A` is formally etale if both `Ω[A⁄R]` and `H¹(L_{A/R})` are zero.
For the infinitesimal lifting definition, see `FormallyEtale.iff_comp_bijective`.  -/
Algebra.FormallyEtale : (R : Type u) → (A : Type v) → [inst : CommRing R] → [inst_1 : CommRing A] → [Algebra R A] → Prop
-- Mathlib.RingTheory.Filtration
/-- The `sSup` of a family of `I.Filtration`s is an `I.Filtration`.  -/
Ideal.Filtration.instSupSet : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → SupSet (I.Filtration M)
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.Truncated.Path₁.ext : ∀ {X : SSet.Truncated 1} {n : ℕ} {x y : X.Path₁ n}, x.vertex = y.vertex → x.arrow = y.arrow → x = y
-- Mathlib.Algebra.GroupWithZero.Defs
CommMonoidWithZero.toCommMonoid : {M₀ : Type u_2} → [self : CommMonoidWithZero M₀] → CommMonoid M₀
-- Init.Data.Float.Model.Format.Valid
/-- If the bit vector encodes a `NaN`, then it is the canonical `NaN`.  -/
Float.Model.Format.Valid.eq_packedNaN : ∀ {spec : Float.Model.Format} {b : BitVec spec.numBits},
  spec.Valid b →
    Float.Model.UnpackedFloat.unpackExponent b = -1#spec.exponentBits →
      Float.Model.UnpackedFloat.unpackMantissa b ≠ 0#spec.mantissaBitsWithoutImplicit →
        b = Float.Model.UnpackedFloat.packedNaN spec
-- Mathlib.Order.Interval.Set.Defs
/-- `Ioc a b` is the left-open right-closed interval $(a, b]$.  -/
Set.Ioc : {α : Type u_1} → [Preorder α] → α → α → Set α
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
Group.mulLeftReflectLE_of_mulLeftMono : ∀ {N : Type u_2} [inst : Group N] [inst_1 : LE N] [MulLeftMono N], MulLeftReflectLE N
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.exists_lipschitzOnWith_of_isBounded : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {r r' : ℝ},
  ConcaveOn ℝ (Metric.ball x₀ r) f →
    r' < r → Bornology.IsBounded (f '' Metric.ball x₀ r) → ∃ K, LipschitzOnWith K f (Metric.ball x₀ r')
-- Init.Classical
Classical.not_iff : ∀ {a b : Prop}, ¬(a ↔ b) ↔ (¬a ↔ b)
-- Init.Data.Array.MinMax
List.min?_toArray : ∀ {α : Type u_1} [inst : Min α] {l : List α}, l.toArray.min? = l.min?
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.smulRight_apply : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ R) (z : M₂) (m : (i : ι) → M₁ i), (f.smulRight z) m = f m • z
-- Mathlib.Data.List.Induction
List.reverseRecOn_concat : ∀ {α : Type u_1} {motive : List α → Sort u_2} (x : α) (xs : List α) (nil : motive [])
  (append_singleton : (l : List α) → (a : α) → motive l → motive (l ++ [a])),
  List.reverseRecOn (xs ++ [x]) nil append_singleton = append_singleton xs x (List.reverseRecOn xs nil append_singleton)
-- Std.Time.Zoned.Database.PosixTz
_private.Std.Time.Zoned.Database.PosixTz.0.Std.Time.TimeZone.posixParseJulian0Spec : Std.Internal.Parsec.String.Parser Std.Time.TimeZone.TransitionSpec
-- Std.Internal.Do.WP.Basic
/-- Soundness of `Functor.map`: mapping `f` over `x` preserves the WP.  -/
Std.Internal.Do.WPMonad.map_le_wp_map : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type z} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {α β : Type u} (f : α → β)
  (x : m α) (post : β → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x (fun a => post (f a)) epost)
    (Std.Internal.Do.wp (f <$> x) post epost)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.coe_ofClass : ∀ {S : Type u_3} {M : Type u_4} [inst : Mul M] [inst_1 : SetLike S M] [inst_2 : MulMemClass S M] (s : S),
  ↑(Subsemigroup.ofClass s) = ↑s
-- Lean.DeclarationRange
Lean.addDeclarationRanges : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → Lean.DeclarationRanges → m Unit
-- Mathlib.Algebra.FreeMonoid.FreeSemigroup
FreeMonoid.equivWithOneFreeSemigroup_symm_apply : ∀ {α : Type u_1} (a : WithOne (FreeSemigroup α)),
  FreeMonoid.equivWithOneFreeSemigroup.symm a = (WithOne.lift FreeSemigroup.toFreeMonoid) a
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.Path.listL.match_1.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode.Path α → Sort u_2) (c : RBTree.RBColor) (parent : RBTree.RBNode.Path α) (v : α)
  (r : RBTree.RBNode α) (h_1 : Unit → motive RBTree.RBNode.Path.root)
  (h_2 :
    (c : RBTree.RBColor) →
      (parent : RBTree.RBNode.Path α) → (v : α) → (r : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent v r))
  (h_3 :
    (c : RBTree.RBColor) →
      (l : RBTree.RBNode α) →
        (v : α) → (parent : RBTree.RBNode.Path α) → motive (RBTree.RBNode.Path.right c l v parent)),
  (match RBTree.RBNode.Path.left c parent v r with
    | RBTree.RBNode.Path.root => h_1 ()
    | RBTree.RBNode.Path.left c parent v r => h_2 c parent v r
    | RBTree.RBNode.Path.right c l v parent => h_3 c l v parent) =
    h_2 c parent v r
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α] {l : List α}
  {k k' : α},
  (k == k') = true → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashSet.ofList l).get! k' = k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.forIn_eq_forIn_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.1 d) = forIn t.keys init f
-- Mathlib.FieldTheory.Finite.Extension
/-- Given any field extension of finite fields `l/k` of degree `n`, we have a non-unique
isomorphism between `l` and our chosen `Extension k p n`.  -/
FiniteField.algEquivExtension : (k : Type u_1) →
  [inst : Field k] →
    [inst_1 : Finite k] →
      (p : ℕ) →
        [inst_2 : Fact (Nat.Prime p)] →
          [inst_3 : CharP k p] →
            (n : ℕ) →
              [inst_4 : NeZero n] →
                (l : Type u_2) →
                  [inst_5 : Field l] →
                    [inst_6 : Algebra k l] → Module.finrank k l = n → l ≃ₐ[k] FiniteField.Extension k p n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula.0.tacticMap_simp : Lean.ParserDescr
-- Mathlib.Algebra.GroupWithZero.Center
Set.div_mem_centralizer₀ : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] {s : Set G₀} {a b : G₀},
  a ∈ s.centralizer → b ∈ s.centralizer → a / b ∈ s.centralizer
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
/-- For `m : AddContent C` sigma-sub-additive, finite on `C`, the `inducedOuterMeasure` given by `m`
coincides with `m` on `C`.  -/
MeasureTheory.AddContent.inducedOuterMeasure_eq : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent ENNReal C),
  m.IsSigmaSubadditive → s ∈ C → (MeasureTheory.inducedOuterMeasure (fun x x_1 => m x) ⋯ ⋯) s = m s
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- The basis for `ℓ⁰(α, 𝕜)` given by `lp.single`.  -/
lp.zeroBasis : {𝕜 : Type u_1} → {α : Type u_3} → [inst : NormedRing 𝕜] → Module.Basis α 𝕜 ↥(lp (fun x => 𝕜) 0)
-- Mathlib.CategoryTheory.Opposites
/-- `Functor.unop` transforms identity functors to identity functors.  -/
CategoryTheory.Functor.unopId : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → (CategoryTheory.Functor.id Cᵒᵖ).unop ≅ CategoryTheory.Functor.id C
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitStatus.ready.inj : ∀ {numCases : ℕ} {isRec tryPostpone : Bool} {numCases_1 : ℕ} {isRec_1 tryPostpone_1 : Bool},
  Lean.Meta.Grind.SplitStatus.ready numCases isRec tryPostpone =
      Lean.Meta.Grind.SplitStatus.ready numCases_1 isRec_1 tryPostpone_1 →
    numCases = numCases_1 ∧ isRec = isRec_1 ∧ tryPostpone = tryPostpone_1
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableMul.measurable_const_mul : ∀ {M : Type u_2} {inst : MeasurableSpace M} {inst_1 : Mul M} [self : MeasurableMul M] (c : M), Measurable fun x => c * x
-- Mathlib.CategoryTheory.Category.RelCat
CategoryTheory.RelCat.instIsEquivalenceOppositeOpFunctor : CategoryTheory.RelCat.opFunctor.IsEquivalence
-- Mathlib.Order.Interval.Finset.Nat
Nat.card_Ioo : ∀ (a b : ℕ), (Finset.Ioo a b).card = b - a - 1
-- Init.Data.List.Find
List.findSome?_replicate_of_isNone : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  (f a).isNone = true → List.findSome? f (List.replicate n a) = none
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.tprod_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (e : γ ≃ β)
  (f : β → α), ∏' (c : γ), f (e c) = ∏' (b : β), f b