mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- If two add homomorphisms are equal on a set,
then they are equal on its additive subsemigroup closure.  -/
AddHom.eqOn_closure : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f g : M →ₙ+ N} {s : Set M},
  Set.EqOn (⇑f) (⇑g) s → Set.EqOn ⇑f ⇑g ↑(AddSubsemigroup.closure s)
-- Mathlib.FieldTheory.Normal.Closure
IntermediateField.normal_iff_forall_fieldRange_le : ∀ {F : Type u_1} {L : Type u_3} [inst : Field F] [inst_1 : Field L] [inst_2 : Algebra F L] [Normal F L]
  {K : IntermediateField F L}, Normal F ↥K ↔ ∀ (σ : ↥K →ₐ[F] L), σ.fieldRange ≤ K
-- Init.Data.String.Lemmas.StringOrder
String.lt_irrefl : ∀ (a : String), ¬a < a
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.map_range : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} {P : Type u_6} [inst_1 : AddGroup N] [inst_2 : AddGroup P]
  (g : N →+ P) (f : G →+ N), AddSubgroup.map g f.range = (g.comp f).range
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.range_toFiniteMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω],
  Set.range MeasureTheory.ProbabilityMeasure.toFiniteMeasure = {μ | μ.mass = 1}
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_add_union_subset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddCommSemigroup α] {s t : Finset α}, s ∩ t + (s ∪ t) ⊆ s + t
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Adjunction.fromCokleisli_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C)
  (X : CategoryTheory.Cokleisli U), (CategoryTheory.Cokleisli.Adjunction.fromCokleisli U).obj X = U.obj X.of
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
deriv_sin : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → deriv (fun x => Real.sin (f x)) x = Real.cos (f x) * deriv f x
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
/-- **Alias** of the reverse direction of `Multiplicative.toAdd_le`. -/
Multiplicative.toAdd_mono : ∀ {α : Type u_1} [inst : Preorder α] {a b : Multiplicative α}, a ≤ b → Multiplicative.toAdd a ≤ Multiplicative.toAdd b
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.casesOn_mk : ∀ {motive : Complex.UnitDisc → Sort u_1} (mk' : (z : ℂ) → (hz : ‖z‖ < 1) → motive (Complex.UnitDisc.mk z hz)) {z : ℂ}
  (hz : ‖z‖ < 1), Complex.UnitDisc.casesOn mk' (Complex.UnitDisc.mk z hz) = mk' z hz
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.subset : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.IsBasis I X → I ⊆ X
-- Mathlib.Data.List.AList
AList.perm_insert : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ : AList β},
  s₁.entries.Perm s₂.entries → (AList.insert a b s₁).entries.Perm (AList.insert a b s₂).entries
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_multiset_sum : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : AddCommMonoid α] [inst_1 : StarAddMonoid α]
  (s : Multiset (Matrix m n α)), s.sum.conjTranspose = (Multiset.map Matrix.conjTranspose s).sum
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- A version of `eRk_eq_zero_iff'` with no ground-set hypothesis.  -/
Matroid.eRk_eq_zero_iff' : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.eRk X = 0 ↔ X ∩ M.E ⊆ M.loops
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.inverseImage.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty D) (F : CategoryTheory.Functor C D) (x x_1 : C) (f : x ⟶ x_1),
  P.inverseImage F f = P (F.map f)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddCoeOfAddMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Add (R i)] →
              [∀ (i : ι), AddMemClass (S i) (R i)] → Add (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.lift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)} (f f_1 : F' ⟶ F)
  (e_f : f = f_1) {G : CategoryTheory.Subfunctor F} (hf : CategoryTheory.Subfunctor.range f ≤ G),
  CategoryTheory.Subfunctor.lift f hf = CategoryTheory.Subfunctor.lift f_1 ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_pos : ∀ {p : ℝ} {x : ENNReal}, 0 < x → x ≠ ⊤ → 0 < x ^ p
-- Mathlib.Algebra.Order.Field.Basic
sub_inv_antitoneOn_Icc_right : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b c : α},
  c < a → AntitoneOn (fun x => (x - c)⁻¹) (Set.Icc a b)
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instHashableRange : Hashable Lean.Lsp.Range
-- Lean.Meta.Match.SolveOverlap
_private.Lean.Meta.Match.SolveOverlap.0.Lean.Meta.Match.solveOverlap.loop : Lean.MVarId → Lean.FVarIdSet → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F G : CategoryTheory.Functor J C} [inst_2 : CategoryTheory.Limits.HasColimit F]
  [inst_3 : CategoryTheory.Limits.HasColimit G] (t : CategoryTheory.Limits.Cocone G) (w : F ≅ G) {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc G t) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.desc F ((CategoryTheory.Limits.Cocone.precompose w.hom).obj t)) h
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The Fourier integral is well defined iff the function is integrable. Version with a general
continuous bilinear function `L`. For the specialization to the inner product in an inner product
space, see `Real.fourierIntegral_convergent_iff`.  -/
Real.fourierIntegral_convergent_iff' : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_4} {W : Type u_5}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  [inst_6 : MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V} {f : V → E} (L : V →L[ℝ] W →L[ℝ] ℝ) (w : W),
  MeasureTheory.Integrable (fun v => Real.fourierChar (-(L v) w) • f v) μ ↔ MeasureTheory.Integrable f μ
