mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.ConditionallyCompleteLattice.Finset
Set.Finite.ciSup_lt_iff : ∀ {ι : Type u_1} {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] {a : α} {s : Set ι} {f : ι → α},
  s.Finite → (∃ x ∈ s, sSup ∅ ≤ f x) → (⨆ i ∈ s, f i < a ↔ ∀ x ∈ s, f x < a)
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_restrict_of_measurable_subtype : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → (Measurable fun x => f ↑x) → AEMeasurable f (μ.restrict s)
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.instLE.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddCon.instLE = { le := fun c d => ∀ ⦃x y : M⦄, c x y → d x y }
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [inst_3 : p.IsCartesian f φ'],
  (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f φ φ').inv =
    CategoryTheory.Functor.IsCartesian.map p f φ' φ
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.pi.eq_1 : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {γ : Type w} [inst_1 : Add γ] (g : (i : I) → γ →ₙ+ f i),
  AddHom.pi g = { toFun := fun x i => (g i) x, map_add' := ⋯ }
-- Mathlib.Analysis.Convex.MetricSpace
/-- Use `dist_iConvexComb_le` instead.  -/
Convexity.IsConvexDist.dist_iConvexComb_fst_snd_le : ∀ {X : Type u_2} [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X] [self : Convexity.IsConvexDist X]
  (f : Convexity.StdSimplex ℝ (X × X)),
  dist (Convexity.iConvexComb f Prod.fst) (Convexity.iConvexComb f Prod.snd) ≤
    Convexity.iConvexComb f fun x => dist x.1 x.2
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_inter_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α},
      Std.DTreeMap.Internal.Impl.contains k m₂ = false → Std.DTreeMap.Internal.Impl.Const.get? (m₁.inter m₂ ⋯) k = none
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_map : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {γ : α → Type w}
  [Std.TransCmp cmp] {f : (a : α) → β a → γ a} {k : α}, t.WF → (k ∈ Std.DTreeMap.Raw.map f t ↔ k ∈ t)
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The permutation representation of the endomorphism monoid on the root index set  -/
RootPairing.Hom.indexHom : {ι : 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) → P.End →* ι ≃ ι
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instIsOrderedAddMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β], IsOrderedAddMonoid (MeasureTheory.SimpleFunc α β)
-- Mathlib.Algebra.GroupWithZero.Torsion
UniqueFactorizationMonoid.instIsMulTorsionFree : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [UniqueFactorizationMonoid M] [NormalizationMonoid M]
  [IsMulTorsionFree Mˣ], IsMulTorsionFree M
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.mem_closure_of_mem' : ∀ {α : Type u_2} {X : Set α} {e : α} (M : Matroid α),
  e ∈ X → autoParam (e ∈ M.E) Matroid.mem_closure_of_mem'._auto_1 → e ∈ M.closure X
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.prun_pbind : ∀ {m : Type w → Type w'} {α : Type u} {β : Type v} {γ : Type w} [inst : Monad m] [LawfulMonad m]
  {x : Std.Iterators.HetT m α} {f : (a : α) → x.Property a → Std.Iterators.HetT m β}
  {g : (b : β) → (x.pbind f).Property b → m γ}, (x.pbind f).prun g = x.prun fun a ha => (f a ha).prun fun b hb => g b ⋯
-- Mathlib.Analysis.Normed.Group.Constructions
/-- Finite product of seminormed groups, using the sup norm.  -/
Pi.seminormedAddGroup : {ι : Type u_1} →
  {G : ι → Type u_4} → [Fintype ι] → [(i : ι) → SeminormedAddGroup (G i)] → SeminormedAddGroup ((i : ι) → G i)
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.eRank_emptyOn : ∀ (α : Type u_2), (Matroid.emptyOn α).eRank = 0
-- Mathlib.Algebra.Group.Finsupp
Finsupp.applyAddHom_apply : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddZeroClass M] (a : ι) (g : ι →₀ M), (Finsupp.applyAddHom a) g = g a
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
/-- We say that `f` approximates a continuous linear map `f'` on `s` with constant `c`,
if `‖f x - f y - f' (x - y)‖ ≤ c * ‖x - y‖` whenever `x, y ∈ s`.

This predicate is defined to facilitate the splitting of the inverse function theorem into small
lemmas. Some of these lemmas can be useful, e.g., to prove that the inverse function is defined
on a specific set.  -/
ApproximatesLinearOn : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] → [inst_4 : NormedSpace 𝕜 F] → (E → F) → (E →L[𝕜] F) → Set E → NNReal → Prop
-- Mathlib.Computability.DFA
DFA.accepts_comap : ∀ {α : Type u} {σ : Type v} (M : DFA α σ) {α' : Type u_1} (f : α' → α),
  (DFA.comap f M).accepts = List.map f ⁻¹' M.accepts
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.naturalityProperty.isStableUnderComposition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F₁ F₂ : CategoryTheory.Functor C D} (app : (X : C) → F₁.obj X ⟶ F₂.obj X),
  (CategoryTheory.MorphismProperty.naturalityProperty app).IsStableUnderComposition
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instSubOffset : Sub Std.Time.Minute.Offset
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.toContinuousLinearEquiv_toLinearEquiv_eq : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B), ↑↑e = ↑e.toAlgEquiv
-- Std.Time.Internal.Bounded
Std.Time.Internal.Bounded.LE.sub.eq_1 : ∀ {n m : ℤ} (bounded : Std.Time.Internal.Bounded.LE n m) (num : ℤ), bounded.sub num = bounded.add (-num)
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mk.inj : ∀ {X : Type u_3} {inst : MetricSpace X} {carrier : Set X} {packingRadius : NNReal}
  {packingRadius_pos : 0 < packingRadius} {isSeparated_packingRadius : Metric.IsSeparated (↑packingRadius) carrier}
  {coveringRadius : NNReal} {coveringRadius_pos : 0 < coveringRadius}
  {isCover_coveringRadius : Metric.IsCover coveringRadius Set.univ carrier} {carrier_1 : Set X}
  {packingRadius_1 : NNReal} {packingRadius_pos_1 : 0 < packingRadius_1}
  {isSeparated_packingRadius_1 : Metric.IsSeparated (↑packingRadius_1) carrier_1} {coveringRadius_1 : NNReal}
  {coveringRadius_pos_1 : 0 < coveringRadius_1}
  {isCover_coveringRadius_1 : Metric.IsCover coveringRadius_1 Set.univ carrier_1},
  { carrier := carrier, packingRadius := packingRadius, packingRadius_pos := packingRadius_pos,
        isSeparated_packingRadius := isSeparated_packingRadius, coveringRadius := coveringRadius,
        coveringRadius_pos := coveringRadius_pos, isCover_coveringRadius := isCover_coveringRadius } =
      { carrier := carrier_1, packingRadius := packingRadius_1, packingRadius_pos := packingRadius_pos_1,
        isSeparated_packingRadius := isSeparated_packingRadius_1, coveringRadius := coveringRadius_1,
        coveringRadius_pos := coveringRadius_pos_1, isCover_coveringRadius := isCover_coveringRadius_1 } →
    carrier = carrier_1 ∧ packingRadius = packingRadius_1 ∧ coveringRadius = coveringRadius_1
