mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
CategoryTheory.instReflectsLimitsOfShapeFunctorObjWhiskeringRightOfHasLimitsOfShapeOfReflectsIsomorphismsOfPreservesLimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  {J : Type u_4} [inst_3 : CategoryTheory.Category.{v_4, u_4} J] [CategoryTheory.Limits.HasLimitsOfShape J D]
  (F : CategoryTheory.Functor D E) [F.ReflectsIsomorphisms] [CategoryTheory.Limits.PreservesLimitsOfShape J F],
  CategoryTheory.Limits.ReflectsLimitsOfShape J ((CategoryTheory.Functor.whiskeringRight C D E).obj F)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.foldl_eq_foldl_toList : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β} {δ : Type w} {f : δ → (a : α) → β a → δ}
  {init : δ}, Std.DTreeMap.Internal.Impl.foldl f init t = List.foldl (fun a b => f a b.fst b.snd) init t.toList
-- Mathlib.Algebra.Group.Submonoid.Finsupp
/-- A variant of `Submonoid.mem_closure_finset` using `s` as the index type.  -/
Submonoid.mem_closure_finset' : ∀ {M : Type u_1} [inst : CommMonoid M] {x : M} {s : Finset M}, x ∈ Submonoid.closure ↑s ↔ ∃ a, x = ∏ i, ↑i ^ a i
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
EisensteinSeries.gammaSet_div_gcd : ∀ {r : ℕ} {v : Fin 2 → ℤ}, v ∈ EisensteinSeries.gammaSet 1 r 0 → ∀ (i : Fin 2), ↑r ∣ v i
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.of_mem_support_derivative : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, n ∈ (Polynomial.derivative p).support → n + 1 ∈ p.support
-- Mathlib.CategoryTheory.MorphismProperty.Comma
/-- Construct a morphism in `P.CostructuredArrow Q F X` by giving a morphism on the underlying
objects of `C`.  -/
CategoryTheory.MorphismProperty.CostructuredArrow.homMk : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} D] →
        {P : CategoryTheory.MorphismProperty D} →
          {Q : CategoryTheory.MorphismProperty C} →
            [inst_2 : Q.IsMultiplicative] →
              {F : CategoryTheory.Functor C D} →
                {X : D} →
                  {A B : P.CostructuredArrow Q F X} →
                    (f : A.left ⟶ B.left) →
                      Q f →
                        autoParam (CategoryTheory.CategoryStruct.comp (F.map f) B.hom = A.hom)
                            CategoryTheory.MorphismProperty.CostructuredArrow.homMk._auto_1 →
                          (A ⟶ B)
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.curry'_whiskerRight_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y Z : C}
  [inst_2 : CategoryTheory.Closed X] [inst_3 : CategoryTheory.Closed Y] (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalClosed.curry' f) (Y ⟹ Z))
      (CategoryTheory.MonoidalClosed.comp X Y Z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Y ⟹ Z)).hom
      ((CategoryTheory.MonoidalClosed.pre f).app Z)
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
/-- If `u` is a neighborhood of `x`, then for small enough `r`, the open ball
`Metric.ball x r` is contained in `u`.  -/
eventually_ball_subset : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] {x : α} {u : Set α},
  u ∈ nhds x → ∀ᶠ (r : ℝ) in nhds 0, Metric.ball x r ⊆ u
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.isScalarTower : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {α : Type v} [inst : SMul R S] [inst_1 : SMul R α]
  [inst_2 : SMul S α] [IsScalarTower R S α], IsScalarTower R S (Matrix m n α)
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.InfoCacheKey.mk : UInt64 → Lean.Expr → Option ℕ → Lean.Meta.InfoCacheKey
-- Aesop.Util.Basic
_private.Aesop.Util.Basic.0.Aesop.addTryThisTacticSeqSuggestion.dedent : String → String
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xn_modEq_x2n_sub_lem : ∀ {a : ℕ} (a1 : 1 < a) {n j : ℕ}, j ≤ n → Pell.xn a1 (2 * n - j) + Pell.xn a1 j ≡ 0 [MOD Pell.xn a1 n]
-- Mathlib.RingTheory.GradedAlgebra.RingHom
map_directSumDecompose : ∀ {ι : Type u_1} {A : Type u_2} {B : Type u_3} {σ : Type u_6} {τ : Type u_7} [inst : Semiring A] [inst_1 : Semiring B]
  [inst_2 : SetLike σ A] [inst_3 : SetLike τ B] [inst_4 : DecidableEq ι] [inst_5 : AddMonoid ι]
  [inst_6 : AddSubmonoidClass σ A] [inst_7 : AddSubmonoidClass τ B] (𝒜 : ι → σ) (ℬ : ι → τ) [inst_8 : GradedRing 𝒜]
  [inst_9 : GradedRing ℬ] {F : Type u_10} [inst_10 : FunLike F A B] [GradedFunLike F 𝒜 ℬ] [RingHomClass F A B] (f : F)
  {x : A} {i : ι}, f ↑(((DirectSum.decompose 𝒜) x) i) = ↑(((DirectSum.decompose ℬ) (f x)) i)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.smulRight_comp_smulRight : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  {M₂ : Type u_6} [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₁ M₁]
  [inst_6 : Module R₁ M₂] [inst_7 : TopologicalSpace R₁] [inst_8 : ContinuousSMul R₁ M₂] {M₃ : Type u_9}
  [inst_9 : AddCommMonoid M₃] [inst_10 : Module R₁ M₃] [inst_11 : TopologicalSpace M₃] [inst_12 : ContinuousSMul R₁ M₃]
  (f : M₃ →L[R₁] R₁) (g : M₁ →L[R₁] R₁) {x : M₂} {y : M₃}, f.smulRight x ∘SL g.smulRight y = g.smulRight (f y • x)
