mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Tactic.Lint.Basic
_private.Batteries.Tactic.Lint.Basic.0.Batteries.Tactic.Lint.getLinter.unsafe_impl_2 : Lean.Name → Lean.Name → Lean.CoreM Batteries.Tactic.Lint.NamedLinter
-- Mathlib.Algebra.Module.NatInt
/-- If `M` is an `R`-module with one and `M` has characteristic zero, then `R` has characteristic
zero as well. Usually `M` is an `R`-algebra.  -/
CharZero.of_module : ∀ {R : Type u_1} (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoidWithOne M] [CharZero M] [Module R M],
  CharZero R
-- Init.Data.BitVec.Lemmas
/-- If two bitvectors have different `msb`s, then signed and unsigned comparisons are opposites  -/
BitVec.slt_eq_not_ult_of_msb_neq : ∀ {w : ℕ} {x y : BitVec w}, x.msb ≠ y.msb → x.slt y = !x.ult y
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_symm_half : ∀ (m : ℕ), (2 * m + 1).choose (m + 1) = (2 * m + 1).choose m
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
Lean.Elab.ConfigEval.EvalConfigItemHandlerKind.wildcard.sizeOf_spec : sizeOf Lean.Elab.ConfigEval.EvalConfigItemHandlerKind.wildcard = 1
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.instCompl : {α : Type u_2} → [inst : TopologicalSpace α] → Compl (TopologicalSpace.Clopens α)
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_union_sdiff_cancel : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u : Finset α}, t ⊆ s → u ⊆ t → s \ t ∪ t \ u = s \ u
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
/-- Compatibility isomorphisms of `functorExtension₁` with respect to the
composition of functors.  -/
CategoryTheory.Idempotents.functorExtension₁Comp : (C : Type u_1) →
  (D : Type u_2) →
    (E : Type u_3) →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            (F : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)) →
              (G : CategoryTheory.Functor D (CategoryTheory.Idempotents.Karoubi E)) →
                (CategoryTheory.Idempotents.functorExtension₁ C E).obj
                    (F.comp ((CategoryTheory.Idempotents.functorExtension₁ D E).obj G)) ≅
                  ((CategoryTheory.Idempotents.functorExtension₁ C D).obj F).comp
                    ((CategoryTheory.Idempotents.functorExtension₁ D E).obj G)
-- Mathlib.MeasureTheory.Function.UniformIntegrable
/-- Suppose `f` is a sequence of functions that converges in measure to `g`. If `f` is
`UniformIntegrable`, then `g` is integrable.  -/
MeasureTheory.UniformIntegrable.integrable_of_tendstoInMeasure : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {κ : Type u_4} {u : Filter κ} [u.NeBot] [u.IsCountablyGenerated] {f : κ → α → β} {g : α → β},
  MeasureTheory.UniformIntegrable f 1 μ → MeasureTheory.TendstoInMeasure μ f u g → MeasureTheory.Integrable g μ
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMat__obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v₁, u_1} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] (M : CategoryTheory.Mat_ C) (i : M.ι),
  (F.mapMat_.obj M).X i = F.obj (M.X i)
-- Mathlib.Algebra.Ring.SumsOfSquares
IsSumSq.natCast : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (n : ℕ), IsSumSq ↑n
-- Mathlib.Data.PNat.Basic
/-- `coe` promoted to an `AddHom`, that is, a morphism which preserves addition.  -/
PNat.coeAddHom : ℕ+ →ₙ+ ℕ
-- Mathlib.Algebra.DirectSum.LinearMap
LinearMap.trace_eq_zero_of_mapsTo_ne : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : ι → Submodule R M} [inst_3 : DecidableEq ι] [∀ (i : ι), Module.Finite R ↥(N i)]
  [∀ (i : ι), Module.Free R ↥(N i)],
  DirectSum.IsInternal N →
    ∀ [IsNoetherian R M] (σ : ι → ι),
      (∀ (i : ι), σ i ≠ i) →
        ∀ {f : Module.End R M}, (∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N (σ i))) → (LinearMap.trace R M) f = 0
-- Init.Data.UInt.Bitwise
USize.ofBitVec_and : ∀ (a b : BitVec System.Platform.numBits), { toBitVec := a &&& b } = { toBitVec := a } &&& { toBitVec := b }
-- Mathlib.CategoryTheory.Sites.JointlySurjective
CategoryTheory.Types.singleton_mem_jointlySurjectivePrecoverage_iff : ∀ {X Y : Type u} {f : X ⟶ Y},
  CategoryTheory.Presieve.singleton f ∈ CategoryTheory.Types.jointlySurjectivePrecoverage.coverings Y ↔
    Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Whiskering a 2-square with a natural transformation at the left side.  -/