-- Mathlib.NumberTheory.Chebyshev
/-- The sum of `log p` over primes `p ≤ x`.  -/
Chebyshev.termθ : Lean.ParserDescr
-- Init.Omega.LinearCombo
/-- Implementation of scalar multiplication of a `LinearCombo` by an `Int`.  -/
Lean.Omega.LinearCombo.smul : Lean.Omega.LinearCombo → ℤ → Lean.Omega.LinearCombo
-- Mathlib.Analysis.Real.Hyperreal
/-- Standard part function: like a "round" to ℝ instead of ℤ  -/
Hyperreal.st : ℝ* → ℝ
-- Mathlib.CategoryTheory.Sites.PreservesSheafification
CategoryTheory.toPresheafToSheafCompComposeAndSheafify_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {A : Type u_1}
  {B : Type u_2} [inst_1 : CategoryTheory.Category.{v_1, u_1} A] [inst_2 : CategoryTheory.Category.{v_2, u_2} B]
  (F : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.HasWeakSheafify J B]
  [inst_4 : CategoryTheory.HasWeakSheafify J A] (X : CategoryTheory.Functor Cᵒᵖ A),
  (CategoryTheory.toPresheafToSheafCompComposeAndSheafify J F).app X =
    (CategoryTheory.presheafToSheaf J B).map (CategoryTheory.Functor.whiskerRight (CategoryTheory.toSheafify J X) F)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.length_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.toList.length = t.size