-- Mathlib.Topology.Closure
interior_eq_iff_isOpen : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, interior s = s ↔ IsOpen s
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unmop_hom_rightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᴹᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom.unmop =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.unmop).hom
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.copy_eq`. -/
Topology.CWComplex.Subcomplex.copy_eq : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  (E : Topology.RelCWComplex.Subcomplex C) (F : Set X) (hF : F = ↑E)
  (J : (n : ℕ) → Set (Topology.RelCWComplex.cell C n)) (hJ : J = E.I), E.copy F hF J hJ = E
-- Mathlib.Data.Finset.MulAntidiagonal
Set.IsWF.mul : ∀ {α : Type u_1} {s t : Set α} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedCancelMonoid α],
  s.IsWF → t.IsWF → (s * t).IsWF
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- A weighted sum of pairwise subtractions, where the point on the left is constant and the
sum of the weights is 1.  -/
Finset.sum_smul_const_vsub_eq_vsub_affineCombination : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p₂ : ι → P) (p₁ : P),
  ∑ i ∈ s, w i = 1 → ∑ i ∈ s, w i • (p₁ -ᵥ p₂ i) = p₁ -ᵥ (Finset.affineCombination k s p₂) w
-- Mathlib.Order.Category.BddDistLat
BddDistLat.instConcreteCategoryBoundedLatticeHomCarrier : CategoryTheory.ConcreteCategory BddDistLat fun x1 x2 => BoundedLatticeHom ↑x1.toDistLat ↑x2.toDistLat
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.mk : ∀ {K : Type u_1} [inst : Field K] [to_charZero : CharZero K] [to_finiteDimensional : FiniteDimensional ℚ K],
  NumberField K
-- Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean
/-- Let `G` be a nonarchimedean additive abelian group, and let `f : α → G` be a
function that tends to zero on the filter of cofinite sets. For each finite subset of `α`, consider
the partial sum of `f` on that subset. These partial sums form a Cauchy filter.  -/
NonarchimedeanAddGroup.cauchySeq_sum_of_tendsto_cofinite_zero : ∀ {α : Type u_1} {G : Type u_2} [inst : AddCommGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G]
  [NonarchimedeanAddGroup G] {f : α → G}, Filter.Tendsto f Filter.cofinite (nhds 0) → CauchySeq fun s => ∑ i ∈ s, f i
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.preBeth_univ : Cardinal.preBeth Ordinal.univ.{u, v} = Cardinal.univ.{u, v}
-- Mathlib.Algebra.Category.ModuleCat.Limits
ModuleCat.forget_preservesLimits : ∀ {R : Type u} [inst : Ring R], CategoryTheory.Limits.PreservesLimits (CategoryTheory.forget (ModuleCat R))
-- Batteries.Control.ForInStep.Lemmas
ForInStep.bind_bindList_assoc : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] [LawfulMonad m] (f : β → m (ForInStep β))
  (g : α → β → m (ForInStep β)) (s : ForInStep β) (l : List α),
  (do
      let x ← s.bind f
      ForInStep.bindList g l x) =
    s.bind fun b => do
      let x ← f b
      ForInStep.bindList g l x
-- Mathlib.AlgebraicTopology.SimplexCategory.Defs
SimplexCategory.Hom.comp.eq_1 : ∀ {a b c : SimplexCategory} (f : b.Hom c) (g : a.Hom b),
  f.comp g = SimplexCategory.Hom.mk (f.toOrderHom.comp g.toOrderHom)
-- Init.Data.Float.Float
/-- Compares two floating point numbers for non-strict inequality.

This function does not reduce in the kernel. It is compiled to the C inequality operator.
 -/
Float.decLe : (a b : Float) → Decidable (a ≤ b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_eq_some_minKey! : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  l.isEmpty = false → Std.Internal.List.minKey? l = some (Std.Internal.List.minKey! l)
-- Init.Data.Int.DivMod.Lemmas
Int.tmod.eq_2 : ∀ (m n : ℕ), (Int.ofNat m).tmod (Int.negSucc n) = Int.ofNat (m % n.succ)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_iff_forall_smul_nonneg`. -/
MonovaryOn.sub_smul_sub_nonneg : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [IsStrictOrderedModule α β] {f : ι → α} {g : ι → β} {s : Set ι},
  MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → 0 ≤ (f j - f i) • (g j - g i)
