mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Return an expression `sumFrom n lo f`  -/
Mathlib.Tactic.Determinant.Ctx.sumFrom : {u : Lean.Level} →
  {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → Mathlib.Tactic.Determinant.Ctx rα → ℕ → Q(ℕ → «$α») → Q(«$α»)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.HasModel.encode_inj : ∀ {α : Type u} [inst : LE α] [inst_1 : LT α] {β : Type v} [inst_2 : LE β] [inst_3 : LT β]
  [inst_4 : Std.PRange.UpwardEnumerable β] [inst_5 : Std.PRange.LawfulUpwardEnumerable β]
  [inst_6 : Std.PRange.LawfulUpwardEnumerableLE β] [inst_7 : Std.PRange.LawfulUpwardEnumerableLT β] [m : HasModel✝ α β]
  {x y : α}, HasModel.encode✝ x = HasModel.encode✝ y ↔ x = y
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.Result.step.injEq : ∀ (e' proof : Lean.Expr) (done contextDependent : Bool) (e'_1 proof_1 : Lean.Expr) (done_1 contextDependent_1 : Bool),
  (Lean.Meta.Sym.Simp.Result.step e' proof done contextDependent =
      Lean.Meta.Sym.Simp.Result.step e'_1 proof_1 done_1 contextDependent_1) =
    (e' = e'_1 ∧ proof = proof_1 ∧ done = done_1 ∧ contextDependent = contextDependent_1)
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_untop_eq_leadingCoeff : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} (hx : x.orderTop ≠ ⊤),
  x.coeff (x.orderTop.untop hx) = x.leadingCoeff
-- Mathlib.Algebra.Algebra.Spectrum.Basic
/-- **Alias** of the reverse direction of `spectrum.algebraMap_mem_iff`. -/
spectrum.algebraMap_mem : ∀ (S : Type u_1) {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] {a : A} {r : R},
  r ∈ spectrum R a → (algebraMap R S) r ∈ spectrum S a
-- Init.Grind.ToInt
/-- The embedding takes multiplication to multiplication, wrapped into the range interval.  -/
Lean.Grind.ToInt.Mul.toInt_mul : ∀ {α : Type u} {inst : Mul α} {I : outParam Lean.Grind.IntInterval} {inst_1 : Lean.Grind.ToInt α I}
  [self : Lean.Grind.ToInt.Mul α I] (x y : α), ↑(x * y) = I.wrap (↑x * ↑y)
-- Mathlib.Analysis.Analytic.IsolatedZeros
/-- If `f` is analytic at `z₀`, then exactly one of the following two possibilities occurs: either
`f` vanishes identically near `z₀`, or locally around `z₀` it has the form `z ↦ (z - z₀) ^ n • g z`
for some `n` and some `g` which is analytic and non-vanishing at `z₀`.  -/
AnalyticAt.exists_eventuallyEq_pow_smul_nonzero_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜},
  AnalyticAt 𝕜 f z₀ →
    ((∃ n g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in nhds z₀, f z = (z - z₀) ^ n • g z) ↔
      ¬∀ᶠ (z : 𝕜) in nhds z₀, f z = 0)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv_left_inv_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] {n : ℤ}
  {X Y : Cᵒᵖ} (f : Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)) ⟶ Y) {Z : C}
  (h : (CategoryTheory.shiftFunctor C n).obj (Opposite.unop X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app Y).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C n).map
          (CategoryTheory.Pretriangulated.opShiftFunctorEquivalenceSymmHomEquiv f).unop)
        h) =
    CategoryTheory.CategoryStruct.comp f.unop h
