mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Category.Preorder
OrderHom.equivFunctor_symm_apply : ∀ {X : Type u} {Y : Type v} [inst : Preorder X] [inst_1 : Preorder Y] (F : CategoryTheory.Functor X Y),
  OrderHom.equivFunctor.symm F = F.toOrderHom
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Basic.0.Std.Tactic.BVDecide.BVExpr.toString.match_1.eq_3 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (len w start : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w)
  (h_1 : (w idx : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var idx))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_4 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) → (rhs : Std.Tactic.BVDecide.BVExpr w) → motive w (lhs.bin op rhs))
  (h_5 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (operand : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op operand))
  (h_6 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_7 :
    (w w_1 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_1) →
        (h : w = w_1 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match len, Std.Tactic.BVDecide.BVExpr.extract start len expr with
    | w, Std.Tactic.BVDecide.BVExpr.var idx => h_1 w idx
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_3 len w start expr
    | w, lhs.bin op rhs => h_4 w lhs op rhs
    | w, Std.Tactic.BVDecide.BVExpr.un op operand => h_5 w op operand
    | w, lhs.append rhs h => h_6 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_7 w w_1 n expr h
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_3 len w start expr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₂ → (t₁ \ t₂).getKey? k = t₁.getKey? k
-- Mathlib.Algebra.Order.Star.Basic
StarOrderedRing.pos_iff : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {x : R}, 0 < x ↔ x ≠ 0 ∧ x ∈ AddSubmonoid.closure (Set.range fun s => star s * s)
-- Init.Data.Nat.Div.Basic
Nat.mod_eq_of_lt : ∀ {a b : ℕ}, a < b → a % b = a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₂_of_char_three : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) [CharP R 3], W.b₂ = W.a₁ ^ 2 + W.a₂
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
/-- Any left rigid category is monoidal closed, with the internal hom `X ⟶[C] Y = ᘁX ⊗ Y`.
This has to be a definition rather than an instance to avoid diamonds, for example between
`category_theory.monoidal_closed.functor_category` and
`CategoryTheory.Monoidal.leftRigidFunctorCategory`. Moreover, in concrete applications there is
often a more useful definition of the internal hom object than `ᘁY ⊗ X`, in which case the monoidal
closed structure shouldn't come the rigid structure (e.g. in the category `FinVect k`, it is more
convenient to define the internal hom as `Y →ₗ[k] X` rather than `ᘁY ⊗ X` even though these are
naturally isomorphic).  -/
CategoryTheory.monoidalClosedOfLeftRigidCategory : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.LeftRigidCategory C] → CategoryTheory.MonoidalClosed C
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
tsum_eq_of_filter_le : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} [T2Space α]
  {L₁ L₂ : SummationFilter β} [L₁.NeBot],
  L₁.filter ≤ L₂.filter → Summable f L₂ → ∑'[L₁] (b : β), f b = ∑'[L₂] (b : β), f b
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofIsoComp_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {X' : C} (g : X' ⟶ X)
  [inst_1 : CategoryTheory.IsIso g]
  (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp g f)),
  (CategoryTheory.Limits.MonoFactorisation.ofIsoComp g F).e =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.inv g) F.e
-- Init.Core
true_imp_iff : ∀ {α : Prop}, True → α ↔ α
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.restrictStalkIso_inv_eq_germ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {U : TopCat}
  (X : AlgebraicGeometry.PresheafedSpace C) {f : U ⟶ ↑X}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) (V : TopologicalSpace.Opens ↑U) (x : ↑U)
  (hx : x ∈ V) {Z : C} (h_1 : (X.restrict h).presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.germ (h.functor.obj V) ((CategoryTheory.ConcreteCategory.hom f) x) ⋯)
      (CategoryTheory.CategoryStruct.comp (X.restrictStalkIso h x).inv h_1) =
    CategoryTheory.CategoryStruct.comp ((X.restrict h).presheaf.germ V x hx) h_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr_algebraMap : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (r : R),
  ((CliffordAlgebra.foldr Q f hf) n) ((algebraMap R (CliffordAlgebra Q)) r) = r • n