CategoryTheory.TwoSquare.whiskerLeft : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        {L' : CategoryTheory.Functor C₁ C₃} →
                          CategoryTheory.TwoSquare T L R B → (L ⟶ L') → CategoryTheory.TwoSquare T L' R B
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.unop_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty Cᵒᵖ} {X Y : Cᵒᵖ}
  (φ : W.RightFraction X Y), φ.unop.f = φ.f.unop
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.instSub : (p n : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → Sub (TruncatedWittVector p n R)
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.liftNC_smul : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : MulOneClass M]
  (f : S →+* R) (g : M →* R) (c : S) (φ : MonoidAlgebra S M),
  (MonoidAlgebra.liftNC ↑f ⇑g) (c • φ) = f c * (MonoidAlgebra.liftNC ↑f ⇑g) φ
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_ceil_left_pure_ceil : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [inst_3 : TopologicalSpace α]
  [IsStrictOrderedRing α] [OrderClosedTopology α] (x : α), Filter.Tendsto Int.ceil (nhdsWithin x (Set.Iic x)) (pure ⌈x⌉)
-- Mathlib.Algebra.Order.Group.OrderIso
/-- **Alias** of the forward direction of `le_neg`. -/
le_neg_of_le_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] [AddRightMono α] {a b : α}, a ≤ -b → b ≤ -a
-- Init.Data.List.Impl
/-- Auxiliary for `modifyTR`: `modifyTR.go f l i acc = acc.toList ++ modify f i l`.  -/
_private.Init.Data.List.Impl.0.List.modifyTR.go : {α : Type u_1} → (α → α) → List α → ℕ → Array α → List α
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
/-- **Alias** of `RootPairing.IsValuedIn.exists_value`. -/
RootPairing.exists_value : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N} {S : Type u_6}
  {inst_5 : CommRing S} {inst_6 : Algebra S R} [self : P.IsValuedIn S] (i j : ι),
  ∃ s, (algebraMap S R) s = P.pairing i j
-- Mathlib.Topology.Algebra.Star
instContinuousStarUnits : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : TopologicalSpace R] [ContinuousStar R],
  ContinuousStar Rˣ
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
rel_iff_cov' : ∀ {M : Type u_1} {N : Type u_2} {μ : M → N → N} {r : N → N → Prop},
  Covariant M N μ r → Contravariant M N μ r → ∀ {m : M} {a b : N}, r (μ m a) (μ m b) ↔ r a b
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_eq_dual_mul_dual : ∀ (A : Type u_1) (K : Type u_2) (L : Type u) (B : Type u_5) [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] (C : Type u_3) (M : Type u_4) [inst_19 : CommRing C] [inst_20 : IsDedekindDomain C]
  [inst_21 : Field M] [inst_22 : Algebra C M] [inst_23 : IsFractionRing C M] [inst_24 : Algebra A C]
  [inst_25 : Algebra B C] [inst_26 : Algebra A M] [inst_27 : Algebra B M] [inst_28 : Algebra K M]
  [inst_29 : Algebra L M] [inst_30 : IsScalarTower A C M] [inst_31 : IsScalarTower A K M]
  [inst_32 : IsScalarTower B C M] [inst_33 : IsScalarTower B L M] [IsScalarTower K L M]
  [inst_35 : IsIntegralClosure C A M] [inst_36 : FiniteDimensional K M] [inst_37 : FiniteDimensional L M]
  [inst_38 : Algebra.IsSeparable K M] [inst_39 : IsIntegralClosure C B M] [inst_40 : Algebra.IsSeparable L M]
  [inst_41 : Module.IsTorsionFree B C], FractionalIdeal.dual A K 1 = FractionalIdeal.dual B L ⋯ * ⋯ ⋯
