mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Abs
_private.Mathlib.Algebra.Order.Group.Abs.0.abs_add_eq_add_abs_le : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] {a b : G},
  a ≤ b → (|a + b| = |a| + |b| ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0)
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) (x : ↑S.cycles),
  (CategoryTheory.ConcreteCategory.hom S.moduleCatHomologyIso.hom)
      ((CategoryTheory.ConcreteCategory.hom S.homologyπ) x) =
    (CategoryTheory.ConcreteCategory.hom S.moduleCatLeftHomologyData.π)
      ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.hom) x)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_right_le_size_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₂.size ≤ (t₁ ∪ t₂).size
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.View.mk.inj : ∀ {α : Type u} {β : α → Type v} {size : ℕ} {k : α} {v : β k} {tree : Std.DTreeMap.Internal.Impl.Tree α β size} {k_1 : α}
  {v_1 : β k_1} {tree_1 : Std.DTreeMap.Internal.Impl.Tree α β size},
  { k := k, v := v, tree := tree } = { k := k_1, v := v_1, tree := tree_1 } → k = k_1 ∧ v ≍ v_1 ∧ tree = tree_1
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instDecidableEqFanin : DecidableEq Std.Sat.AIG.Fanin
-- Mathlib.Topology.Compactness.Compact
CompactSpace.nonempty_sInter : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X] {s : Set (Set X)},
  (∀ t ∈ s, IsClosed t) → (∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty) → (⋂₀ s).Nonempty
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
/-- Right whiskering of an oplax natural transformation and a modification.  -/
CategoryTheory.Oplax.OplaxTrans.whiskerRight : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            (η ⟶ θ) → (ι : G ⟶ H) → CategoryTheory.CategoryStruct.comp η ι ⟶ CategoryTheory.CategoryStruct.comp θ ι
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.of_nonpos_disjoint_union_eq_zero : ∀ {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {A B : Set α},
  Disjoint A B → MeasurableSet A → MeasurableSet B → s A ≤ 0 → s B ≤ 0 → s (A ∪ B) = 0 → s A = 0
-- Mathlib.Data.Finset.Sigma
Function.onFun.eq_1 : ∀ {α : Sort u₁} {β : Sort u₂} {φ : Sort u₃} (f : β → β → φ) (g : α → β) (x y : α),
  Function.onFun f g x y = f (g x) (g y)
-- Mathlib.AlgebraicTopology.SimplicialSet.Degenerate
SSet.Subcomplex.le_iff_contains_nonDegenerate : ∀ {X : SSet} (A B : X.Subcomplex),
  A ≤ B ↔
    ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (Opposite.op { len := n }) → ↑x ∈ B.obj (Opposite.op { len := n })
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toArray_rco : ∀ {m n : ℤ} {i : ℕ}, (m...n).toArray[i]? = if i < (n - m).toNat then some (m + ↑i) else none
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- Given a family of morphisms `f i : A i ⟶ B i` and a morphism `πX : X ⟶ S`,
this type parametrizes the commutative squares with a morphism `f i` on the left
and `πX` on the right.  -/
CategoryTheory.SmallObject.FunctorObjIndex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} → {A B : I → C} → ((i : I) → A i ⟶ B i) → {S X : C} → (X ⟶ S) → Type (max v w)
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.coeSeq : {α : Type u} → Coe (Stream'.Seq1 α) (Stream'.Seq α)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_empty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α],
  ∅.maxKey! = default
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq : ∀ {θ ψ : Real.Angle}, θ.sign = ψ.sign → (θ = ψ ↔ |θ.toReal| = |ψ.toReal|)
-- Mathlib.Topology.EMetricSpace.Lipschitz
locallyLipschitzOn_univ : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  LocallyLipschitzOn Set.univ f ↔ LocallyLipschitz f
-- Mathlib.Data.FunLike.Group
FunLike.divInvMonoid.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : One F]
  [inst_3 : Pow F ℕ] [inst_4 : Inv F] [inst_5 : Div F] [inst_6 : Pow F ℤ] [inst_7 : DivInvMonoid β]
  [inst_8 : IsOneApply F α β] [inst_9 : IsMulApply F α β] [inst_10 : IsInvApply F α β] [inst_11 : IsDivApply F α β]
  [inst_12 : IsPowApply ℕ F α β] [inst_13 : IsPowApply ℤ F α β],
  FunLike.divInvMonoid = Function.Injective.divInvMonoid (fun f => ⇑f) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerve.functorOfNerveMap_map : ∀ {C D : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  (φ :
    CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C) ⟶
      CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of D))
  {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.nerve.functorOfNerveMap φ).map f =
    CategoryTheory.nerve.homEquiv ((CategoryTheory.nerve.edgeMk f).toTruncated.map φ)
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
/-- Also see `not_dvd_discr_iff_forall_liesOver` for a slightly easier to prove RHS.  -/
NumberField.not_dvd_discr_iff_forall_mem : ∀ (K : Type u_1) (𝒪 : Type u_2) [inst : Field K] [inst_1 : NumberField K] [inst_2 : CommRing 𝒪] [inst_3 : Algebra 𝒪 K]
  [IsIntegralClosure 𝒪 ℤ K] {p : ℤ},
  Prime p → (¬p ∣ NumberField.discr K ↔ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → Algebra.IsUnramifiedAt ℤ P)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.inner_toCLM_conjTranspose_right : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : PartialOrder A] [inst_3 : StarOrderedRing A] [inst_4 : Fintype n] {M : CStarMatrix m n A}
  {v : WithCStarModule A (m → A)} {w : WithCStarModule A (n → A)},
  inner A v ((CStarMatrix.toCLM (Matrix.conjTranspose M)) w) = inner A ((CStarMatrix.toCLM M) v) w