-- Mathlib.Topology.Homotopy.TopCat.Basic
TopCat.Homotopy.ι₀_h : ∀ {X Y : TopCat} {f₀ f₁ : X ⟶ Y} (F : TopCat.Homotopy f₀ f₁), CategoryTheory.CategoryStruct.comp TopCat.ι₀ F.h = f₀
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.mk_algebraMap : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A}
  (r : R) (hr : (algebraMap R A) r ∈ S), ⟨(algebraMap R A) r, hr⟩ = (algebraMap R ↥S) r
-- Init.Data.SInt.Lemmas
Int32.toInt_bmod_size : ∀ (a : Int32), a.toInt.bmod Int32.size = a.toInt
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.isPell_mul : ∀ {d : ℤ} {b c : ℤ√d}, Pell.IsPell b → Pell.IsPell c → Pell.IsPell (b * c)
-- Mathlib.Order.SuccPred.Basic
PredOrder.ofLinearWellFoundedGT.eq_1 : ∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedGT α],
  PredOrder.ofLinearWellFoundedGT α =
    PredOrder.ofCore (fun a => if h : (Set.Iio a).Nonempty then ⋯.min (Set.Iio a) h else a) ⋯ ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
SSet.homologyMap_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X Y Z : SSet) (f : X ⟶ Y) (g : Y ⟶ Z) (R : C)
  [inst_3 : CategoryTheory.CategoryWithHomology C] (n : ℕ),
  SSet.homologyMap (CategoryTheory.CategoryStruct.comp f g) R n =
    CategoryTheory.CategoryStruct.comp (SSet.homologyMap f R n) (SSet.homologyMap g R n)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.map_updateRow : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {i : m} {b : n → α} [inst : DecidableEq m]
  (f : α → β), (M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b)
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.Iso.map_hom_inv_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : C} (e : X ≅ Y)
  (F : CategoryTheory.Functor C (CategoryTheory.Functor D E)) (Z : D),
  CategoryTheory.CategoryStruct.comp ((F.map e.hom).app Z) ((F.map e.inv).app Z) =
    CategoryTheory.CategoryStruct.id ((F.obj X).obj Z)
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
UniformContinuous.sub : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α]
  [inst_3 : UniformSpace β] {f g : β → α},
  UniformContinuous f → UniformContinuous g → UniformContinuous fun x => f x - g x
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.nndist_le_opNNNorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜₂] [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F) (x y : E), nndist (f x) (f y) ≤ ‖f‖₊ * nndist x y
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
/-- The cokernel of `Φ.ι : Φ.r ⟶ 𝟭 C`.  -/
CategoryTheory.Abelian.Preradical.quotient : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [CategoryTheory.Abelian C] → CategoryTheory.Abelian.Preradical C → CategoryTheory.Functor C C
-- Mathlib.Algebra.Ring.Basic
isRightRegular_iff_left_eq_zero_of_mul : ∀ {R : Type u_3} [inst : NonUnitalNonAssocRing R] {r : R}, IsRightRegular r ↔ ∀ (x : R), x * r = 0 → x = 0
-- Mathlib.LinearAlgebra.Dual.Lemmas
LinearMap.id_separatingRight : ∀ {K : Type u_1} {V : Type u_2} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], LinearMap.id.SeparatingRight
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
/-- Extension for the `positivity` tactic: the von Mangoldt function is nonnegative.  -/
Mathlib.Meta.Positivity.evalVonMangoldt : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.RingTheory.AdicCompletion.Noetherian
IsHausdorff.of_isDomain : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [IsNoetherianRing R] [IsDomain R], I ≠ ⊤ → IsHausdorff I R
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- For `P` a property of ring homomorphisms, `sourceAffineLocally P` holds for `f : X ⟶ Y`
whenever `P` holds for the restriction of `f` on every affine open subset of `X`.  -/
AlgebraicGeometry.sourceAffineLocally : ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  AlgebraicGeometry.AffineTargetMorphismProperty
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.Hom.mk.inj : ∀ {R : Type u} {inst : Semiring R} {M N : SemimoduleCat R} {hom' hom'_1 : ↑M →ₗ[R] ↑N},
  { hom' := hom' } = { hom' := hom'_1 } → hom' = hom'_1
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.T.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ), LaurentPolynomial.T n = AddMonoidAlgebra.single n 1
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.inclusion_id_assoc : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) {Z : AlgebraicGeometry.Scheme} (h : I.subscheme ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.inclusion ⋯) h = h
-- Std.Data.DTreeMap.Internal.Operations
/-- Builds the tree `l ++ ⟨k, v⟩ ++ r` without any balancing information at the root.  -/
Std.DTreeMap.Internal.Impl.link : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k →
        (l r : Std.DTreeMap.Internal.Impl α β) →
          l.Balanced → r.Balanced → Std.DTreeMap.Internal.Impl.Tree α β (l.size + 1 + r.size)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.lift_comp_inl : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] [inst_2 : AddMonoid P]
  (f : M →+ P) (g : N →+ P), (AddMonoid.Coprod.lift f g).comp AddMonoid.Coprod.inl = f