-- Mathlib.Analysis.Convolution
/-- The forward convolution of two functions `f` and `g` on `ℝ`, with respect to a continuous
bilinear map `L` and measure `ν`. It is defined to be the function mapping `x` to
`∫ t in 0..x, L (f t) (g (x - t)) ∂ν` if `0 < x`, and 0 otherwise.  -/
MeasureTheory.posConvolution : {E : Type uE} →
  {E' : Type uE'} →
    {F : Type uF} →
      [inst : NormedAddCommGroup E] →
        [inst_1 : NormedAddCommGroup E'] →
          [inst_2 : NormedAddCommGroup F] →
            [inst_3 : NormedSpace ℝ E] →
              [inst_4 : NormedSpace ℝ E'] →
                [inst_5 : NormedSpace ℝ F] →
                  (ℝ → E) →
                    (ℝ → E') →
                      (E →L[ℝ] E' →L[ℝ] F) →
                        autoParam (MeasureTheory.Measure ℝ) MeasureTheory.posConvolution._auto_1 → ℝ → F
-- Init.Data.List.Attach
List.head?_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a),
  (List.pmap f xs H).head? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.head?
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Append
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Append.0.Std.Iterators.Types.Append.instIterator.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} {β α₁ : Type u_1} [inst : Std.Iterator α₁ m β] (it₁ : Std.IterM m β)
  (motive : it₁.Step → Sort u_3) (it₁' : Std.IterM m β) (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁'))
  (h_1 :
    (it₁' : Std.IterM m β) →
      (out : β) → (h : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, h⟩)
  (h_2 :
    (it₁' : Std.IterM m β) → (h : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', h⟩)
  (h_3 : (h : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, h⟩),
  (match ⟨Std.IterStep.skip it₁', h⟩ with
    | ⟨Std.IterStep.yield it₁' out, h⟩ => h_1 it₁' out h
    | ⟨Std.IterStep.skip it₁', h⟩ => h_2 it₁' h
    | ⟨Std.IterStep.done, h⟩ => h_3 h) =
    h_2 it₁' h
-- Init.Data.UInt.Lemmas
UInt64.ofBitVec_uInt32ToBitVec : ∀ (n : UInt32), { toBitVec := BitVec.setWidth 64 n.toBitVec } = n.toUInt64
-- Mathlib.Logic.Equiv.Option
/-- **Alias** of `Equiv.removeNoneAux_inv`. -/
Equiv.removeNone_aux_inv : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) (x : α), e.symm.removeNoneAux (e.removeNoneAux x) = x
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.instDecidableEqRingFunc : {a : ℕ} → DecidableEq (FirstOrder.ringFunc a)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.openCell_zero_injective`. -/
Topology.CWComplex.openCell_zero_injective : ∀ {X : Type u_1} [t : TopologicalSpace X] {D : Set X} (C : Set X) [inst : Topology.RelCWComplex C D],
  Function.Injective (Topology.RelCWComplex.openCell 0)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.forall : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  {p : ArchimedeanClass M → Prop}, (∀ (A : ArchimedeanClass M), p A) ↔ ∀ (a : M), p (ArchimedeanClass.mk a)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.mk.inj : ∀ {G : Type u_6} {inst : AddGroup G} {toFun : G → ℝ} {map_zero' : toFun 0 = 0}
  {add_le' : ∀ (r s : G), toFun (r + s) ≤ toFun r + toFun s} {neg' : ∀ (r : G), toFun (-r) = toFun r} {toFun_1 : G → ℝ}
  {map_zero'_1 : toFun_1 0 = 0} {add_le'_1 : ∀ (r s : G), toFun_1 (r + s) ≤ toFun_1 r + toFun_1 s}
  {neg'_1 : ∀ (r : G), toFun_1 (-r) = toFun_1 r},
  { toFun := toFun, map_zero' := map_zero', add_le' := add_le', neg' := neg' } =
      { toFun := toFun_1, map_zero' := map_zero'_1, add_le' := add_le'_1, neg' := neg'_1 } →
    toFun = toFun_1
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.pairingIn_pairingIn_mem_set_of_length_eq : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [Finite ι]
  [CharZero R] [inst_7 : P.IsCrystallographic] {i j : ι} [IsDomain R] {B : P.InvariantForm},
  (B.form (P.root i)) (P.root i) = (B.form (P.root j)) (P.root j) →
    (P.pairingIn ℤ i j, P.pairingIn ℤ j i) ∈ {(0, 0), (1, 1), (-1, -1), (2, 2), (-2, -2)}
-- Mathlib.MeasureTheory.Group.Defs
MeasureTheory.Measure.IsMulLeftInvariant.mk : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] {μ : MeasureTheory.Measure G},
  (∀ (g : G), MeasureTheory.Measure.map (fun x => g * x) μ = μ) → μ.IsMulLeftInvariant
-- Mathlib.Algebra.Category.Grp.FilteredColimits
/-- The colimit of `F ⋙ forget₂ AddGrpCat AddMonCat` in the category `AddMonCat`.
In the following, we will show that this has the structure of an additive group.  -/
AddGrpCat.FilteredColimits.G : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J AddGrpCat → AddMonCat
-- Mathlib.GroupTheory.OrderOfElement
/-- Commuting elements of finite order are closed under multiplication.  -/
Commute.isOfFinOrder_mul : ∀ {G : Type u_1} [inst : Monoid G] {x y : G}, Commute x y → IsOfFinOrder x → IsOfFinOrder y → IsOfFinOrder (x * y)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.instFunLike : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Algebra R A] → [inst_4 : Module A M] → [inst_5 : Module R M] → FunLike (Derivation R A M) A M
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.tensorProduct_tensorProduct : ∀ (R : Type u_8) (S : Type u_9) (A : Type u_10) (B : Type u_11) [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra A B] [inst_7 : IsScalarTower R A B] [inst_8 : Algebra R S]
  {x : Algebra (TensorProduct R A S) (TensorProduct R B S)}
  {x_1 : IsScalarTower A (TensorProduct R A S) (TensorProduct R B S)},
  (algebraMap (TensorProduct R A S) (TensorProduct R B S)).comp Algebra.TensorProduct.includeRight.toRingHom =
      Algebra.TensorProduct.includeRight.toRingHom →
    Algebra.IsPushout A B (TensorProduct R A S) (TensorProduct R B S)
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
AddChar.PrimitiveAddChar.mk.injEq : ∀ {R : Type u} [inst : CommRing R] {R' : Type v} [inst_1 : Field R'] (n : ℕ+)
  (char : AddChar R (CyclotomicField (↑n) R')) (prim : char.IsPrimitive) (n_1 : ℕ+)
  (char_1 : AddChar R (CyclotomicField (↑n_1) R')) (prim_1 : char_1.IsPrimitive),
  ({ n := n, char := char, prim := prim } = { n := n_1, char := char_1, prim := prim_1 }) = (n = n_1 ∧ char ≍ char_1)
-- Mathlib.Order.Interval.Set.Disjoint
IsLUB.biUnion_Iio_eq : ∀ {α : Type v} [inst : LinearOrder α] {s : Set α} {a : α}, IsLUB s a → ⋃ x ∈ s, Set.Iio x = Set.Iio a
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.isometry_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A], Isometry Unitization.inr
-- Aesop.Rule
Aesop.UnfoldRule.mk.inj : ∀ {decl : Lean.Name} {unfoldThm? : Option Lean.Name} {decl_1 : Lean.Name} {unfoldThm?_1 : Option Lean.Name},
  { decl := decl, unfoldThm? := unfoldThm? } = { decl := decl_1, unfoldThm? := unfoldThm?_1 } →
    decl = decl_1 ∧ unfoldThm? = unfoldThm?_1
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- A variant of `intervalIntegral.integral_deriv_eq_sub`, the Fundamental theorem
of calculus, involving integrating over the unit interval.  -/
intervalIntegral.integral_unitInterval_deriv_eq_sub : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  [inst_3 : RCLike 𝕜] [inst_4 : NormedSpace 𝕜 E] [IsScalarTower ℝ 𝕜 E] {f f' : 𝕜 → E} {z₀ z₁ : 𝕜},
  ContinuousOn (fun t => f' (z₀ + t • z₁)) (Set.Icc 0 1) →
    (∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (z₀ + t • z₁)) (z₀ + t • z₁)) →
      z₁ • ∫ (t : ℝ) in 0..1, f' (z₀ + t • z₁) = f (z₀ + z₁) - f z₀
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.instSuccOrderToType : (o : Ordinal.{u_1}) → SuccOrder o.ToType
-- Mathlib.RingTheory.Finiteness.Defs
/-- A module over a semiring is `Module.Finite` if it is finitely generated as a module.  -/
Module.Finite.fg_top : ∀ {R : Type u_1} {M : Type u_4} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : Module R M}
  [self : Module.Finite R M], ⊤.FG
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_apply_dite : ∀ {ι : Type u_1} {M : Type u_3} {γ : Type u_5} {s : Finset ι} [inst : AddCommMonoid M] {p : ι → Prop}
  [inst_1 : DecidablePred p] [inst_2 : DecidablePred fun x => ¬p x] (f : (x : ι) → p x → γ) (g : (x : ι) → ¬p x → γ)
  (h : γ → M), ∑ x ∈ s, h (if hx : p x then f x hx else g x hx) = ∑ x, h (f ↑x ⋯) + ∑ x, h (g ↑x ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.deleteVerts_inter_verts_left_eq : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {s : Set V}, G'.deleteVerts (G'.verts ∩ s) = G'.deleteVerts s
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.X_eq_zero_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [NoZeroDivisors R] {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → P 0 = 0
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological_i₂ : ∀ (pq : ℤ × ℤ), CategoryTheory.Abelian.SpectralObject.coreE₂Cohomological.i₂ pq = WithBotTop.coe (pq.2 + 1)
-- Aesop.Util.Tactic.Ext
Aesop.straightLineExtProgress : Lean.MVarId → Lean.MetaM Aesop.ExtResult
-- Mathlib.CategoryTheory.Sites.CompatibleSheafification
CategoryTheory.GrothendieckTopology.sheafificationWhiskerRightIso_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {E : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} E]
  (F : CategoryTheory.Functor D E)
  [inst_3 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) D]
  [inst_4 :
    ∀ (J : CategoryTheory.Limits.MulticospanShape),
      CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan J) E]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ E]
  [inst_7 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ F]
  [inst_8 :
    ∀ (X : C) (W : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D),
      CategoryTheory.Limits.PreservesLimit (W.index P).multicospan F]
  (P : CategoryTheory.Functor Cᵒᵖ D), (J.sheafificationWhiskerRightIso F).hom.app P = (J.sheafifyCompIso F P).hom
-- Mathlib.Algebra.MonoidAlgebra.Division
_private.Mathlib.Algebra.MonoidAlgebra.Division.0.AddMonoidAlgebra.«term_/ᵒᶠ_» : Lean.TrailingParserDescr
-- Init.Grind.Norm
Lean.Grind.natCast_div : ∀ (a b : ℕ), ↑(a / b) = ↑a / ↑b
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.rlp_πObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y), I.rlp (CategoryTheory.SmallObject.πObj I κ f)
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.map_nhds_eq : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → ∀ (x : X), Filter.map f (nhds x) = nhdsWithin (f x) (Set.range f)
-- Mathlib.CategoryTheory.Generator.HomologicalComplex
HomologicalComplex.isSeparator_coproduct_separatingFamily : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [c.HasNoLoop]
  [inst_2 : CategoryTheory.Limits.HasCoproductsOfShape ι C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] {X : C},
  CategoryTheory.IsSeparator X →
    CategoryTheory.IsSeparator (∐ fun i => HomologicalComplex.separatingFamily c (fun x => X) (PUnit.unit, i))
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.ι_preservesColimitIso_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G]
  [inst_4 : CategoryTheory.Limits.HasColimit F] (j : J) {Z : D} (h : CategoryTheory.Limits.colimit (F.comp G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.ι F j))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) j) h
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_of_left_mem_of_le : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid ι]
  [inst_3 : PartialOrder ι] [CanonicallyOrderedAdd ι] [inst_5 : SetLike σ A] [inst_6 : AddSubmonoidClass σ A]
  (𝒜 : ι → σ) [inst_7 : GradedRing 𝒜] {a b : A} {n i : ι} [inst_8 : Sub ι] [OrderedSub ι] [AddLeftReflectLE ι],
  a ∈ 𝒜 i → i ≤ n → ↑(((DirectSum.decompose 𝒜) (a * b)) n) = a * ↑(((DirectSum.decompose 𝒜) b) (n - i))
-- Mathlib.Topology.Baire.BaireMeasurable
BaireMeasurableSet.of_compl : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α}, BaireMeasurableSet sᶜ → BaireMeasurableSet s
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.instHashableEMatchTheoremKind : Hashable Lean.Meta.Grind.EMatchTheoremKind
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_ne_one_iff : ∀ {α : Type u} [inst : Preorder α], Order.cof α ≠ 1 ↔ NoTopOrder α
-- Mathlib.CategoryTheory.Filtered.Small
/-- The small type modelling the filtered closure.  -/
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsFiltered.FilteredClosureSmall.AbstractFilteredClosure : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsFilteredOrEmpty C] → {α : Type w} → (α → C) → Type (max v w)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Fanin.flip.eq_1 : ∀ (f : Std.Sat.AIG.Fanin) (val : Bool), f.flip val = { val := f.val ^^^ val.toNat }
-- Init.Data.Char.Ordinal
_private.Init.Data.Char.Ordinal.0.Char.ofOrdinal.eq_1 : ∀ (f : Fin Char.numCodePoints),
  Char.ofOrdinal f =
    if h : ↑f < 55296 then { val := UInt32.ofNatLT ↑f ⋯, valid := ⋯ }
    else { val := UInt32.ofNatLT (↑f + Char.numSurrogates) ⋯, valid := ⋯ }