-- Mathlib.Analysis.Calculus.Deriv.Pow
deriv_pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {x : 𝕜},
  DifferentiableAt 𝕜 f x → ∀ (n : ℕ), deriv (f ^ n) x = ↑n * f x ^ (n - 1) * deriv f x
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.le_rpow_iff_log_le : ∀ {x y z : ℝ}, 0 < x → 0 < y → (x ≤ y ^ z ↔ Real.log x ≤ z * Real.log y)
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.conjugator.nil : ∀ {α : Type u} [inst : DecidableEq α], FreeGroup.reduceCyclically.conjugator [] = []
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.exists_st_iff_not_infinite : ∀ {x : ℝ*}, (∃ r, x.IsSt r) ↔ ¬x.Infinite
-- Mathlib.NumberTheory.ZetaValues
periodizedBernoulli.eq_1 : ∀ (k : ℕ), periodizedBernoulli k = AddCircle.liftIco 1 0 (bernoulliFun k)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPushouts.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C},
  autoParam (∀ {X Y S : C} {f : S ⟶ X} (g : S ⟶ Y), P f → CategoryTheory.Limits.HasPushout f g)
      CategoryTheory.MorphismProperty.HasPushouts.hasPushout._autoParam →
    P.HasPushouts
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a vector field under a map between manifolds. If the derivative of the map is
not invertible, then pullback is given the junk value zero.  -/
VectorField.mpullback : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {H : Type u_2} →
      [inst_1 : TopologicalSpace H] →
        {E : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : NormedSpace 𝕜 E] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {H' : Type u_5} →
                        [inst_6 : TopologicalSpace H'] →
                          {E' : Type u_6} →
                            [inst_7 : NormedAddCommGroup E'] →
                              [inst_8 : NormedSpace 𝕜 E'] →
                                (I' : ModelWithCorners 𝕜 E' H') →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        (M → M') → ((x : M') → TangentSpace I' x) → (x : M) → TangentSpace I x
-- Mathlib.Order.SymmDiff
compl_symmDiff_self : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), symmDiff aᶜ a = ⊤
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- If `V : Π i, G i →ₗᵢ[𝕜] E` is an orthogonal family such that the supremum of the ranges of
`V i` is dense, then `(E, V)` is a Hilbert sum of `G`.  -/
IsHilbertSum.mk : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] {G : ι → Type u_4} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] [inst_5 : CompleteSpace E] {V : (i : ι) → G i →ₗᵢ[𝕜] E}
  [∀ (i : ι), CompleteSpace (G i)],
  OrthogonalFamily 𝕜 G V → ⊤ ≤ (⨆ i, (V i).range).topologicalClosure → IsHilbertSum 𝕜 G V
-- Mathlib.Analysis.Convex.Exposed
IsExposed.isExtreme : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : TopologicalSpace E] [inst_6 : Module 𝕜 E] {A B : Set E},
  IsExposed 𝕜 A B → IsExtreme 𝕜 A B
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.of_injective : ∀ {α : Type u}, Function.Injective FreeCommRing.of
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_alter_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {fallback : β} {f : Option β → Option β}, (m.alter k f).getD k fallback = (f m[k]?).getD fallback
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- `biproduct f` computes the biproduct of a family of elements `f`. (It is defined as an
abbreviation for `limit (Discrete.functor f)`, so for most facts about `biproduct f`, you will
just use general facts about limits and colimits.)  -/
CategoryTheory.Limits.«term⨁_» : Lean.ParserDescr
-- Mathlib.Tactic.LinearCombination.Lemmas
/-- Given an (in)equality, look up the lemma to right-scalar-multiply it by a constant (vector).
If relevant, also take into account the degree of positivity which can be proved of the constant:
strict or non-strict.  -/
Mathlib.Ineq.smulConstRelData : Mathlib.Ineq.WithStrictness → Lean.Name
-- Mathlib.Dynamics.Flow
Flow.mk.sizeOf_spec : ∀ {τ : Type u_1} {α : Type u_2} [inst : TopologicalSpace τ] [inst_1 : TopologicalSpace α] [inst_2 : AddZero τ]
  [inst_3 : SizeOf τ] [inst_4 : SizeOf α] (toFun : τ → α → α) (cont' : Continuous (Function.uncurry toFun))
  (map_add' : ∀ (t₁ t₂ : τ) (x : α), toFun (t₁ + t₂) x = toFun t₁ (toFun t₂ x)) (map_zero' : ∀ (x : α), toFun 0 x = x),
  sizeOf { toFun := toFun, cont' := cont', map_add' := map_add', map_zero' := map_zero' } = 1 + sizeOf cont'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrpObj.lift_addCommutator_eq_add_add_neg_neg_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {X G : C}
  [inst_2 : CategoryTheory.AddGrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f₁ f₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.AddGrpObj.addCommutator G) h) =
    CategoryTheory.CategoryStruct.comp (f₁ + f₂ + -f₁ + -f₂) h
-- Lean.Data.AssocList
_private.Lean.Data.AssocList.0.Lean.AssocList.forIn.loop : {α : Type u} →
  {β : Type v} →
    {δ : Type w} → {m : Type w → Type w'} → [Monad m] → (α × β → δ → m (ForInStep δ)) → δ → Lean.AssocList α β → m δ
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso_hom_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorRight W)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRightIso X₁ X₂).hom.right =
    (CategoryTheory.MonoidalCategoryStruct.associator X₁.right X₂.right W).hom
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.isNilpotent_pi`.

---

n-ary products of nilpotent groups are nilpotent.  -/
isNilpotent_pi : ∀ {η : Type u_2} {Gs : η → Type u_3} [inst : (i : η) → Group (Gs i)] [Finite η] [∀ (i : η), Group.IsNilpotent (Gs i)],
  Group.IsNilpotent ((i : η) → Gs i)
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.topEquiv.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G], AddSubgroup.topEquiv = AddSubmonoid.topEquiv
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Result.mk : Lean.Expr → Option Lean.Expr → Bool → Lean.Meta.Simp.Result
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.of_toList_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  t₁.toList.Perm t₂.toList → t₁.Equiv t₂
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The coefficients of each root in the `𝔤₂` root pairing, relative to the base.  -/
RootPairing.EmbeddedG2.allCoeffs : List (Fin 2 → ℤ)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- If every element belongs to exactly `n` Finsets, then the sum of their sizes is `n` times how
many they are.  -/
Finset.sum_card : ∀ {α : Type u_2} [inst : DecidableEq α] {B : Finset (Finset α)} {n : ℕ} [inst_1 : Fintype α],
  (∀ (a : α), {b ∈ B | a ∈ b}.card = n) → ∑ s ∈ B, s.card = Fintype.card α * n
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.IsCircuit.closure_sdiff_singleton_eq : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.IsCircuit C → ∀ (e : α), M.closure (C \ {e}) = M.closure C
-- Init.Data.Option.Lemmas
Option.isNone_pbind_iff : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : (a : α) → o = some a → Option β},
  (o.pbind f).isNone = true ↔ o = none ∨ ∃ a, ∃ (h : o = some a), f a h = none
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.State.mk : Lean.NameMap Lean.ExprSet → Array (Lean.Ident × Lean.Name) → Lean.Elab.ConfigEval.State✝
-- Mathlib.CategoryTheory.Functor.Functorial
CategoryTheory.instFunctorialObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (F : CategoryTheory.Functor C D) → CategoryTheory.Functorial F.obj
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.continuousAt : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) {x : M₁}, ContinuousAt (⇑e) x
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.matchAt?.fun_cases_unfolding : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} (startPos : s.Pos)
  (motive : Option s.Pos → Prop),
  (∀ (h : ∃ endPos, String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos), motive (some h.choose)) →
    ((¬∃ endPos, String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos) → motive none) →
      motive (String.Slice.Pattern.Model.matchAt? pat startPos)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.smul_bot : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α G] (a : α),
  a • ⊥ = ⊥
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_erase : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α}, a ∈ m.erase k ↔ (k == a) = false ∧ a ∈ m
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
aemeasurable_lineDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {v : E}
  [inst_9 : MeasurableSpace F] [BorelSpace F],
  Continuous f → ∀ (μ : MeasureTheory.Measure E), AEMeasurable (fun x => lineDeriv 𝕜 f x v) μ
-- Mathlib.Analysis.Normed.Group.Subgroup
AddSubgroup.seminormedAddGroup.eq_1 : ∀ {E : Type u_1} [inst : SeminormedAddGroup E] {s : AddSubgroup E},
  AddSubgroup.seminormedAddGroup =
    { norm := fun a => ‖s.subtype a‖, toAddGroup := s.toAddGroup, toPseudoMetricSpace := Subtype.pseudoMetricSpace,
      dist_eq := ⋯ }
-- Mathlib.Data.ENNReal.Operations
ENNReal.ofReal_iInf : ∀ {ι : Sort u_1} [Nonempty ι] (f : ι → ℝ), ENNReal.ofReal (⨅ i, f i) = ⨅ i, ENNReal.ofReal (f i)
-- Mathlib.LinearAlgebra.Matrix.HadamardMatrix
/-- Negating a Hadamard matrix gives a Hadamard matrix.  -/
Matrix.IsHadamard.neg : ∀ {n : Type u_2} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Ring R] [inst_3 : StarRing R]
  {A : Matrix n n R}, A.IsHadamard → (-A).IsHadamard
-- Mathlib.Computability.TuringMachine.Config
/-- The `stepRet` function respects the `then k'` homomorphism. Note that this is an exact
equality, not a simulation; the original and embedded machines move in lock-step until the
embedded machine reaches the halt state.  -/
Turing.ToPartrec.stepRet_then : ∀ {k k' : Turing.ToPartrec.Cont} {v : List ℕ},
  Turing.ToPartrec.stepRet (k.then k') v = (Turing.ToPartrec.stepRet k v).then k'
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.mk.injEq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (L₀ L₁ L₂ L₃ : CategoryTheory.ShortComplex C) (v₀₁ : L₀ ⟶ L₁) (v₁₂ : L₁ ⟶ L₂) (v₂₃ : L₂ ⟶ L₃)
  (w₀₂ :
    autoParam (CategoryTheory.CategoryStruct.comp v₀₁ v₁₂ = 0) CategoryTheory.ShortComplex.SnakeInput.w₀₂._autoParam)
  (w₁₃ :
    autoParam (CategoryTheory.CategoryStruct.comp v₁₂ v₂₃ = 0) CategoryTheory.ShortComplex.SnakeInput.w₁₃._autoParam)
  (h₀ : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι v₀₁ w₀₂))
  (h₃ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ v₂₃ w₁₃)) (L₁_exact : L₁.Exact)
  (epi_L₁_g : CategoryTheory.Epi L₁.g) (L₂_exact : L₂.Exact) (mono_L₂_f : CategoryTheory.Mono L₂.f)
  (L₀_1 L₁_1 L₂_1 L₃_1 : CategoryTheory.ShortComplex C) (v₀₁_1 : L₀_1 ⟶ L₁_1) (v₁₂_1 : L₁_1 ⟶ L₂_1)
  (v₂₃_1 : L₂_1 ⟶ L₃_1)
  (w₀₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp v₀₁_1 v₁₂_1 = 0)
      CategoryTheory.ShortComplex.SnakeInput.w₀₂._autoParam)
  (w₁₃_1 :
    autoParam (CategoryTheory.CategoryStruct.comp v₁₂_1 v₂₃_1 = 0)
      CategoryTheory.ShortComplex.SnakeInput.w₁₃._autoParam)
  (h₀_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι v₀₁_1 w₀₂_1))
  (h₃_1 : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ v₂₃_1 w₁₃_1))
  (L₁_exact_1 : L₁_1.Exact) (epi_L₁_g_1 : CategoryTheory.Epi L₁_1.g) (L₂_exact_1 : L₂_1.Exact)
  (mono_L₂_f_1 : CategoryTheory.Mono L₂_1.f),
  ({ L₀ := L₀, L₁ := L₁, L₂ := L₂, L₃ := L₃, v₀₁ := v₀₁, v₁₂ := v₁₂, v₂₃ := v₂₃, w₀₂ := w₀₂, w₁₃ := w₁₃, h₀ := h₀,
        h₃ := h₃, L₁_exact := L₁_exact, epi_L₁_g := epi_L₁_g, L₂_exact := L₂_exact, mono_L₂_f := mono_L₂_f } =
      { L₀ := L₀_1, L₁ := L₁_1, L₂ := L₂_1, L₃ := L₃_1, v₀₁ := v₀₁_1, v₁₂ := v₁₂_1, v₂₃ := v₂₃_1, w₀₂ := w₀₂_1,
        w₁₃ := w₁₃_1, h₀ := h₀_1, h₃ := h₃_1, L₁_exact := L₁_exact_1, epi_L₁_g := epi_L₁_g_1, L₂_exact := L₂_exact_1,
        mono_L₂_f := mono_L₂_f_1 }) =
    (L₀ = L₀_1 ∧ L₁ = L₁_1 ∧ L₂ = L₂_1 ∧ L₃ = L₃_1 ∧ v₀₁ ≍ v₀₁_1 ∧ v₁₂ ≍ v₁₂_1 ∧ v₂₃ ≍ v₂₃_1 ∧ h₀ ≍ h₀_1 ∧ h₃ ≍ h₃_1)