-- Mathlib.Topology.Algebra.ConstMulAction
Homeomorph.smul_symm : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [inst_3 : ContinuousConstSMul G α] {g : G}, (Homeomorph.smul g).symm = Homeomorph.smul g⁻¹
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.bot_mem : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α}, ⊥ ∈ L
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
BoundedContinuousFunction.instCoeTC : {F : Type u_1} →
  {α : Type u} →
    {β : Type v} →
      [inst : TopologicalSpace α] →
        [inst_1 : PseudoMetricSpace β] →
          [inst_2 : FunLike F α β] → [BoundedContinuousMapClass F α β] → CoeTC F (BoundedContinuousFunction α β)
-- Mathlib.Algebra.Category.ModuleCat.Kernels
ModuleCat.cokernel_π_cokernelIsoRangeQuotient_hom_apply : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↑H),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.cokernelIsoRangeQuotient f).hom)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.cokernel.π f)) x) =
    Submodule.Quotient.mk x
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.congr_refl : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B],
  Algebra.TensorProduct.congr AlgEquiv.refl AlgEquiv.refl = AlgEquiv.refl
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : Add α] [inst_1 : Monoid γ]
  [inst_2 : AddGroup β] [inst_3 : DistribMulAction γ β],
  Function.Antiperiodic f c → ∀ (a : γ), Function.Antiperiodic (a • f) c
