mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
/-- Split coequalizers are absolute: they are preserved by any functor.  -/
CategoryTheory.IsSplitCoequalizer.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X Y : C} →
          {f g : X ⟶ Y} →
            {Z : C} →
              {π : Y ⟶ Z} →
                CategoryTheory.IsSplitCoequalizer f g π →
                  (F : CategoryTheory.Functor C D) → CategoryTheory.IsSplitCoequalizer (F.map f) (F.map g) (F.map π)
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.ext' : ∀ {α : Type u} [inst : Group α] {f g : GroupTopology α}, TopologicalSpace.IsOpen = TopologicalSpace.IsOpen → f = g
-- Mathlib.NumberTheory.FLT.Three
/-- `Solution` is the same as `Solution'` with the additional assumption that `λ ^ 2 ∣ a + b`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution : {K : Type u_1} → [inst : Field K] → {ζ : K} → IsPrimitiveRoot ζ 3 → Type u_1
-- Mathlib.Analysis.Complex.Norm
Complex.isCauSeq_conj : ∀ (f : CauSeq ℂ fun x => ‖x‖), IsCauSeq (fun x => ‖x‖) fun n => (starRingEnd ℂ) (↑f n)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepSet_iff_meas_biInter : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : ι → Set Ω},
  (∀ (i : ι), MeasurableSet (f i)) →
    (ProbabilityTheory.iIndepSet f μ ↔ ∀ (s : Finset ι), μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i))
-- Mathlib.NumberTheory.Ostrowski
/-- The minimal positive integer with absolute value smaller than 1 is a prime number.  -/
Rat.AbsoluteValue.is_prime_of_minimal_nat_zero_lt_and_lt_one : ∀ {f : AbsoluteValue ℚ ℝ} {p : ℕ}, 0 < f ↑p → f ↑p < 1 → (∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m) → Nat.Prime p
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.ofLe.eq_1 : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K' : LieSubalgebra R L} (h : K ≤ K'), LieSubalgebra.ofLe h = (LieSubalgebra.inclusion h).range
-- Mathlib.Algebra.Group.Even
isSquare_ofAdd_iff : ∀ {α : Type u_2} [inst : Add α] {a : α}, IsSquare (Multiplicative.ofAdd a) ↔ Even a
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.all_ae_norm_ofReal_F_le_bound : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {F : ℕ → α → β} {bound : α → ℝ},
  (∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
    ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ENNReal.ofReal ‖F n a‖ ≤ ENNReal.ofReal (bound a)
-- Mathlib.LinearAlgebra.Matrix.Block
/-- **Alias** of `Matrix.det_of_isUpperTriangular`. -/
Matrix.det_of_upperTriangular : ∀ {m : Type u_3} {R : Type v} {M : Matrix m m R} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : LinearOrder m], M.IsUpperTriangular → M.det = ∏ i, M i i
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.insert.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (l l_1 : Std.ExtTreeSet α cmp),
  l = l_1 → ∀ (a a_1 : α), a = a_1 → l.insert a = l_1.insert a_1
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasStrictDerivAt.hasDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasStrictDerivAt f f' x → HasDerivAt f f' x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
multipliableUniformlyOn_euler_sin_prod_on_compact : ∀ {Z : Set ℂ}, IsCompact Z → MultipliableUniformlyOn (fun n z => 1 + sineTerm z n) Z
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_sub : ∀ {a b : USize} (h : System.Platform.numBits = 64), (a - b).toBitVec64 h = a.toBitVec64 h - b.toBitVec64 h
-- Mathlib.RingTheory.Polynomial.Resultant.Basic
Polynomial.resultant_zero_right : ∀ {R : Type u_1} [inst : CommRing R] (f : Polynomial R) (m n : ℕ), f.resultant 0 m n = 0 ^ m * f.coeff 0 ^ n
-- Mathlib.Topology.Connected.Basic
/-- A preconnected set is one where there is no non-trivial open partition.  -/
IsPreconnected : {α : Type u} → [TopologicalSpace α] → Set α → Prop
-- Mathlib.Order.Interval.Set.OrdConnected
/-- The preimage of an `OrdConnected` set under a map which is antitone on a set `t`,
when intersected with `t`, is `OrdConnected`. More precisely, it is the intersection with `t`
of an `OrdConnected` set.  -/
Set.OrdConnected.preimage_antitoneOn : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : β → α} {t : Set β} {s : Set α},
  s.OrdConnected → AntitoneOn f t → ∃ u, u.OrdConnected ∧ t ∩ f ⁻¹' s = t ∩ u
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.forIn.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {σ : Type u_1} [inst : Monad m] (as : RBTree.RBNode α) (init : σ)
  (f : α → σ → m (ForInStep σ)), as.forIn init f = ForInStep.run <$> RBTree.RBNode.forIn.visit f as init