-- Mathlib.Algebra.BigOperators.Finprod
finsum_mem_support : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M),
  ∑ᶠ (a : α) (_ : a ∈ Function.support f), f a = ∑ᶠ (a : α), f a
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'Map_id : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i'],
  HomologicalComplex.truncLE'Map (CategoryTheory.CategoryStruct.id K) e =
    CategoryTheory.CategoryStruct.id (K.truncLE' e)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.Equiv.of_keysArray_perm : ∀ {α : Type u} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit}, t₁.keysArray.Perm t₂.keysArray → t₁.Equiv t₂
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitUncurryIsoColimitCompColim_ι_hom : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit (CategoryTheory.Functor.uncurry.obj F)]
  [inst_5 : CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.Limits.colim)] {j : J} {k : K},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (CategoryTheory.Functor.uncurry.obj F) (j, k))
      (CategoryTheory.Limits.colimitUncurryIsoColimitCompColim F).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.obj j) k)
      (CategoryTheory.Limits.colimit.ι (F.comp CategoryTheory.Limits.colim) j)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_zero_set : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}, μ s = 0 → μ.restrict s = 0
-- Mathlib.Order.Disjoint
disjoint_of_subsingleton : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α} [Subsingleton α], Disjoint a b
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The zero morphism of an additive monoid object.  -/
CategoryTheory.AddMonObj.«termζ[_]» : Lean.ParserDescr
-- Mathlib.GroupTheory.NoncommPiCoprod
MonoidHom.noncommPiCoprod.congr_simp : ∀ {M : Type u_1} [inst : Monoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → Monoid (N i)] (ϕ ϕ_1 : (i : ι) → N i →* M) (e_ϕ : ϕ = ϕ_1)
  (hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)),
  MonoidHom.noncommPiCoprod ϕ hcomm = MonoidHom.noncommPiCoprod ϕ_1 ⋯
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_self_conj : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : E), (starRingEnd 𝕜) (inner 𝕜 x x) = inner 𝕜 x x
-- Init.Prelude
/-- The homogeneous version of `HDiv`: `a / b : α` where `a b : α`.  -/
Div : Type u → Type u
-- Init.Data.Nat.Compare
Nat.instLawfulOrderOrd : Std.LawfulOrderOrd ℕ
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.ground_id : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  PolynomialLaw.id.ground = id
-- Mathlib.Topology.LocallyConstant.Basic
IsLocallyConstant.neg : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : Neg Y] ⦃f : X → Y⦄,
  IsLocallyConstant f → IsLocallyConstant (-f)
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.State.mk.sizeOf_spec : ∀ (visitedLevel : Lean.LevelSet) (visitedExpr : Lean.ExprSet) (params : Array Lean.Name),
  sizeOf { visitedLevel := visitedLevel, visitedExpr := visitedExpr, params := params } =
    1 + sizeOf visitedLevel + sizeOf visitedExpr + sizeOf params
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.mgf_dirac' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {t : ℝ} [MeasurableSingletonClass Ω] {ω : Ω},
  ProbabilityTheory.mgf X (MeasureTheory.Measure.dirac ω) t = Real.exp (t * X ω)