-- Mathlib.Tactic.NormNum.Eq
/-- The `norm_num` extension which identifies expressions of the form `a = b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalEq : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.AlgebraicGeometry.Artinian
/-- A scheme is Artinian if it is locally Artinian and quasi-compact  -/
AlgebraicGeometry.IsArtinianScheme : AlgebraicGeometry.Scheme → Prop
-- Mathlib.Tactic.Bound
/-- Close numerical goals with `norm_num`  -/
Mathlib.Tactic.Bound.boundNormNum : Aesop.RuleTac
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.noncommPiCoprod.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] (ϕ : (i : ι) → N i →+ M)
  (hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)),
  AddMonoidHom.noncommPiCoprod ϕ hcomm =
    { toFun := fun f => Finset.univ.noncommSum (fun i => (ϕ i) (f i)) ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.MeasureTheory.Integral.Prod
/-- The Bochner integral is a.e.-measurable.
This shows that the integrand of (the right-hand-side of) Fubini's theorem is a.e.-measurable.  -/
MeasureTheory.AEStronglyMeasurable.integral_prod_right' : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] ⦃f : α × β → E⦄,
  MeasureTheory.AEStronglyMeasurable f (μ.prod ν) →
    MeasureTheory.AEStronglyMeasurable (fun x => ∫ (y : β), f (x, y) ∂ν) μ
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.smul_comp : ∀ {k : Type u} {G : Type v} [inst : CommSemiring k] [inst_1 : Monoid G] {M N O : Rep.{u_1, u, v} k G} (r : k)
  (f : M ⟶ N) (g : N ⟶ O), CategoryTheory.CategoryStruct.comp (r • f) g = r • CategoryTheory.CategoryStruct.comp f g
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_neg : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Neg R] (a : QuaternionAlgebra R c₁ c₂ c₃), (-a).imJ = -a.imJ
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Term.realize_varsToConstants : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'}
  [inst_1 : (L.withConstants α).Structure M] [(L.lhomWithConstants α).IsExpansionOn M] {t : L.Term (α ⊕ β)} {v : β → M},
  FirstOrder.Language.Term.realize v t.varsToConstants =
    FirstOrder.Language.Term.realize (Sum.elim (fun a => ↑(L.con a)) v) t
-- Mathlib.Analysis.Complex.Circle
Circle.instCompactSpace : CompactSpace Circle
-- Mathlib.Combinatorics.Additive.CovBySMul
/-- Predicate for a set `A` to be covered by at most `K` cosets of another set `B`
under the action by the monoid `M`.  -/
CovByVAdd : (M : Type u_1) → {X : Type u_3} → [inst : AddMonoid M] → [AddAction M X] → ℝ → Set X → Set X → Prop
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.motive : Lean.Meta.MatcherApp → Lean.Expr
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.instIsEquivalenceFunctorFunctorsInvertingWhiskeringLeftFunctor : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) (E : Type u_3) [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W], (CategoryTheory.Localization.whiskeringLeftFunctor L W E).IsEquivalence
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- The identity morphism between reflexive quivers.  -/
CategoryTheory.ReflPrefunctor.id : (V : Type u_1) → [inst : CategoryTheory.ReflQuiver V] → V ⥤rq V
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.WF.erase! : ∀ {α : Type u} {β : α → Type v} {x : Ord α} [Std.TransOrd α] {k : α} {l : Std.DTreeMap.Internal.Impl α β},
  l.WF → (Std.DTreeMap.Internal.Impl.erase! k l).WF
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
IsSymmSndFDerivAt.eq_1 : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) (x : E),
  IsSymmSndFDerivAt 𝕜 f x = ∀ (v w : E), ((fderiv 𝕜 (fderiv 𝕜 f) x) v) w = ((fderiv 𝕜 (fderiv 𝕜 f) x) w) v
-- Init.Data.Array.Count
Array.count_erase_of_ne : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α},
  a ≠ b → ∀ (xs : Array α), Array.count a (xs.erase b) = Array.count a xs
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.triangle_obj₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L),
  (CochainComplex.mappingCone.triangle φ).obj₁ = K
-- Init.Data.String.Lemmas.Basic
_private.Init.Data.String.Lemmas.Basic.0.String.Slice.Pos.nextn.match_1.splitter : (motive : ℕ → Sort u_1) → (n : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive n
-- Lean.Meta.Basic
/-- Similar to `forallTelescope`, but given `type` of the form `forall xs, A`,
it reduces `A` and continues building the telescope if it is a `forall`.

If `cleanupAnnotations` is `true`, we apply `Expr.cleanupAnnotations` to each type in the telescope.

If `whnfType` is `true`, we give `k` the `whnf` of the resulting type. This is a free operation.
 -/
Lean.Meta.forallTelescopeReducing : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] →
    [Monad n] →
      {α : Type} → Lean.Expr → (Array Lean.Expr → Lean.Expr → n α) → optParam Bool false → optParam Bool false → n α
-- Init.Data.BitVec.Lemmas
BitVec.toNat_sshiftRight : ∀ {w : ℕ} {x : BitVec w} {n : ℕ},
  (x.sshiftRight n).toNat = if x.msb = true then 2 ^ w - 1 - (2 ^ w - 1 - x.toNat) >>> n else x.toNat >>> n
-- Mathlib.Data.Nat.Nth
Nat.nth_eq_orderEmbOfFin : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite) {n : ℕ} (hn : n < hf.toFinset.card),
  Nat.nth p n = (hf.toFinset.orderEmbOfFin ⋯) ⟨n, hn⟩
-- Mathlib.Analysis.Calculus.Deriv.Abs
DifferentiableWithinAt.abs_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E},
  DifferentiableWithinAt ℝ f s x → 0 < f x → DifferentiableWithinAt ℝ (fun x => |f x|) s x
-- Mathlib.Data.Nat.Fib.Zeckendorf
_private.Mathlib.Data.Nat.Fib.Zeckendorf.0.Nat.zeckendorf.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (m n : ℕ) → m = n + 1 → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | m@h:n.succ => h_2 m n h) =
    h_1 ()
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- If `k.left` is an epimorphism, then `k` is an epimorphism. In other words, `Over.forget X` reflects
epimorphisms.
The converse does not hold without additional assumptions on the underlying category, see
`CategoryTheory.Over.epi_left_of_epi`.
 -/
CategoryTheory.Over.epi_of_epi_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (k : f ⟶ g)
  [hk : CategoryTheory.Epi (CategoryTheory.Over.Hom.left k)], CategoryTheory.Epi k
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ ∪ t₂)[k]? = t₁[k]?
-- Init.GetElem
none_eq_getElem?_iff : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)], none = c[i]? ↔ ¬dom c i
-- Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex
/-- The preimage of a subcomplex by a morphism of simplicial sets.  -/
SSet.Subcomplex.preimage : {X Y : SSet} → X.Subcomplex → (Y ⟶ X) → Y.Subcomplex
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix_mulVec_apply : ∀ {V : Type u_1} {R : Type u_2} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : NonAssocRing R] (v : V) (vec : V → R),
  (SimpleGraph.lapMatrix R G).mulVec vec v = ↑(G.degree v) * vec v - ∑ u ∈ G.neighborFinset v, vec u
-- Mathlib.Algebra.Order.Hom.Ring
/-- `OrderRingHom α β`, denoted `α →+*o β`,
is the type of monotone semiring homomorphisms from `α` to `β`.

When possible, instead of parametrizing results over `(f : OrderRingHom α β)`,
you should parametrize over `(F : Type*) [OrderRingHomClass F α β] (f : F)`.

When you extend this structure, make sure to extend `OrderRingHomClass`.  -/
«term_→+*o_» : Lean.TrailingParserDescr
-- Init.Data.List.Sublist
_private.Init.Data.List.Sublist.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Mathlib.Topology.Separation.SeparatedNhds
SeparatedNhds.isClosed_left_of_isClosed_union : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s t : Set X}, SeparatedNhds s t → IsClosed (s ∪ t) → IsClosed s
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.int_mul : ∀ {p x : ℝ} {m : ℤ}, LiouvilleWith p x → m ≠ 0 → LiouvilleWith p (↑m * x)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic
CStarAlgebra.instNonnegSpectrumClassComplexUnital : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A], NonnegSpectrumClass ℂ A
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_toNat_eq_self`. -/
ENat.coe_toNat_eq_self : ∀ {n : ℕ∞}, ↑n.toNat = n ↔ n ≠ ⊤
-- Lean.DeprecatedModule
Lean.Environment.getDeprecatedModuleByIdx? : Lean.Environment → Lean.ModuleIdx → Option Lean.DeprecatedModuleEntry
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the largest key that is less than the given key,
panicking if no such key exists.
 -/