-- Mathlib.CategoryTheory.Category.PartialFun
instFaithfulPartialFunTypeToPartialFun : typeToPartialFun.Faithful
-- Init.Data.Fin.Lemmas
Fin.natAdd_last : ∀ {m n : ℕ}, Fin.natAdd n (Fin.last m) = Fin.last (n + m)
-- Mathlib.GroupTheory.FreeGroup.IsFreeGroup
FreeAddGroupBasis.lift.eq_1 : ∀ {ι : Type u_1} {G : Type u_3} {H : Type u_4} [inst : AddGroup G] [inst_1 : AddGroup H] (b : FreeAddGroupBasis ι G),
  b.lift =
    FreeAddGroup.lift.trans
      { toFun := fun f => f.comp b.repr.toAddMonoidHom, invFun := fun f => f.comp b.repr.symm.toAddMonoidHom,
        left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.exists_root_of_degree_eq_one : ∀ {R : Type u} [inst : Field R] {p : Polynomial R}, p.degree = 1 → ∃ x, p.IsRoot x
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheoremTree : Type
-- Mathlib.Combinatorics.SimpleGraph.Density
SimpleGraph.edgeDensity_def : ∀ {α : Type u_4} (G : SimpleGraph α) [inst : DecidableRel G.Adj] (s t : Finset α),
  G.edgeDensity s t = ↑(G.interedges s t).card / (↑s.card * ↑t.card)
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.balLeft.match_4.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (l : RBTree.RBNode α) →
      ((a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b)) →
        ((l : RBTree.RBNode α) →
            (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
              motive l) →
          motive l
-- Mathlib.Topology.Defs.Basic
/-- The set representing the whole space is an open set.
Use `isOpen_univ` in the root namespace instead.  -/
TopologicalSpace.isOpen_univ : ∀ {X : Type u} [self : TopologicalSpace X], TopologicalSpace.IsOpen Set.univ
-- Mathlib.Order.Preorder.Chain
Flag.instPartialOrder : {α : Type u_1} → [inst : LE α] → PartialOrder (Flag α)
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.mk_left : ∀ {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) [inst : AlgebraicGeometry.WeaklyEtale f],
  (AlgebraicGeometry.Scheme.ProEt.mk f).left = X
-- Mathlib.CategoryTheory.Comma.Basic
/-- Composing the `leftOp` of `opFunctor L R` with `fst L.op R.op` is naturally isomorphic
to `snd L R`.  -/
CategoryTheory.Comma.opFunctorCompFst : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              (R : CategoryTheory.Functor B T) →
                (CategoryTheory.Comma.opFunctor L R).leftOp.comp (CategoryTheory.Comma.fst R.op L.op) ≅
                  (CategoryTheory.Comma.snd L R).op
-- Mathlib.Topology.Semicontinuity.Defs
UpperSemicontinuous.upperSemicontinuousOn : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β},
  UpperSemicontinuous f → ∀ (s : Set α), UpperSemicontinuousOn f s
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
Set.Subsingleton.measurableSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] {s : Set α}, s.Subsingleton → MeasurableSet s
-- Init.Grind.Module.Basic
Lean.Grind.AddCommGroup.toNeg : {M : Type u} → [self : Lean.Grind.AddCommGroup M] → Neg M
-- Mathlib.Data.Finsupp.SMul
/-- `Finsupp.comapSMul` is multiplicative  -/
Finsupp.comapMulAction : {α : Type u_1} →
  {M : Type u_3} →
    {G : Type u_5} → [inst : Monoid G] → [MulAction G α] → [inst_2 : AddCommMonoid M] → MulAction G (α →₀ M)