-- Mathlib.Algebra.Algebra.Prod
/-- The `Function.prod` of two morphisms is a morphism.  -/
AlgHom.prod : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R B] →
                  [inst_5 : Semiring C] → [inst_6 : Algebra R C] → (A →ₐ[R] B) → (A →ₐ[R] C) → A →ₐ[R] B × C
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- A field extension `E / F` is purely inseparable if and only if the relative perfect closure of
`F` in `E` is equal to `E`.  -/
isPurelyInseparable_iff_perfectClosure_eq_top : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsPurelyInseparable F E ↔ perfectClosure F E = ⊤
-- Mathlib.Topology.Algebra.Order.Field
/-- In a linearly ordered field with the order topology, if `f` tends to a negative constant `C` and
`g` tends to `Filter.atTop` then `f * g` tends to `Filter.atBot`.  -/
Filter.Tendsto.neg_mul_atTop : ∀ {𝕜 : Type u_1} {α : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderTopology 𝕜] {l : Filter α} {f g : α → 𝕜} {C : 𝕜},
  C < 0 →
    Filter.Tendsto f l (nhds C) → Filter.Tendsto g l Filter.atTop → Filter.Tendsto (fun x => f x * g x) l Filter.atBot
-- Init.Data.List.Lemmas
/-- `simp` unfolds `tailD` in terms of `tail?` and `Option.getD`.  -/
List.tailD_eq_tail? : ∀ {α : Type u_1} {l l' : List α}, l.tailD l' = l.tail?.getD l'
-- Mathlib.CategoryTheory.Types.Basic
TypeCat.Fun.mk.sizeOf_spec : ∀ {X : Type u_1} {Y : Type u_2} [inst : SizeOf X] [inst_1 : SizeOf Y] (toFun : X → Y), sizeOf { toFun := toFun } = 1
-- Mathlib.GroupTheory.GroupAction.Period
/-- For any non-zero `n` less than the period of `m` on `a`, `a` is moved by `n • m`.  -/
AddAction.nsmul_vadd_ne_of_lt_period : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] {m : M} {a : α} {n : ℕ},
  0 < n → n < AddAction.period m a → n • m +ᵥ a ≠ a
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : (a : α) → β a → Option (β a)}, t.WF → (Std.DTreeMap.Raw.filterMap f t).WF
-- Mathlib.Util.Notation3
/-- Turns the `DelabKey` into a key that the `delab` attribute accepts.
 -/