Std.ExtTreeMap.getKeyLT! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeMap α β cmp → α → α
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.prod_monotone : ∀ {X Y : SSet} {A₁ A₂ : X.Subcomplex}, A₁ ≤ A₂ → ∀ {B₁ B₂ : Y.Subcomplex}, B₁ ≤ B₂ → A₁.prod B₁ ≤ A₂.prod B₂
-- Init.Data.Array.Find
_private.Init.Data.Array.Find.0.Option.pmap_or.match_1.splitter : {α : Type u_1} →
  {p : α → Prop} →
    {o' : Option α} →
      (motive : (o : Option α) → {h : ∀ (a : α), o.or o' = some a → p a} → Sort u_2) →
        (o : Option α) →
          {h : ∀ (a : α), o.or o' = some a → p a} →
            ((h : ∀ (a : α), none.or o' = some a → p a) → motive none) →
              ((a : α) → (h : ∀ (a_1 : α), (some a).or o' = some a_1 → p a_1) → motive (some a)) → motive o
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_lt_sin_of_lt_of_le_pi_div_two : ∀ {x y : ℝ}, -(Real.pi / 2) ≤ x → y ≤ Real.pi / 2 → x < y → Real.sin x < Real.sin y
-- Mathlib.RingTheory.Ideal.GoingUp
/-- If `S` is an integral `R`-algebra such that `q` is the unique prime of `S` lying over
a prime `p` of `R`, then any `x ∉ q` divides some `r ∉ p`.  -/
Ideal.exists_notMem_dvd_algebraMap_of_primesOver_eq_singleton : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [p.IsPrime] {q : Ideal S} [q.IsPrime],
  p.primesOver S = {q} → ∀ [Algebra.IsIntegral R S], ∀ x ∉ q, ∃ r ∉ p, x ∣ (algebraMap R S) r