-- Mathlib.Analysis.Calculus.FDeriv.RestrictScalars
DifferentiableWithinAt.restrictScalars_fderivWithin : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {E : Type u_3} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E]
  [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E] {F : Type u_4} [inst_7 : NormedAddCommGroup F]
  [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F] [inst_10 : IsScalarTower 𝕜 𝕜' F] {f : E → F} {s : Set E}
  {x : E},
  DifferentiableWithinAt 𝕜' f s x →
    UniqueDiffWithinAt 𝕜 s x → ContinuousLinearMap.restrictScalars 𝕜 (fderivWithin 𝕜' f s x) = fderivWithin 𝕜 f s x
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.instCoeFunPresieve : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → CoeFun (CategoryTheory.Sieve X) fun x => CategoryTheory.Presieve X
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.C.eq_1 : ∀ {R : Type u_1} [inst : Semiring R], LaurentPolynomial.C = AddMonoidAlgebra.singleZeroRingHom
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.restrict_dirac : ∀ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {s : Set α} {x : α} {m : M},
  MeasurableSet s →
    ∀ [inst_2 : Decidable (x ∈ s)],
      (MeasureTheory.VectorMeasure.dirac x m).restrict s = if x ∈ s then MeasureTheory.VectorMeasure.dirac x m else 0
-- Mathlib.RingTheory.Flat.Stability
Module.Flat.ulift_left_iff : ∀ {R : Type u} {M : Type w} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.Flat (ULift.{t, u} R) M ↔ Module.Flat R M
-- Mathlib.CategoryTheory.Functor.Currying
/-- The flipped equivalence of types of bifunctors given by currying.  -/
CategoryTheory.Functor.curryingFlipEquiv : {C : Type u₂} →
  [inst : CategoryTheory.Category.{v₂, u₂} C] →
    {D : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} D] →
        {E : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} E] →
            CategoryTheory.Functor D (CategoryTheory.Functor C E) ≃ CategoryTheory.Functor (C × D) E
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.CofibrantBrownFactorization.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : HomotopicalAlgebra.ModelCategory C} {X Y : C}
  {f : X ⟶ Y}
  {toMapFactorizationData :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f}
  {s : Y ⟶ toMapFactorizationData.Z}
  {s_p :
    autoParam (CategoryTheory.CategoryStruct.comp s toMapFactorizationData.p = CategoryTheory.CategoryStruct.id Y)
      HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam}
  {cofibration_s :
    autoParam (HomotopicalAlgebra.Cofibration s)
      HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam}
  {toMapFactorizationData_1 :
    (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f}
  {s_1 : Y ⟶ toMapFactorizationData_1.Z}
  {s_p_1 :
    autoParam (CategoryTheory.CategoryStruct.comp s_1 toMapFactorizationData_1.p = CategoryTheory.CategoryStruct.id Y)
      HomotopicalAlgebra.CofibrantBrownFactorization.s_p._autoParam}
  {cofibration_s_1 :
    autoParam (HomotopicalAlgebra.Cofibration s_1)
      HomotopicalAlgebra.CofibrantBrownFactorization.cofibration_s._autoParam},
  { toMapFactorizationData := toMapFactorizationData, s := s, s_p := s_p, cofibration_s := cofibration_s } =
      { toMapFactorizationData := toMapFactorizationData_1, s := s_1, s_p := s_p_1, cofibration_s := cofibration_s_1 } →
    toMapFactorizationData = toMapFactorizationData_1 ∧ s ≍ s_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.IntegrationByParts
/-- The integral of the derivative of a product of two maps.
Special case of `integral_deriv_mul_eq_sub_of_hasDeriv_right` where the functions have a
two-sided derivative in the interior of the interval.  -/
intervalIntegral.integral_deriv_mul_eq_sub_of_hasDerivAt : ∀ {a b : ℝ} {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] [CompleteSpace A] {u v u' v' : ℝ → A},
  ContinuousOn u (Set.uIcc a b) →
    ContinuousOn v (Set.uIcc a b) →
      (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt u (u' x) x) →
        (∀ x ∈ Set.Ioo (min a b) (max a b), HasDerivAt v (v' x) x) →
          IntervalIntegrable u' MeasureTheory.volume a b →
            IntervalIntegrable v' MeasureTheory.volume a b →
              ∫ (x : ℝ) in a..b, u' x * v x + u x * v' x = u b * v b - u a * v a
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofNatTruncate_of_lt : ∀ {n : ℕ}, n < UInt8.size → (UInt8.ofNatClamp n).toNat = n
-- Init.Data.Int.Gcd
Int.gcd_dvd_right : ∀ (a b : ℤ), ↑(a.gcd b) ∣ b
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.instIsPreimmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f],
  AlgebraicGeometry.IsPreimmersion f
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkInductiveAux₁.eq_2 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : ChainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 0 ⟶ Q.X 1) (one : P.X 1 ⟶ Q.X 2)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp (P.d 1 0) zero + CategoryTheory.CategoryStruct.comp one (Q.d 2 1))
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X n ⟶ Q.X (n + 1)) ×'
            (f' : P.X (n + 1) ⟶ Q.X (n + 2)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp (P.d (n + 1) n) f +
                  CategoryTheory.CategoryStruct.comp f' (Q.d (n + 2) (n + 1))) →
        (f'' : P.X (n + 2) ⟶ Q.X (n + 3)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 1)) p.snd.fst +
              CategoryTheory.CategoryStruct.comp f'' (Q.d (n + 3) (n + 2))),
  Homotopy.mkInductiveAux₁ e zero one comm_one succ 1 = ⟨one, ⟨(succ 0 ⟨zero, ⟨one, comm_one⟩⟩).fst, ⋯⟩⟩