-- Mathlib.ModelTheory.Basic
/-- Used for defining `FirstOrder.Language.Theory.ModelType.instInhabited`.  -/
FirstOrder.Language.Inhabited.trivialStructure : (L : FirstOrder.Language) → {α : Type u_1} → [Inhabited α] → L.Structure α
-- Aesop.RuleTac.Basic
Aesop.Subgoal.mk.inj : ∀ {diff diff_1 : Aesop.GoalDiff}, { diff := diff } = { diff := diff_1 } → diff = diff_1
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_smul : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f : X → Y}
  {α : Type u_3} [inst_2 : NormedRing α] [inst_3 : Module α Y] [NormSMulClass α Y] (c : α),
  eHolderNorm r (c • f) = ↑‖c‖₊ * eHolderNorm r f
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
/-- In the 1-dimensional case, a set is Presburger arithmetic definable in `ℕ` if and only if it
is ultimately periodic, i.e. periodic after some number `k`.  -/
FirstOrder.Language.presburger.definable₁_iff_ultimately_periodic : ∀ {A s : Set ℕ}, A.Definable₁ FirstOrder.Language.presburger s ↔ ∃ k, ∃ p > 0, ∀ x ≥ k, x ∈ s ↔ x + p ∈ s
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
/-- To show two paths equal it suffices to show that they have the same edges.  -/
SSet.Path.ext' : ∀ {X : SSet} {n : ℕ} {f g : X.Path (n + 1)}, (∀ (i : Fin (n + 1)), f.arrow i = g.arrow i) → f = g
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inversion induced on the quotient by a congruence relation on a type with an
inversion.  -/
Con.hasInv : {M : Type u_1} → [inst : Group M] → (c : Con M) → Inv c.Quotient
-- Lean.Elab.Tactic.Simp
_private.Lean.Elab.Tactic.Simp.0.Lean.Elab.Tactic.instEvalExprConfig_1 : Lean.Elab.ConfigEval.EvalExpr Lean.Meta.DSimp.Config
-- Lean.Meta.Basic
/-- If `config.zetaDelta := false`, we may select specific local declarations to be unfolded using
the field `zetaDeltaSet`. Note that, we do not include this field in the `Config` structure
because this field is not taken into account while caching results.
Moreover, we reset all caches whenever setting it.
 -/