-- Init.Data.ByteArray.Basic
ByteArray.fastAppend_eq : ∀ {a b : ByteArray}, a.fastAppend b = a ++ b
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.cast.eq_1 : ∀ {ι : Type u_9} {M : ι → Type u_10} [inst : (i : ι) → Add (M i)] {i j : ι} (h : i = j),
  AddEquiv.cast h = { toEquiv := Equiv.cast ⋯, map_add' := ⋯ }
-- Init.Data.UInt.Bitwise
UInt32.toNat_and : ∀ (a b : UInt32), (a &&& b).toNat = a.toNat &&& b.toNat
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- **Alias** of the reverse direction of `isMulCommutative_iff_of_setLike`. -/
IsMulCommutative.of_setLike_mul_comm : ∀ {S : Type u_3} {M : Type u_4} [inst : SetLike S M] [inst_1 : Mul M] [inst_2 : MulMemClass S M] {s : S},
  (∀ a ∈ s, ∀ b ∈ s, a * b = b * a) → IsMulCommutative ↥s
-- Lean.Elab.Do.Basic
Lean.Elab.Do.CodeLiveness.deadSyntactically.sizeOf_spec : sizeOf Lean.Elab.Do.CodeLiveness.deadSyntactically = 1
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv_apply : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y) (y : ↑Y.toTopCat)
  (z :
    ↑(Y.presheaf.stalk
        ((CategoryTheory.ConcreteCategory.hom e.hom.base) ((CategoryTheory.ConcreteCategory.hom e.inv.base) y)))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.inv y))
      ((CategoryTheory.ConcreteCategory.hom
          (AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap e.hom
            ((CategoryTheory.ConcreteCategory.hom e.inv.base) y)))
        z) =
    (CategoryTheory.ConcreteCategory.hom (Y.presheaf.stalkSpecializes ⋯)) z
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.instT2SpaceCarrierObjTopCatCompHausLikeToTop : ∀ (P : TopCat → Prop) (X : CompHausLike P), T2Space ↑((CompHausLike.compHausLikeToTop P).obj X)
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
PowerSeries.coeff_pentagonalSeries_eq_zero_iff : ∀ (R : Type u_1) [inst : CommRing R] [Nontrivial R] {n : ℕ},
  (PowerSeries.coeff n) (PowerSeries.pentagonalSeries R) = 0 ↔ n ∉ Set.range pentagonal
-- Init.Data.Nat.ToString
Nat.toNat_digitChar_of_lt_ten : ∀ {n : ℕ}, n < 10 → n.digitChar.toNat = 48 + n
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.stdBasis.congr_simp : ∀ (R : Type u_1) (m : Type u_2) (n : Type u_3) [inst : Fintype m] [inst_1 : Finite n] [inst_2 : Semiring R],
  Matrix.stdBasis R m n = Matrix.stdBasis R m n
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.divCoeffs c) = 1 + sizeOf c
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
_private.Init.Data.String.Lemmas.Pattern.String.ForwardPattern.0.String.Slice.Pos.revSkipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.euclidean.instRingMixedSpace : (K : Type u_1) → [inst : Field K] → Ring (NumberField.mixedEmbedding.euclidean.mixedSpace K)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.isUnit_iff : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : DivisionMonoid α] {s : Finset α}, IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a
-- Init.Data.Sum.Basic
Sum.map_inr : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → α') (g : β → β') (x : β),
  Sum.map f g (Sum.inr x) = Sum.inr (g x)