-- Mathlib.Data.Finset.Sort
/-- An order embedding `f` from `Fin k` to a finset of cardinality `k` has to coincide with
the increasing bijection `orderEmbOfFin s h`.  -/
Finset.orderEmbOfFin_unique' : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Finset α} {k : ℕ} (h : s.card = k) {f : Fin k ↪o α},
  (∀ (x : Fin k), f x ∈ s) → f = s.orderEmbOfFin h
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.mk.eq_1 : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : CommGroupWithZero B] (f : A →*₀ B)
  [inst_2 : DecidablePred fun b => b = 0] (r s : A),
  MonoidWithZeroHom.ValueGroup₀.mk f r s =
    if h : f r = 0 ∨ f s = 0 then 0 else ↑(MonoidWithZeroHom.valueGroup.mk f r s ⋯ ⋯)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.leftHomologyMap'_congr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.ShortComplex.leftHomologyMap' φ₁ h₁ h₂ = CategoryTheory.ShortComplex.leftHomologyMap' φ₂ h₁ h₂
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.usize.sizeOf_spec : sizeOf Lean.IR.IRType.usize = 1
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.instAdditiveShift : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] [inst_5 : CategoryTheory.Preadditive C]
  [inst_6 : CategoryTheory.Preadditive A] [F.Additive] [∀ (n : M), (CategoryTheory.shiftFunctor C n).Additive] (n : M),
  (F.shift n).Additive
-- Std.Data.HashSet.Lemmas
Std.HashSet.toArray_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α}, m.toList.toArray = m.toArray