-- Mathlib.Combinatorics.Graph.Subgraph
Graph.noEdge_empty : ∀ {α : Type u_1} {β : Type u_2}, Graph.noEdge ∅ β = ⊥
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} [inst : Inhabited β] {f : Option β → Option β},
      Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.alter t k f) k = (f (Std.DTreeMap.Raw.Const.get? t k)).get!
-- Mathlib.Data.Finset.Preimage
Finset.preimage_inr : ∀ {α : Type u} {β : Type v} (s : Finset (α ⊕ β)), s.preimage Sum.inr ⋯ = s.toRight
-- Mathlib.Data.Finset.Sups
/-- `s ⊻ t` is the finset of elements of the form `a ⊔ b` where `a ∈ s`, `b ∈ t`.  -/
Finset.hasSups : {α : Type u_2} → [DecidableEq α] → [SemilatticeSup α] → HasSups (Finset α)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.toAddSubmonoid_sSup : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set (Submodule R M)), (sSup s).toAddSubmonoid = sSup (Submodule.toAddSubmonoid '' s)
-- Mathlib.Data.Multiset.ZeroCons
Multiset.zero_subset : ∀ {α : Type u_1} (s : Multiset α), 0 ⊆ s
-- Std.Data.DHashMap.Basic
/-- Retrieves the key from the mapping that matches `a`. Ensures that such a mapping exists by
requiring a proof of `a ∈ m`. The result is guaranteed to be pointer equal to the key in the map.
 -/