-- Std.Data.DTreeMap.Internal.Operations
/-- Slower version of `maxView` which can be used in the absence of balance information but still
assumes the preconditions of `maxView`, otherwise might panic.
 -/
Std.DTreeMap.Internal.Impl.maxView! : {α : Type u} →
  {β : α → Type v} →
    (k : α) →
      β k → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl.RawView α β
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_map_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀)
  {Z : AlgebraicGeometry.Scheme} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).f i) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst)
            (𝒰.X i.fst).affineCover).f
        i.snd)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰).f i.fst) h)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.toPoly.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] (P : Cubic R),
  P.toPoly =
    Polynomial.C P.a * Polynomial.X ^ 3 + Polynomial.C P.b * Polynomial.X ^ 2 + Polynomial.C P.c * Polynomial.X +
      Polynomial.C P.d
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- A *circuit* at `u : V` is a nonempty trail beginning and ending at `u`.  -/
SimpleGraph.Walk.IsCircuit : {V : Type u} → {G : SimpleGraph V} → {u : V} → G.Walk u u → Prop
-- Mathlib.RingTheory.Ideal.Defs
Ideal.mul_mem_left : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α) (a : α) {b : α}, b ∈ I → a * b ∈ I
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.comap_ker : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {P : Type u_8} [inst_2 : MulOneClass P] (g : N →* P)
  (f : G →* N), Subgroup.comap f g.ker = (g.comp f).ker
-- Mathlib.Logic.Equiv.Prod
Equiv.piSplitAt_apply : ∀ {α : Type u_9} [inst : DecidableEq α] (i : α) (β : α → Type u_10) (f : (j : α) → β j),
  (Equiv.piSplitAt i β) f = (f i, fun j => f ↑j)
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.binomial_succ_succ : ∀ {α : Type u_1} {f : α → ℕ} {a b : α} [inst : DecidableEq α],
  a ≠ b →
    Nat.multinomial {a, b} (Function.update (Function.update f a (f a).succ) b (f b).succ) =
      Nat.multinomial {a, b} (Function.update f a (f a).succ) + Nat.multinomial {a, b} (Function.update f b (f b).succ)
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_div : ∀ {a b : ℕ} (ha : a < 2 ^ 16) (hb : b < 2 ^ 16), UInt16.ofNatLT (a / b) ⋯ = UInt16.ofNatLT a ha / UInt16.ofNatLT b hb
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instCreatesLimitsOfShapeIndFunctorOppositeTypeWalkingParallelPairInclusionOfHasLimitsOfShape : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Limits.WalkingParallelPair C] →
      CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Ind.inclusion C)
-- Init.Data.SInt.Lemmas
ISize.toInt8_ofIntClamp : ∀ {n : ℤ},
  -2 ^ (System.Platform.numBits - 1) ≤ n →
    n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofIntClamp n).toInt8 = Int8.ofInt n
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instZero : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → Zero (SkewMonoidAlgebra k G)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.ofIsoObj_homEquiv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type w)} {X Y : C}
  (R : F.CorepresentableBy X) (e : Y ≅ X) {Z : C}, (R.ofIsoObj e).homEquiv = e.homFromEquiv.trans R.homEquiv
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_apply_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a : α), toIcoMod hp a a = a
-- Init.System.IOError
IO.Error.timeExpired.sizeOf_spec : ∀ (osCode : UInt32) (details : String),
  sizeOf (IO.Error.timeExpired osCode details) = 1 + sizeOf osCode + sizeOf details