Lean.Meta.Context.zetaDeltaSet : Lean.Meta.Context → Lean.FVarIdSet
-- Mathlib.Tactic.Linter.TextBased
/-- Unicode variant selectors are used in a bad way.
* `s` is the string containing the unicode character and any unicode variant selector following it
* `selector` is the desired selector or `none`
 -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.StyleError.unicodeVariant : String → Option Char → Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_div_right_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulRightInvariant] (x : G), Filter.map (fun t => t / x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
-- Mathlib.Order.Atoms
IsSimpleOrder.bot_lt_iff_eq_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : BoundedOrder α] [IsSimpleOrder α] {a : α}, ⊥ < a ↔ a = ⊤
-- Mathlib.MeasureTheory.Integral.DivergenceTheorem
/-- An auxiliary lemma for
`MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable`. This is exactly
`BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt` reformulated for the
Bochner integral.  -/
_private.Mathlib.MeasureTheory.Integral.DivergenceTheorem.0.MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1)))
  (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → E)
  (s : Set (Fin (n + 1) → ℝ)),
  s.Countable →
    ContinuousOn f (BoxIntegral.Box.Icc I) →
      (∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x) →
        MeasureTheory.IntegrableOn (fun x => ∑ i, (f' x) (Pi.single i 1) i) (BoxIntegral.Box.Icc I)
            MeasureTheory.volume →
          ∫ (x : Fin (n + 1) → ℝ) in BoxIntegral.Box.Icc I, ∑ i, (f' x) (Pi.single i 1) i =
            ∑ i,
              ((∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -
                ∫ (x : Fin n → ℝ) in BoxIntegral.Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i)
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Precompose a partial equivalence with an equivalence.
We modify the source and target to have better definitional behavior.  -/
Equiv.transPartialEquiv : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → α ≃ β → PartialEquiv β γ → PartialEquiv α γ
-- Lean.LocalContext
/-- Given `lctx₁ - exceptFVars` of the form `(x_1 : A_1) ... (x_n : A_n)`, then return true
iff there is a local context `B_1* (x_1 : A_1) ... B_n* (x_n : A_n)` which is a prefix
of `lctx₂` where `B_i`'s are (possibly empty) sequences of local declarations.  -/
Lean.LocalContext.isSubPrefixOf : Lean.LocalContext → Lean.LocalContext → optParam (Array Lean.Expr) #[] → Bool
-- Init.Data.UInt.Lemmas
UInt16.toUSize_mod : ∀ (a b : UInt16), (a % b).toUSize = a.toUSize % b.toUSize
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.joinPoint.injEq : ∀ (a : Array Lean.IR.Param) (a_1 : Lean.IR.FnBody) (a_2 : Array Lean.IR.Param) (a_3 : Lean.IR.FnBody),
  (Lean.IR.LocalContextEntry.joinPoint a a_1 = Lean.IR.LocalContextEntry.joinPoint a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Init.Data.BitVec.Bitblast
BitVec.bit_neg_eq_neg : ∀ {w : ℕ} (x : BitVec w), -x = ((BitVec.iunfoldr (fun i c => (c, !x[↑i])) ()).2.adc (1#w) false).2
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.threeMore.sizeOf_spec : sizeOf ByteArray.utf8DecodeChar?.FirstByte.threeMore = 1
-- Mathlib.Algebra.Group.Semiconj.Units
/-- If `a` semiconjugates an additive unit `x` to an additive unit `y`, then it
semiconjugates `-x` to `-y`.  -/
AddSemiconjBy.addUnits_neg_right : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} {x y : AddUnits M}, AddSemiconjBy a ↑x ↑y → AddSemiconjBy a ↑(-x) ↑(-y)
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.instBEqStyleError : BEq Mathlib.Linter.TextBased.StyleError✝
-- Mathlib.Algebra.Module.Torsion.Basic
Module.IsTorsionBySet.mk_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R}
  [inst_3 : I.IsTwoSided] (hM : Module.IsTorsionBySet R M ↑I) (b : R) (x : M), (Ideal.Quotient.mk I) b • x = b • x
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
AlgebraicGeometry.instLocallyQuasiFiniteFstScheme : ∀ {X Y S : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) [AlgebraicGeometry.LocallyQuasiFinite g],
  AlgebraicGeometry.LocallyQuasiFinite (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instOne : {ι : Type u_1} → {M : ι → Type u_5} → [(i : ι) → One (M i)] → One ((i : ι) → M i)
-- Lean.Server.Requests
Lean.Server.RequestError.ofException : Lean.Exception → IO Lean.Server.RequestError
-- Mathlib.Probability.StrongLaw
ProbabilityTheory.truncation_eq_of_nonneg : ∀ {α : Type u_1} {f : α → ℝ} {A : ℝ},
  (∀ (x : α), 0 ≤ f x) → ProbabilityTheory.truncation f A = (Set.Ioc 0 A).indicator id ∘ f
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.natDegree_minpolyX : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K), (f.minpolyX ↥K⟮f⟯).natDegree = max f.num.natDegree f.denom.natDegree
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
/-- Here, we need that `Nat.card α` has at least `4` elements,
so that  either `t` has at least 3 elements, or `tᶜ` has at least 2.
The condition is necessary, because the result is wrong when
`α = {1, 2, 3}` and either `t = {1, 2}` or `t = {1}`.  -/
alternatingGroup.exists_mem_stabilizer_smul_eq : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α],
  4 ≤ Nat.card α → ∀ {t : Set α}, ∀ a ∈ t, ∀ b ∈ t, ∃ g ∈ MulAction.stabilizer (↥(alternatingGroup α)) t, g • a = b
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a left absorbing element for multiplication  -/
MulZeroClass.zero_mul : ∀ {M₀ : Type u} [self : MulZeroClass M₀] (a : M₀), 0 * a = 0
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.OptionT.orElse.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (x : Option α) (h_1 : (a : α) → motive (some a))
  (h_2 : (x : Option α) → motive x),
  (∀ (a : α), x = some a → False) →
    (match x with
      | some a => h_1 a
      | x => h_2 x) =
      h_2 x
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_sup : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [H.Characteristic] [K.Characteristic], (H ⊔ K).Characteristic
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
StarAlgHom.codRestrict.congr_simp : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B] [inst_7 : StarRing B]
  [inst_8 : StarModule R B] (f f_1 : A →⋆ₐ[R] B) (e_f : f = f_1) (S : StarSubalgebra R B) (hf : ∀ (x : A), f x ∈ S),
  f.codRestrict S hf = f_1.codRestrict S ⋯
-- Mathlib.Algebra.Algebra.Defs
Algebra.algebraMap_eq_smul_one' : ∀ {R : Type u} {A : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A],
  ⇑(algebraMap R A) = fun r => r • 1
-- Std.Sat.AIG.Basic
/-- In order to be a valid AIG, `decls` must form a DAG.
 -/
Std.Sat.AIG.hdag : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] (self : Std.Sat.AIG α), Std.Sat.AIG.IsDAG α self.decls
-- Mathlib.Order.Fin.Tuple
Fin.snocOrderIso_toEquiv : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)],
  (Fin.snocOrderIso α).toEquiv = Fin.snocEquiv α