Mathlib.Notation3.DelabKey.key : Mathlib.Notation3.DelabKey → Lean.Name
-- Lean.CoreM
Lean.Core.resetMessageLog : Lean.CoreM Unit
-- Std.Data.TreeSet.Raw.Basic
/-- Two tree sets are equivalent in the sense of Equiv iff all the values are equal.  -/
Std.TreeSet.Raw.Equiv : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp → Prop
-- Batteries.Data.String.Legacy
_private.Batteries.Data.String.Legacy.0.String.Legacy.anyAux.eq_def : ∀ (s : String) (stopPos : String.Pos.Raw) (p : Char → Bool) (i : String.Pos.Raw),
  String.Legacy.anyAux s stopPos p i =
    if h : i < stopPos then
      if p (String.Pos.Raw.get s i) = true then true
      else
        have this := ⋯;
        String.Legacy.anyAux s stopPos p (String.Pos.Raw.next s i)
    else false
-- Mathlib.CategoryTheory.IsConnected
/-- Implementation detail of `isoConstant`.  -/
_private.Mathlib.CategoryTheory.IsConnected.0.CategoryTheory.IsPreconnected.IsoConstantAux.factorThroughDiscrete : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {α : Type u₂} →
      (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) →
        (CategoryTheory.IsPreconnected.IsoConstantAux.liftToDiscrete✝ F).comp (CategoryTheory.Discrete.functor F.obj) ≅
          F