-- Mathlib.FieldTheory.Finite.GaloisField
instIsSplittingFieldZModGaloisFieldHSubPolynomialHPowNatX : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (n : ℕ),
  Polynomial.IsSplittingField (ZMod p) (GaloisField p n) (Polynomial.X ^ p ^ n - Polynomial.X)
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwInfo.mk : Lean.Expr →
  Lean.Expr →
    Option Lean.Expr →
      Lean.SubExpr.Pos → Mathlib.Tactic.ClickSuggestions.RwKind → Mathlib.Tactic.ClickSuggestions.RwInfo
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Extension of `liftCM` to continuous maps taking values in `T.baseSet` (local version of
homotopy lifting)  -/
Bundle.Trivialization.clift : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              {ι : Type u_5} →
                [inst_3 : TopologicalSpace ι] →
                  (T : Bundle.Trivialization F proj) →
                    [LocallyCompactPair ι ↑T.baseSet] → C(↑T.source × C(ι, ↑T.baseSet), C(ι, ↑T.source))
-- Mathlib.Order.SuccPred.Limit
PredOrder.prelimitRecOn.eq_1 : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  [inst_2 : WellFoundedGT α] (succ : (a : α) → ¬IsMin a → motive a → motive (Order.pred a))
  (isSuccPrelimit : (a : α) → Order.IsPredPrelimit a → ((b : α) → a < b → motive b) → motive a),
  PredOrder.prelimitRecOn b succ isSuccPrelimit =
    ⋯.fix
      (fun a IH =>
        if h : Order.IsPredPrelimit a then isSuccPrelimit a h IH
        else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
      b
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
/-- `HasRingHomProperty P Q` is a type class asserting that `P` is local at the target and the source,
and for `f : Spec B ⟶ Spec A`, it is equivalent to the ring hom property `Q`.
To make the proofs easier, we state it instead as
1. `Q` is local (See `RingHom.PropertyIsLocal`)
2. `P f` if and only if `Q` holds for every `Γ(Y, U) ⟶ Γ(X, V)` for all affine `U`, `V`.
  See `HasRingHomProperty.iff_appLE`.
 -/
AlgebraicGeometry.HasRingHomProperty : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme →
  outParam ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop
-- Mathlib.Analysis.Convex.Extreme
/-- **Alias** of `IsExtreme.convex_sdiff`. -/
IsExtreme.convex_diff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {A B : Set E} [IsOrderedRing 𝕜], Convex 𝕜 A → IsExtreme 𝕜 A B → Convex 𝕜 (A \ B)
-- Mathlib.Topology.Sober
genericPoint_closure : ∀ (α : Type u_1) [inst : TopologicalSpace α] [inst_1 : QuasiSober α] [inst_2 : IrreducibleSpace α],
  closure {genericPoint α} = Set.univ
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.characteristic_iff_le_comap : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ Subgroup.comap ϕ.toMonoidHom H
-- ProofWidgets.Component.RefreshComponent
ProofWidgets.RefreshComponent.AwaitRefreshParams.mk : Lean.Server.WithRpcRef ProofWidgets.RefreshComponent.RefreshRef → ℕ → ProofWidgets.RefreshComponent.AwaitRefreshParams
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.IsHermitian.sub : ∀ {α : Type u_1} {n : Type u_4} [inst : AddGroup α] [inst_1 : StarAddMonoid α] {A B : Matrix n n α},
  A.IsHermitian → B.IsHermitian → (A - B).IsHermitian
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
Complex.deriv_const_cpow : ∀ {f : ℂ → ℂ} {x : ℂ},
  DifferentiableAt ℂ f x → ∀ (c : ℂ), deriv (fun x => c ^ f x) x = Complex.log c * deriv f x * c ^ f x
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.hom_sub : ∀ {R : Type u} [inst : Ring R] {M N : ModuleCat R} (f g : M ⟶ N),
  ModuleCat.Hom.hom (f - g) = ModuleCat.Hom.hom f - ModuleCat.Hom.hom g
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.balRight.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)))
  (h_3 : (l : RBTree.RBNode α) → motive l) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
  l = RBTree.RBNode.node RBTree.RBColor.black a x b →
    (match l with
      | RBTree.RBNode.node RBTree.RBColor.black a x b => h_1 a x b
      | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) => h_2 a x b y c
      | l => h_3 l) ≍
      h_1 a x b
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimit_mul_mk_eq' : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J] {j : J} (x y : ↑(F.obj j)),
  MonCat.FilteredColimits.M.mk F ⟨j, x⟩ * MonCat.FilteredColimits.M.mk F ⟨j, y⟩ =
    MonCat.FilteredColimits.M.mk F ⟨j, x * y⟩