-- Mathlib.Order.Hom.CompleteLattice
FrameHom.mk.injEq : ∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (toInfTopHom : InfTopHom α β)
  (map_sSup' : ∀ (s : Set α), toInfTopHom.toFun (sSup s) = sSup (toInfTopHom.toFun '' s))
  (toInfTopHom_1 : InfTopHom α β)
  (map_sSup'_1 : ∀ (s : Set α), toInfTopHom_1.toFun (sSup s) = sSup (toInfTopHom_1.toFun '' s)),
  ({ toInfTopHom := toInfTopHom, map_sSup' := map_sSup' } =
      { toInfTopHom := toInfTopHom_1, map_sSup' := map_sSup'_1 }) =
    (toInfTopHom = toInfTopHom_1)
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.leftMulMapPreGNS_apply : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) [inst_2 : StarOrderedRing A]
  (a : A) (x : f.PreGNS), (f.leftMulMapPreGNS a) x = f.toPreGNS (a * f.ofPreGNS x)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- Composition of pseudofunctors.  -/
CategoryTheory.Pseudofunctor.comp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Bicategory D] →
            CategoryTheory.Pseudofunctor B C → CategoryTheory.Pseudofunctor C D → CategoryTheory.Pseudofunctor B D
-- Lean.DocString.Syntax
/-- Paragraph  -/
Lean.Doc.Syntax.para : Lean.ParserDescr
-- Mathlib.Tactic.Linarith.Datatypes
/-- `Comp.add c1 c2` adds the expressions represented by `c1` and `c2`.
The coefficient of variable `a` in `c1.add c2`
is the sum of the coefficients of `a` in `c1` and `c2`.
 -/