-- Mathlib.Algebra.Ring.Equiv
MulEquiv.isDomain_iff : ∀ {A : Type u_7} {B : Type u_8} [inst : Semiring A] [inst_1 : Semiring B] (e : A ≃* B), IsDomain A ↔ IsDomain B
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.BoundedFormula.freeVarFinset.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (_n : ℕ)
  (h_1 : (_n : ℕ) → motive _n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (_n : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (_n l : ℕ) →
      (_R : L.Relations l) →
        (ts : Fin l → L.Term (α ⊕ Fin _n)) → motive _n (FirstOrder.Language.BoundedFormula.rel _R ts))
  (h_4 : (_n : ℕ) → (f₁ f₂ : L.BoundedFormula α _n) → motive _n (f₁.imp f₂))
  (h_5 : (_n : ℕ) → (f : L.BoundedFormula α (_n + 1)) → motive _n f.all),
  (match _n, FirstOrder.Language.BoundedFormula.falsum with
    | _n, FirstOrder.Language.BoundedFormula.falsum => h_1 _n
    | _n, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 _n t₁ t₂
    | _n, FirstOrder.Language.BoundedFormula.rel _R ts => h_3 _n l _R ts
    | _n, f₁.imp f₂ => h_4 _n f₁ f₂
    | _n, f.all => h_5 _n f) =
    h_1 _n
-- Init.Data.Nat.Lemmas
Nat.add_sub_sub_cancel : ∀ {a b c : ℕ}, c ≤ a → a + b - (a - c) = b + c
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.period.eq_1 : ∀ {α : Type v} {M : Type u} [inst : AddMonoid M] [inst_1 : AddAction M α] (m : M) (a : α),
  AddAction.period m a = Function.minimalPeriod (fun x => m +ᵥ x) a
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasRightInverse.comp_continuousLinearEquivalence : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} {F' : Type u_5} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] [inst_7 : TopologicalSpace F'] [inst_8 : AddCommMonoid F'] [inst_9 : Module R F']
  {f : E →L[R] F} {f₀ : F' ≃L[R] E}, f.HasRightInverse → (f ∘SL ↑f₀).HasRightInverse
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsLowerSet.monotone_to_lowerTopology_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [Topology.IsLowerSet α] [Topology.IsLower β] {f : α → β}, Monotone f → Continuous f
-- Mathlib.Analysis.Calculus.LHopital
/-- L'Hôpital's rule for approaching +∞, `HasDerivAt` version  -/
HasDerivAt.lhopital_zero_atTop : ∀ {l : Filter ℝ} {f f' g g' : ℝ → ℝ},
  (∀ᶠ (x : ℝ) in Filter.atTop, HasDerivAt f (f' x) x) →
    (∀ᶠ (x : ℝ) in Filter.atTop, HasDerivAt g (g' x) x) →
      (∀ᶠ (x : ℝ) in Filter.atTop, g' x ≠ 0) →
        Filter.Tendsto f Filter.atTop (nhds 0) →
          Filter.Tendsto g Filter.atTop (nhds 0) →
            Filter.Tendsto (fun x => f' x / g' x) Filter.atTop l → Filter.Tendsto (fun x => f x / g x) Filter.atTop l
-- Lean.Environment
/-- Sets synchronous and (private) asynchronous parts of the environment to the given kernel environment.  -/
_private.Lean.Environment.0.Lean.Environment.setCheckedSync : Lean.Environment → Lean.Kernel.Environment → Lean.Environment
-- Mathlib.Data.EReal.Operations
EReal.left_distrib_of_nonneg : ∀ {a b c : EReal}, 0 ≤ a → 0 ≤ b → c * (a + b) = c * a + c * b
-- Mathlib.Tactic.SplitIfs
/-- Simplifies if-then-else expressions after cases have been split out.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.reduceIfsAt : Lean.Elab.Tactic.Location → Lean.Elab.Tactic.TacticM Unit
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains'.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_succ_C : ∀ {R : Type u_1} [inst : Semiring R] {a : R} {n : ℕ}, (PowerSeries.coeff (n + 1)) (PowerSeries.C a) = 0
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_one : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α],
  (Matrix.diagonal fun x => 1) = 1
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.Arrows.PullbackCompatible.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C}
  {I : Type u_1} {X : I → C} (π π_1 : (i : I) → X i ⟶ B) (e_π : π = π_1)
  [inst_1 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] (x x_1 : (i : I) → P.obj (Opposite.op (X i))),
  x = x_1 →
    CategoryTheory.Presieve.Arrows.PullbackCompatible P π x =
      CategoryTheory.Presieve.Arrows.PullbackCompatible P π_1 x_1
-- Init.Control.Except
/-- Transforms a successful computation's value using `f`. Typically used via the `<$>` operator.
 -/
ExceptT.map : {ε : Type u} → {m : Type u → Type v} → [Monad m] → {α β : Type u} → (α → β) → ExceptT ε m α → ExceptT ε m β
-- Mathlib.Order.RelSeries
RelSeries.last_append : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r),
  (p.append q connect).last = q.last
-- Mathlib.Topology.Order
isOpen_sSup_iff : ∀ {α : Type u} {s : Set α} {T : Set (TopologicalSpace α)}, IsOpen s ↔ ∀ t ∈ T, IsOpen s
-- Mathlib.Algebra.GroupWithZero.WithZero
/-- Recursion principle for `Mᵐ⁰`. To construct predicate for all elements of `Mᵐ⁰`, it is enough to
construct its value at `0` and its value at `exp a` for all `a : M`.  -/
WithZero.expRecOn : {M : Type u_4} →
  {motive : WithZero (Multiplicative M) → Sort u_6} →
    (x : WithZero (Multiplicative M)) → motive 0 → ((a : M) → motive (WithZero.exp a)) → motive x
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of `hasFDerivWithinAt_sdiff_singleton`. -/
hasFDerivWithinAt_diff_singleton : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [T1Space E] (y : E),
  HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_mono_left : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {G'' : Type u_8}
  [inst_2 : NormedAddCommGroup G''] [inst_3 : PartialOrder G''] [IsOrderedAddMonoid G''] [inst_5 : NormedSpace ℝ G'']
  {m : MeasurableSpace α} (T T' : Set α → F →L[ℝ] G''),
  (∀ (s : Set α) (x : F), (T s) x ≤ (T' s) x) →
    ∀ (f : MeasureTheory.SimpleFunc α F),
      MeasureTheory.SimpleFunc.setToSimpleFunc T f ≤ MeasureTheory.SimpleFunc.setToSimpleFunc T' f
-- Mathlib.Condensed.Light.TopCatAdjunction
LightCondSet.instIsIsoFunctorSequentialCounitSequentialAdjunction : CategoryTheory.IsIso LightCondSet.sequentialAdjunction.counit
-- Mathlib.CategoryTheory.Monad.Algebra
/-- The category of Eilenberg-Moore coalgebras for a comonad.  -/
CategoryTheory.Comonad.Coalgebra.eilenbergMoore : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {G : CategoryTheory.Comonad C} → CategoryTheory.Category.{v₁, max u₁ v₁} G.Coalgebra
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.comp_id : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (φ : A →ₐc[R] B), φ.comp (BialgHom.id R A) = φ
-- Mathlib.Tactic.Widget.LibraryRewrite
/-- Try to rewrite `e` with each of the rewrite lemmas, and sort the resulting rewrites.  -/
Mathlib.Tactic.LibraryRewrite.checkAndSortRewriteLemmas : Lean.Expr →
  Array Mathlib.Tactic.LibraryRewrite.RewriteLemma →
    Lean.MetaM (Array (Mathlib.Tactic.LibraryRewrite.Rewrite × Lean.Name))
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.lift_eq_aleph_ofNat : ∀ {c : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo],
  Cardinal.lift.{v, u} c = Cardinal.aleph (OfNat.ofNat n) ↔ c = Cardinal.aleph (OfNat.ofNat n)
-- Lean.Data.Options
Lean.Options.find? : Lean.Options → Lean.Name → Option Lean.DataValue
-- Mathlib.Data.EReal.Basic
EReal.toENNReal_eq_zero_iff : ∀ {x : EReal}, x.toENNReal = 0 ↔ x ≤ 0
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instInhabitedDiagnosticCode.default : Lean.Lsp.DiagnosticCode
-- Mathlib.Analysis.Convex.Gauge
gauge_neg : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E},
  (∀ x ∈ s, -x ∈ s) → ∀ (x : E), gauge s (-x) = gauge s x
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.uniformContinuous_union : ∀ {α : Type u_1} [inst : UniformSpace α], UniformContinuous fun x => x.1 ∪ x.2
-- Mathlib.Data.Seq.Basic
Stream'.Seq.get?_mem_take : ∀ {α : Type u} {s : Stream'.Seq α} {m n : ℕ}, m < n → ∀ {x : α}, s.get? m = some x → x ∈ Stream'.Seq.take n s
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
/-- **The Lebesgue Decomposition theorem between a signed measure and a measure**:
Given a signed measure `s` and a σ-finite measure `μ`, there exist a signed measure `t` and a
measurable and integrable function `f`, such that `t` is mutually singular with respect to `μ`
and `s = t + μ.withDensityᵥ f`. In this case `t = s.singularPart μ` and
`f = s.rnDeriv μ`.  -/
MeasureTheory.SignedMeasure.singularPart_add_withDensity_rnDeriv_eq : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (s : MeasureTheory.SignedMeasure α)
  [s.HaveLebesgueDecomposition μ], s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso_inv_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u_2} (j : J) (X : J → C),
  (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C j).inv.app X = CategoryTheory.CategoryStruct.id (X j)
-- Lean.Util.PPExt
Lean.PPFns.mk.sizeOf_spec : ∀ (ppExprWithInfos : Lean.PPContext → Lean.Expr → IO Lean.FormatWithInfos)
  (ppConstNameWithInfos : Lean.PPContext → Lean.Name → IO Lean.FormatWithInfos)
  (ppTerm : Lean.PPContext → Lean.Term → IO Std.Format) (ppLevel : Lean.PPContext → Lean.Level → IO Std.Format)
  (ppGoal : Lean.PPContext → Lean.MVarId → IO Std.Format),
  sizeOf
      { ppExprWithInfos := ppExprWithInfos, ppConstNameWithInfos := ppConstNameWithInfos, ppTerm := ppTerm,
        ppLevel := ppLevel, ppGoal := ppGoal } =
    1
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- A preadditive category `C` with an additive shift, and a class of "distinguished triangles"
relative to that shift is called pretriangulated if the following hold:
* Any triangle that is isomorphic to a distinguished triangle is also distinguished.
* Any triangle of the form `(X,X,0,id,0,0)` is distinguished.
* For any morphism `f : X ⟶ Y` there exists a distinguished triangle of the form `(X,Y,Z,f,g,h)`.
* The triangle `(X,Y,Z,f,g,h)` is distinguished if and only if `(Y,Z,X⟦1⟧,g,h,-f⟦1⟧)` is.
* Given a diagram:
  ```
        f       g       h
    X  ───> Y  ───> Z  ───> X⟦1⟧
    │       │                │
    │a      │b               │a⟦1⟧'
    V       V                V
    X' ───> Y' ───> Z' ───> X'⟦1⟧
        f'      g'      h'
  ```
  where the left square commutes, and whose rows are distinguished triangles,
  there exists a morphism `c : Z ⟶ Z'` such that `(a,b,c)` is a triangle morphism.
 -/
CategoryTheory.Pretriangulated : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] → Type (max u v)
-- Mathlib.Algebra.Ring.Ext
NonUnitalNonAssocCommSemiring.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : NonUnitalNonAssocCommSemiring R},
  inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Tactic.Simproc.Divisors
_private.Mathlib.Tactic.Simproc.Divisors.0.Nat.divisors_ofNat.unsafe_1 : ℕ → List ℕ
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_seq_def : ∀ {R : Type u_1} [inst : CommRing R] (c : R) (f : RingSeminorm R) (x : R),
  seminormFromConst_seq c f x = fun n => f (x * c ^ n) / f c ^ n
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.mul_polyOfInterest_aux2 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  ↑p ^ n * WittVector.wittMul p n + WittVector.wittPolyProdRemainder p n = WittVector.wittPolyProd p n
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.primPart_ne_zero : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] [Nontrivial R] (p : Polynomial R), p.primPart ≠ 0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k : α} {v : β}, (m.insert k v)[k]! = v
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
_private.Mathlib.Algebra.SkewMonoidAlgebra.Basic.0.SkewMonoidAlgebra.add.eq_1 : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] (a b : G →₀ k),
  SkewMonoidAlgebra.add✝ { coeff := a } { coeff := b } = { coeff := a + b }