-- Mathlib.Order.Interval.Set.Pi
Set.image_single_Ico_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → Zero (α i)] (i : ι) (a : α i), Pi.single i '' Set.Ico a 0 = Set.Ico (Pi.single i a) 0
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
IsLeast.directedOn : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α},
  IsLeast s a → DirectedOn (fun x1 x2 => x2 ≤ x1) s
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isSemisimple_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsSemisimpleModule R M], Module.End.IsSemisimple 0
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.id_apply : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (x : M), LieModuleHom.id x = x
-- Init.Data.Int.Lemmas
Int.negSucc_eq_neg_ofNat_iff : ∀ {a b : ℕ}, Int.negSucc a = -↑b ↔ a + 1 = b
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddLocalization.r_iff_oreEqv_r : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {x y : M × ↥S},
  (AddLocalization.r S) x y ↔ (AddOreLocalization.oreEqv S M) x y
-- Mathlib.Util.Export
Lean.Export.Entry.expr.injEq : ∀ (n n_1 : Lean.Expr), (Lean.Export.Entry.expr n = Lean.Export.Entry.expr n_1) = (n = n_1)
-- Mathlib.Order.WithBot
Equiv.withBotSubtypeNe.eq_1 : ∀ {α : Type u_1},
  Equiv.withBotSubtypeNe =
    {
      toFun := fun x =>
        match x with
        | ⟨x, h⟩ => x.unbot h,
      invFun := fun x => ⟨↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The edist to a set is `< r` iff there exists a point in the set at edistance `< r`  -/
Metric.infEDist_lt_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s : Set α} {r : ENNReal},
  Metric.infEDist x s < r ↔ ∃ y ∈ s, edist x y < r
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.mk.inj : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} {simplex : Y.obj (Opposite.op { len := d })}
  {nonDegenerate : simplex ∈ Y.nonDegenerate d}
  {notMem : simplex ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d })))}
  {simplex_1 : Y.obj (Opposite.op { len := d })} {nonDegenerate_1 : simplex_1 ∈ Y.nonDegenerate d}
  {notMem_1 : simplex_1 ∉ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d })))},
  { simplex := simplex, nonDegenerate := nonDegenerate, notMem := notMem } =
      { simplex := simplex_1, nonDegenerate := nonDegenerate_1, notMem := notMem_1 } →
    simplex = simplex_1
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.prodZeroIso_iso_inv_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prodZeroIso X).inv CategoryTheory.Limits.prod.fst =
    CategoryTheory.CategoryStruct.id X
-- Mathlib.Probability.Kernel.CondDistrib
ProbabilityTheory.condDistrib_ae_eq_iff_measure_eq_compProd : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_3 : MeasureTheory.IsFiniteMeasure μ] {Y : α → Ω} {mβ : MeasurableSpace β} (X : α → β),
  AEMeasurable Y μ →
    ∀ (κ : ProbabilityTheory.Kernel β Ω) [ProbabilityTheory.IsFiniteKernel κ],
      ⇑(ProbabilityTheory.condDistrib Y X μ) =ᵐ[MeasureTheory.Measure.map X μ] ⇑κ ↔
        MeasureTheory.Measure.map (fun x => (X x, Y x)) μ = (MeasureTheory.Measure.map X μ).compProd κ
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_a : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra}
  (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c)
  [inst_2 : CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor]
  [inst_3 : CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor],
  (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).a = CategoryTheory.Monad.ForgetCreatesColimits.lambda c t
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.ωConj_toFun : ∀ {ι : 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} (b : P.Base)
  [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (x : Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R),
  (RootPairing.GeckConstruction.ωConj b) x = RootPairing.GeckConstruction.ω b * x * RootPairing.GeckConstruction.ω b
-- Lean.Elab.Tactic.Basic
/-- Like `throwErrorAt`, but, if recovery is enabled, logs the error instead.
 -/
Lean.Elab.Tactic.throwOrLogErrorAt : Lean.Syntax → Lean.MessageData → Lean.Elab.Tactic.TacticM Unit