Mathlib.Tactic.Linarith.Comp.add : Mathlib.Tactic.Linarith.Comp → Mathlib.Tactic.Linarith.Comp → Mathlib.Tactic.Linarith.Comp
-- Init.Data.Vector.Attach
Vector.unattach_replicate : ∀ {α : Type u_1} {p : α → Prop} {n : ℕ} {x : { x // p x }}, (Vector.replicate n x).unattach = Vector.replicate n ↑x
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_const_mul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {d : 𝕜 → 𝔸} (c : 𝔸),
  DifferentiableWithinAt 𝕜 d s x → derivWithin (fun y => c * d y) s x = c * derivWithin d s x
-- Mathlib.RingTheory.Ideal.Height
Ideal.finiteHeight_iff_lt : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R}, I.FiniteHeight ↔ I = ⊤ ∨ I.height < ⊤
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
MeasureTheory.MeasurablySeparable.iUnion : ∀ {ι : Type u_2} [Countable ι] {α : Type u_3} [inst : MeasurableSpace α] {s t : ι → Set α},
  (∀ (m n : ι), MeasureTheory.MeasurablySeparable (s m) (t n)) → MeasureTheory.MeasurablySeparable (⋃ n, s n) (⋃ m, t m)
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit_hom_whiskerLeft_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (G : CategoryTheory.Functor D K) [inst_4 : CategoryTheory.Limits.HasLimitsOfShape J C] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitCompWhiskeringLeftIsoCompLimit F G).hom
      (G.whiskerLeft (CategoryTheory.Limits.limit.π F j)) =
    CategoryTheory.Limits.limit.π (F.comp ((CategoryTheory.Functor.whiskeringLeft D K C).obj G)) j
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- Pullbacks distribute over universal coproducts in both arguments: This is the isomorphism
`∐ (Xᵢ ×[S] Xⱼ) ≅ (∐ Xᵢ) ×[S] (∐ Xⱼ)`.  -/
CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {ι' : Type u_4} {S : C} {X : ι → C}
  {a : CategoryTheory.Limits.Cofan X},
  CategoryTheory.IsUniversalColimit a →
    ∀ {Y : ι' → C} {b : CategoryTheory.Limits.Cofan Y},
      CategoryTheory.IsUniversalColimit b →
        ∀ (f : (i : ι) → X i ⟶ S) (g : (i : ι') → Y i ⟶ S) (u : a.pt ⟶ S) (v : b.pt ⟶ S)
          [∀ (i : ι), CategoryTheory.Limits.HasPullback (f i) v] {P : ι × ι' → C}
          {q₁ : (i : ι) → (j : ι') → P (i, j) ⟶ X i} {q₂ : (i : ι) → (j : ι') → P (i, j) ⟶ Y j},
          (∀ (i : ι) (j : ι'), CategoryTheory.IsPullback (q₁ i j) (q₂ i j) (f i) (g j)) →
            ∀ {Z : C} {p₁ : Z ⟶ a.pt} {p₂ : Z ⟶ b.pt},
              CategoryTheory.IsPullback p₁ p₂ u v →
                ∀ {d : CategoryTheory.Limits.Cofan P} (e : d.pt ≅ Z),
                  autoParam (∀ (i : ι), CategoryTheory.CategoryStruct.comp (a.inj i) u = f i)
                      CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback._auto_1 →
                    autoParam (∀ (i : ι'), CategoryTheory.CategoryStruct.comp (b.inj i) v = g i)
                        CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback._auto_3 →
                      autoParam
                          (∀ (i : ι) (j : ι'),
                            CategoryTheory.CategoryStruct.comp (d.inj (i, j))
                                (CategoryTheory.CategoryStruct.comp e.hom p₁) =
                              CategoryTheory.CategoryStruct.comp (q₁ i j) (a.inj i))
                          CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback._auto_5 →
                        autoParam
                            (∀ (i : ι) (j : ι'),
                              CategoryTheory.CategoryStruct.comp (d.inj (i, j))
                                  (CategoryTheory.CategoryStruct.comp e.hom p₂) =
                                CategoryTheory.CategoryStruct.comp (q₂ i j) (b.inj j))
                            CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback._auto_7 →
                          Nonempty (CategoryTheory.Limits.IsColimit d)
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Expr.denote.match_1.eq_5 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (k : ℕ) (a : Lean.Grind.Linarith.Expr)
  (h_1 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_2 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_3 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_4 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b))
  (h_5 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a))
  (h_6 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_7 : (a : Lean.Grind.Linarith.Expr) → motive a.neg),
  (match Lean.Grind.Linarith.Expr.natMul k a with
    | Lean.Grind.Linarith.Expr.zero => h_1 ()
    | Lean.Grind.Linarith.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_5 k a
    | Lean.Grind.Linarith.Expr.intMul k a => h_6 k a
    | a.neg => h_7 a) =
    h_5 k a
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
VectorPrebundle.mk_contMDiffCoordChange : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜]
  {EB : Type u_7} [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8}
  [inst_3 : TopologicalSpace HB] {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B]
  [inst_5 : ChartedSpace HB B] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace 𝕜 F] [inst_10 : (x : B) → TopologicalSpace (E x)]
  (a : VectorPrebundle 𝕜 F E) [ha : VectorPrebundle.IsContMDiff IB a n]
  {e e' : Bundle.Pretrivialization F Bundle.TotalSpace.proj} (he : e ∈ a.pretrivializationAtlas)
  (he' : e' ∈ a.pretrivializationAtlas) {b : B},
  b ∈ e.baseSet ∩ e'.baseSet →
    ∀ (v : F), (b, (VectorPrebundle.contMDiffCoordChange n IB a he he' b) v) = ↑e' ⟨b, e.symm b v⟩
-- Mathlib.Algebra.Order.Floor.Ring
Int.ceil_le_mul : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {a b : k},
  1 < b → ↑⌈(b - 1)⁻¹⌉ / b ≤ a → ↑⌈a⌉ ≤ b * a
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift.eq_1 : ∀ {X : SSet} (sx : X.StrictSegal) {n : ℕ}
  (s :
    CategoryTheory.Limits.Cone
      ((CategoryTheory.StructuredArrow.proj (Opposite.op { len := n }) (SimplexCategory.Truncated.inclusion 2).op).comp
        ((SimplexCategory.Truncated.inclusion 2).op.comp X)))
  (x : s.pt),
  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift sx s x =
    sx.spineToSimplex
      {
        vertex := fun i =>
          (CategoryTheory.ConcreteCategory.hom
              (s.π.app
                (CategoryTheory.StructuredArrow.mk
                  (((SimplexCategory.Truncated.inclusion 2).obj
                          (Opposite.unop
                            (Opposite.op
                              { obj := { len := 0 },
                                property := SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_2 }))).const
                      { len := n } i).op)))
            x,
        arrow := fun i =>
          (CategoryTheory.ConcreteCategory.hom
              (s.π.app (CategoryTheory.StructuredArrow.mk (SimplexCategory.mkOfLe i.castSucc i.succ ⋯).op)))
            x,
        arrow_src := ⋯, arrow_tgt := ⋯ }