Std.DHashMap.getKey : {α : Type u} → {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → (m : Std.DHashMap α β) → (a : α) → a ∈ m → α
-- Mathlib.CategoryTheory.GlueData
/-- If `F` preserves the gluing, we obtain an iso between the glued objects.  -/
CategoryTheory.GlueData.gluedIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    {C' : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v, u₂} C'] →
        (D : CategoryTheory.GlueData C) →
          (F : CategoryTheory.Functor C C') →
            [inst_2 : CategoryTheory.Limits.HasMulticoequalizer D.diagram] →
              [inst_3 : CategoryTheory.Limits.PreservesColimit D.diagram.multispan F] →
                [inst_4 :
                    ∀ (i j k : D.J),
                      CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F] →
                  F.obj D.glued ≅ (D.mapGlueData F).glued
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
/-- If `m u = ∞` for any set `u` that has nonempty intersection both with `s` and `t`, then
`μ (s ∪ t) = μ s + μ t`, where `μ = MeasureTheory.OuterMeasure.boundedBy m`.

E.g., if `α` is an (e)metric space and `m u = ∞` on any set of diameter `≥ r`, then this lemma
implies that `μ (s ∪ t) = μ s + μ t` on any two sets such that `r ≤ edist x y` for all `x ∈ s`
and `y ∈ t`.  -/
MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter : ∀ {α : Type u_1} {m : Set α → ENNReal} {s t : Set α},
  (∀ (u : Set α), (s ∩ u).Nonempty → (t ∩ u).Nonempty → m u = ⊤) →
    (MeasureTheory.OuterMeasure.boundedBy m) (s ∪ t) =
      (MeasureTheory.OuterMeasure.boundedBy m) s + (MeasureTheory.OuterMeasure.boundedBy m) t
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.hasLeftKanExtension : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F}
  (h : E.IsPointwiseLeftKanExtension), L.HasLeftKanExtension F
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_ofNatLT : ∀ {n x i : ℕ} (h : x < 2 ^ n), (x#'h).getMsbD i = (decide (i < n) && x.testBit (n - 1 - i))
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.g_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (s : S.Splitting),
  CategoryTheory.CategoryStruct.comp S.g s.s =
    CategoryTheory.CategoryStruct.id S.X₂ - CategoryTheory.CategoryStruct.comp s.r S.f
-- Mathlib.Topology.Algebra.Module.Basic
Submodule.topologicalAddGroup_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] (S : Submodule R M) [IsTopologicalAddGroup M], IsTopologicalAddGroup (M ⧸ S)
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- The sum of two diffeomorphisms: this is `Sum.map` as a diffeomorphism.  -/
Diffeomorph.sumCongr : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_5} →
                  [inst_5 : TopologicalSpace H] →
                    {I : ModelWithCorners 𝕜 E H} →
                      {M : Type u_9} →
                        [inst_6 : TopologicalSpace M] →
                          [inst_7 : ChartedSpace H M] →
                            {n : WithTop ℕ∞} →
                              {M' : Type u_13} →
                                [inst_8 : TopologicalSpace M'] →
                                  [inst_9 : ChartedSpace H M'] →
                                    {N : Type u_15} →
                                      [inst_10 : TopologicalSpace N] →
                                        [inst_11 : ChartedSpace H N] →
                                          {J : ModelWithCorners 𝕜 E' H} →
                                            {N' : Type u_17} →
                                              [inst_12 : TopologicalSpace N'] →
                                                [inst_13 : ChartedSpace H N'] →
                                                  Diffeomorph I J M N n →
                                                    Diffeomorph I J M' N' n → Diffeomorph I J (M ⊕ M') (N ⊕ N') n
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_zsmul : ∀ {G : Type u_5} [inst : AddGroup G] (n : ℤ) (a : G), WithZero.exp (n • a) = WithZero.exp a ^ n
-- Mathlib.LinearAlgebra.Matrix.Notation
/-- Notation for m×n matrices, aka `Matrix (Fin m) (Fin n) α`.

For instance:
* `!![a, b, c; d, e, f]` is the matrix with two rows and three columns, of type
  `Matrix (Fin 2) (Fin 3) α`
* `!![a, b, c]` is a row vector of type `Matrix (Fin 1) (Fin 3) α` (see also `Matrix.row`).
* `!![a; b; c]` is a column vector of type `Matrix (Fin 3) (Fin 1) α` (see also `Matrix.col`).

This notation implements some special cases:

* `![,,]`, with `n` `,`s, is a term of type `Matrix (Fin 0) (Fin n) α`
* `![;;]`, with `m` `;`s, is a term of type `Matrix (Fin m) (Fin 0) α`
* `![]` is the 0×0 matrix

Note that vector notation is provided elsewhere (by `Matrix.vecNotation`) as `![a, b, c]`.
Under the hood, `!![a, b, c; d, e, f]` is syntax for `Matrix.of ![![a, b, c], ![d, e, f]]`.
 -/
Matrix.matrixNotation : Lean.ParserDescr
-- Mathlib.GroupTheory.GroupAction.Hom
MulActionHom.coe_mul : ∀ {M : Type u_2} {N : Type u_3} {X : Type u_4} {Y : Type u_5} {σ : M → N} [inst : SMul M X] [inst_1 : Monoid N]
  [inst_2 : Monoid Y] [inst_3 : MulDistribMulAction N Y] (f g : X →ₑ[σ] Y), ⇑(f * g) = ⇑f * ⇑g
-- Lean.Elab.App
/-- Auxiliary structure for elaborating the application `f args namedArgs`.  -/
Lean.Elab.Term.ElabAppArgs.State : Type
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.affineBasisCover_is_basis : ∀ (X : AlgebraicGeometry.Scheme), TopologicalSpace.IsTopologicalBasis {x | ∃ a, x = Set.range ⇑(X.affineBasisCover.f a)}
-- Mathlib.Algebra.Order.AddGroupWithTop
add_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommMonoidWithTop α] (a : α), a + ⊤ = ⊤
-- Mathlib.Order.CompactlyGenerated.Basic
sSup_compact_eq_top : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α], sSup {a | IsCompactElement a} = ⊤
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.div_smul : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] {R : Type u_1} [inst_2 : Monoid R]
  [inst_3 : DistribMulAction R (Polynomial K)] [inst_4 : IsScalarTower R (Polynomial K) (Polynomial K)] (c : R)
  (p q : Polynomial K),
  (algebraMap (Polynomial K) (RatFunc K)) (c • p) / (algebraMap (Polynomial K) (RatFunc K)) q =
    c • ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)
-- Mathlib.Order.Grade
instWellFoundedLTOfGradeOrderNat : ∀ {α : Type u_3} [inst : Preorder α] [GradeOrder ℕ α], WellFoundedLT α
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
_private.Mathlib.RingTheory.DedekindDomain.Ideal.Basic.0.IsDedekindDomainInv.integrallyClosed : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A], IsDedekindDomainInv✝ A → IsIntegrallyClosed A
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow_zero : ∀ {o : ONote}, o.NFBelow 0 ↔ o = 0
-- Mathlib.Topology.Order.LeftRightNhds
/-- In a linearly ordered additive commutative group with the order
topology, if `f` tends to `atTop` and `g` tends to `C` then `f + g` tends to `atTop`.  -/
Filter.Tendsto.atTop_add : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddCommGroup α] [inst_2 : LinearOrder α]
  [IsOrderedAddMonoid α] [OrderTopology α] {l : Filter β} {f g : β → α} {C : α},
  Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l (nhds C) → Filter.Tendsto (fun x => f x + g x) l Filter.atTop
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_modify_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k : α} {f : β k → β k}, (m.modify k f).getKey! k = if k ∈ m then k else default
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeHaveIdDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Order.OrderClosed
Icc_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderClosedTopology α] {a b x : α},
  a < x → x < b → Set.Icc a b ∈ nhds x
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.FixPoint.resetModified : Lean.Elab.Term.MutualClosure.FixPoint.M Unit
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.stateful.sizeOf_spec : ∀ (h : Lean.TSyntax `Lean.binderIdent), sizeOf (Lean.Parser.Tactic.MRefinePat.stateful h) = 1 + sizeOf h
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
_private.Mathlib.MeasureTheory.Integral.Bochner.Basic.0.MeasureTheory.«term_→ₛ_» : Lean.TrailingParserDescr
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfDom_comp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {T : Submonoid P} {k : M ≃* P}
  (H : Submonoid.map k.symm.toMonoidHom T = S) (x : M), (f.ofMulEquivOfDom H) (k x) = f x
-- Mathlib.Order.Hom.Basic
OrderIso.ofRelIsoLT_toRelIsoLT : ∀ {α : Type u_6} {β : Type u_7} [inst : PartialOrder α] [inst_1 : PartialOrder β] (e : α ≃o β),
  OrderIso.ofRelIsoLT e.toRelIsoLT = e
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.hasShift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.ObjectProperty C) →
      {A : Type u_2} →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] →
            [P.IsStableUnderShift A] → CategoryTheory.HasShift P.FullSubcategory A
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The pair `f g : A ⟶ B` is coreflexive if there is a morphism `B ⟶ A` which is a retraction for both.
 -/
CategoryTheory.IsCoreflexivePair : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {A B : C} → (A ⟶ B) → (A ⟶ B) → Prop
-- Mathlib.Order.Category.DistLat
DistLat.coe_comp : ∀ {X Y Z : DistLat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Init.Data.Float.Model.Float32
/-- Compute the difference of two `Float32.Model`.
 -/
Float32.Model.sub : Float32.Model → Float32.Model → Float32.Model
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- The scalar multiplication of two `C^n` functions on a domain is `C^n`.  -/
ContDiffOn.smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}
  {𝕜' : Type u_3} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F] [IsBoundedSMul 𝕜' F]
  [IsScalarTower 𝕜 𝕜' F] {s : Set E} {f : E → 𝕜'} {g : E → F},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (f • g) s
-- Std.Data.Iterators.Lemmas.Combinators.Drop
_private.Std.Data.Iterators.Lemmas.Combinators.Drop.0.Std.Iter.step_drop.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (k : ℕ) (h_1 : Unit → motive 0) (h_2 : (k : ℕ) → motive k.succ),
  (match k.succ with
    | 0 => h_1 ()
    | k.succ => h_2 k) =
    h_2 k
-- Init.Data.String.Basic
String.Slice.Pos.next.congr_simp : ∀ {s : String.Slice} (pos pos_1 : s.Pos) (e_pos : pos = pos_1) (h : pos ≠ s.endPos), pos.next h = pos_1.next ⋯
-- Init.Data.SInt.Lemmas
Int8.toInt_ofInt_of_le : ∀ {n : ℤ}, -2 ^ 7 ≤ n → n < 2 ^ 7 → (Int8.ofInt n).toInt = n
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.instSemilatticeInf : (R : Type u_1) → [inst : NonUnitalNonAssocRing R] → SemilatticeInf (TwoSidedIdeal R)
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E}, VectorField.lieBracketWithin 𝕜 V W Set.univ = VectorField.lieBracket 𝕜 V W
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.ι_t_app_apply : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι}
  [inst_1 : P.IsProper] {j : ι} (c : f.Cell j) (x : SimplexCategoryᵒᵖ) (x_1 : c.horn.toSSet.obj x),
  (CategoryTheory.ConcreteCategory.hom ((f.t j).app x))
      ((CategoryTheory.ConcreteCategory.hom (c.ιSigmaHorn.app x)) x_1) =
    (CategoryTheory.ConcreteCategory.hom ((SSet.Subcomplex.Pairing.RankFunction.Cell.mapHorn f c).app x)) x_1
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Pushforward a zero-preserving scalar multiplication along a zero-preserving map.
See note [reducible non-instances].  -/
ZeroHom.smulZeroClass : {M : Type u_1} →
  {A : Type u_7} →
    {B : Type u_9} →
      [inst : Zero A] →
        [inst_1 : SMulZeroClass M A] →
          [inst_2 : Zero B] →
            [inst_3 : SMul M B] → (f : ZeroHom A B) → (∀ (c : M) (x : A), f (c • x) = c • f x) → SMulZeroClass M B
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.getD_eq_of_contains : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α],
  m.WF → ∀ {k fallback : α}, m.contains k = true → m.getD k fallback = k
-- Init.Data.Nat.Lemmas
/-- Dependent version of `decidableExistsLE`.  -/
Nat.decidableExistsLE' : {k : ℕ} →
  {p : (m : ℕ) → m ≤ k → Prop} → [I : (m : ℕ) → (h : m ≤ k) → Decidable (p m h)] → Decidable (∃ m, ∃ (h : m ≤ k), p m h)
-- Init.Data.SInt.Lemmas
Int32.le_minValue_iff : ∀ {a : Int32}, a ≤ Int32.minValue ↔ a = Int32.minValue
-- Init.Conv
/-- * `unfold id` unfolds all occurrences of definition `id` in the target.
* `unfold id1 id2 ...` is equivalent to `unfold id1; unfold id2; ...`.

Definitions can be either global or local definitions.

For non-recursive global definitions, this tactic is identical to `delta`.
For recursive global definitions, it uses the "unfolding lemma" `id.eq_def`,
which is generated for each recursive definition, to unfold according to the recursive definition given by the user.
Only one level of unfolding is performed, in contrast to `simp only [id]`, which unfolds definition `id` recursively.

This is the `conv` version of the `unfold` tactic.
 -/
Lean.Parser.Tactic.Conv.unfold : Lean.ParserDescr
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_coe : ∀ (r : NNReal), ⌊↑r⌋ₑ = ↑⌊r⌋₊
-- Mathlib.MeasureTheory.SetAlgebra
/-- The measurable space generated by a family of sets `𝒜` is the same as the one generated
by the algebra of sets generated by `𝒜`.  -/
MeasureTheory.generateFrom_generateSetAlgebra_eq : ∀ {α : Type u_1} {𝒜 : Set (Set α)},
  MeasurableSpace.generateFrom (MeasureTheory.generateSetAlgebra 𝒜) = MeasurableSpace.generateFrom 𝒜
-- Mathlib.Order.Interval.Finset.SuccPred
Finset.Ico_succ_succ_eq_Ioc_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : SuccOrder α] {b : α},
  ¬IsMax b → ∀ (a : α), Finset.Ico (Order.succ a) (Order.succ b) = Finset.Ioc a b
-- Mathlib.Topology.UnitInterval
unitInterval.strictAnti_symm : StrictAnti unitInterval.symm
-- Aesop.Tracing
Aesop.TraceOption.isEnabled : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → Aesop.TraceOption → m Bool
-- Mathlib.Data.Set.Subsingleton
Set.nontrivial_iff_exists_ne : ∀ {α : Type u} {s : Set α} {x : α}, x ∈ s → (s.Nontrivial ↔ ∃ y ∈ s, y ≠ x)
-- Mathlib.Algebra.Group.Units.Equiv
Units.mulLeft_apply : ∀ {M : Type u_3} [inst : Monoid M] (u : Mˣ), ⇑u.mulLeft = fun x => ↑u * x
-- Mathlib.Topology.Algebra.Order.Field
Homeomorph.mulLeft₀.congr_simp : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : GroupWithZero α] [inst_2 : SeparatelyContinuousMul α] (c c_1 : α)
  (e_c : c = c_1) (hc : c ≠ 0), Homeomorph.mulLeft₀ c hc = Homeomorph.mulLeft₀ c_1 ⋯
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_of_subsingleton : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} [Subsingleton R], p.natDegree = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_diff!_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true →
          Std.DTreeMap.Internal.Impl.Const.getD (m₁.diff! m₂) k fallback = fallback
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.QuasicoherentData.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R} {I : Type w} {X : I → C}
  {coversTop : J.CoversTop X} {presentation : (i : I) → (M.over (X i)).Presentation} {I_1 : Type w} {X_1 : I_1 → C}
  {coversTop_1 : J.CoversTop X_1} {presentation_1 : (i : I_1) → (M.over (X_1 i)).Presentation},
  { I := I, X := X, coversTop := coversTop, presentation := presentation } =
      { I := I_1, X := X_1, coversTop := coversTop_1, presentation := presentation_1 } →
    I = I_1 ∧ X ≍ X_1 ∧ presentation ≍ presentation_1
-- Mathlib.Order.RelClasses
/-- Set notation form of `eq_of_le_of_not_lt` -/
eq_of_subset_of_not_ssubset : ∀ {α : Type u_2} [UsesSetNotationForOrder α] [inst : PartialOrder α] {a b : α}, a ⊆ b → ¬a ⊂ b → a = b