mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
/-- More convenient version of `TrivSqZeroExt.eq_smul_exp_of_invertible` for when `R` is a
field.  -/
TrivSqZeroExt.eq_smul_exp_of_ne_zero : ∀ {R : Type u_3} {M : Type u_4} [inst : Field R] [inst_1 : AddCommGroup M] [Algebra ℚ R] [Module ℚ M]
  [inst_4 : Module R M] [inst_5 : Module Rᵐᵒᵖ M] [inst_6 : IsCentralScalar R M] [inst_7 : TopologicalSpace R]
  [inst_8 : TopologicalSpace M] [inst_9 : IsTopologicalRing R] [inst_10 : IsTopologicalAddGroup M]
  [inst_11 : ContinuousSMul R M] [inst_12 : ContinuousSMul Rᵐᵒᵖ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M),
  x.fst ≠ 0 → x = x.fst • NormedSpace.exp (x.fst⁻¹ • TrivSqZeroExt.inr x.snd)
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.instFinite : ∀ {α₁ α₂ : Type w} {m : Type w → Type w'} {β : Type w} [inst : Monad m] [inst_1 : Std.Iterator α₁ m β]
  [inst_2 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m],
  Std.Iterators.Finite (Std.Iterators.Types.Append α₁ α₂ m β) m
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- If `F : Pseudofunctor B Cat`, this is the data of a property of
objects in all categories `F.obj X` for `X : B`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] → CategoryTheory.Pseudofunctor B CategoryTheory.Cat → Type (max u u')
-- Mathlib.NumberTheory.ArithmeticFunction.Carmichael
/-- **Alias** of `ArithmeticFunction.carmichael`.

---

`λ` is the Carmichael function, also known as the reduced totient function,
defined as the exponent of the unit group of `ZMod n`.  -/
ArithmeticFunction.Carmichael : ArithmeticFunction ℕ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertMany_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  Std.DTreeMap.Const.insertMany t [] = t
-- Lean.Data.Json.Basic
Lean.Json.str.injEq : ∀ (s s_1 : String), (Lean.Json.str s = Lean.Json.str s_1) = (s = s_1)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- a limit kernel fork of `f`  -/
CategoryTheory.Abelian.AbelianStruct.kernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Abelian.AbelianStruct f → CategoryTheory.Limits.KernelFork f
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trAux.match_1.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → σ → Sort u_4) (l : Γ → σ → Λ) (v : σ)
  (h_1 : (d : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.move d q) v)
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.write a q) v)
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.load a q) v)
  (h_4 : (p : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → motive (Turing.TM1.Stmt.goto l) v) (h_6 : (v : σ) → motive Turing.TM1.Stmt.halt v),
  (match Turing.TM1.Stmt.goto l, v with
    | Turing.TM1.Stmt.move d q, v => h_1 d q v
    | Turing.TM1.Stmt.write a q, v => h_2 a q v
    | Turing.TM1.Stmt.load a q, v => h_3 a q v
    | Turing.TM1.Stmt.branch p q₁ q₂, v => h_4 p q₁ q₂ v
    | Turing.TM1.Stmt.goto l, v => h_5 l v
    | Turing.TM1.Stmt.halt, v => h_6 v) =
    h_5 l v
-- Lean.Meta.Basic
Lean.Meta.Cache.defEqTrans : Lean.Meta.Cache → Lean.Meta.DefEqCache
-- Mathlib.RepresentationTheory.FDRep
FDRep.hom_hom_action_ρ : ∀ {R : Type u} {G : Type v} [inst : CommRing R] [inst_1 : Monoid G] (V : FDRep R G) (g : G),
  ModuleCat.Hom.hom (V.ρ g).hom = V.ρ g
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ReducedWord.mk.injEq : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (head : G) (toList : List (ℤˣ × G))
  (chain : List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) toList) (head_1 : G)
  (toList_1 : List (ℤˣ × G))
  (chain_1 : List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) toList_1),
  ({ head := head, toList := toList, chain := chain } = { head := head_1, toList := toList_1, chain := chain_1 }) =
    (head = head_1 ∧ toList = toList_1)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
/-- The map `y ↦ x + y` as a `CircleDeg1Lift`. More precisely, we define a homomorphism from
`Multiplicative ℝ` to `CircleDeg1Liftˣ`, so the translation by `x` is
`translation (Multiplicative.ofAdd x)`.  -/
CircleDeg1Lift.translate : Multiplicative ℝ →* CircleDeg1Liftˣ
-- Mathlib.Order.Atoms
IsAtomistic.mk : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α],
  (∀ (b : α), ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a) → IsAtomistic α
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
SchwartzMap.instFourierTransform : {E : Type u_2} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] →
      {V : Type u_3} →
        [inst_2 : NormedAddCommGroup V] →
          [inst_3 : InnerProductSpace ℝ V] →
            [FiniteDimensional ℝ V] →
              [inst_5 : MeasurableSpace V] → [BorelSpace V] → FourierTransform (SchwartzMap V E) (SchwartzMap V E)
-- Mathlib.Algebra.Category.Ring.Basic
CommSemiRingCat.inv_hom_apply : ∀ {R S : CommSemiRingCat} (e : R ≅ S) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) r) = r
-- Mathlib.Topology.Sheaves.PUnit
TopCat.Presheaf.isSheaf_iff_isTerminal_of_indiscrete : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : TopCat},
  X.str = ⊤ →
    ∀ (F : TopCat.Presheaf C X), F.IsSheaf ↔ Nonempty (CategoryTheory.Limits.IsTerminal (F.obj (Opposite.op ⊥)))
-- Mathlib.Topology.Order.Completion
Order.Fill.continuous_some : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α], Continuous ⇑Order.Fill.some
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.instEquivLike : {A : Type u_1} →
  {B : Type u_2} →
    [inst : Add A] →
      [inst_1 : Add B] →
        [inst_2 : Mul A] → [inst_3 : Mul B] → [inst_4 : Star A] → [inst_5 : Star B] → EquivLike (A ≃⋆+* B) A B
-- Mathlib.Algebra.Group.Opposite
MulOpposite.commute_op : ∀ {α : Type u_1} [inst : Mul α] {x y : α}, Commute (MulOpposite.op x) (MulOpposite.op y) ↔ Commute x y
-- Lean.Environment
_private.Lean.Environment.0.Lean.Kernel.Environment.add : Lean.Kernel.Environment → Lean.ConstantInfo → Lean.Kernel.Environment
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
/-- The **restricted product** of a family `R : ι → Type*` of types, relative to subsets
`A : (i : ι) → Set (R i)` and the filter `𝓕 : Filter ι`, is the set of all `x : Π i, R i`
such that the set `{j | x j ∈ A j}` belongs to `𝓕`. We denote it by `Πʳ i, [R i, A i]_[𝓕]`.

The most common use case is with `𝓕 = cofinite`, in which case the restricted product is the set
of all `x : Π i, R i` such that `x j ∈ A j` for all but finitely many `j`. We denote it simply
by `Πʳ i, [R i, A i]`.

Similarly, if `S` is a principal filter, the restricted product `Πʳ i, [R i, A i]_[𝓟 s]`
is the set of all `x : Π i, R i` such that `∀ j ∈ S, x j ∈ A j`.  -/
RestrictedProduct : {ι : Type u_1} → (R : ι → Type u_2) → ((i : ι) → Set (R i)) → Filter ι → Type (max u_1 u_2)
-- Lean.Elab.Tactic.Grind.Main
/-- Position for the `[..]` child syntax in the `grind` tactic.  -/
Lean.Elab.Tactic.grindParamsPos : ℕ
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_apply_mem`. -/
Submodule.IsCompl.projection_apply_mem : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) (x : E), (p.projection q hpq) x ∈ p
-- Mathlib.Topology.Algebra.Support
tsupport_sub : ∀ {X : Type u_1} {α : Type u_2} [inst : TopologicalSpace X] [inst_1 : SubtractionMonoid α] (f g : X → α),
  (tsupport fun x => f x - g x) ⊆ tsupport f ∪ tsupport g
-- Mathlib.Data.Multiset.Powerset
Multiset.card_powerset : ∀ {α : Type u_1} (s : Multiset α), s.powerset.card = 2 ^ s.card
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk_obj₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (h : Z ⟶ (CategoryTheory.shiftFunctor C 1).obj X),
  (CategoryTheory.Pretriangulated.Triangle.mk f g h).obj₂ = Y
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
CategoryTheory.ObjectProperty.instNonemptyOfIsClosedUnderColimitsOfShapeDiscretePEmptyOfHasInitial : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderColimitsOfShape (CategoryTheory.Discrete PEmpty.{1})] [CategoryTheory.Limits.HasInitial C], P.Nonempty
-- Mathlib.CategoryTheory.Limits.Shapes.SequentialProduct
CategoryTheory.Limits.SequentialProduct.cone_π_app_comp_Pi_π_neg : ∀ {C : Type u_1} {M N : ℕ → C} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : (n : ℕ) → M n ⟶ N n)
  [inst_1 : CategoryTheory.Limits.HasCountableProducts C] (m n : ℕ) (h : ¬n < m),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.SequentialProduct.cone f).π.app (Opposite.op m))
      (CategoryTheory.Limits.Pi.π (fun m_1 => if x : m_1 < Opposite.unop (Opposite.op m) then M m_1 else N m_1) n) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π M n)
      (CategoryTheory.CategoryStruct.comp (f n) (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.pointwise_isCentralScalar : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Monoid α] [inst_2 : MulDistribMulAction α M]
  [inst_3 : MulDistribMulAction αᵐᵒᵖ M] [IsCentralScalar α M], IsCentralScalar α (Submonoid M)
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.sum_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] [inst_7 : ContinuousAdd N] {α : Type u_7} (f : α → M [⋀^ι]→L[R] N) (m : ι → M)
  {s : Finset α}, (∑ a ∈ s, f a) m = ∑ a ∈ s, (f a) m
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.left_induction : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) {P : CliffordAlgebra Q → Prop},
  (∀ (r : R), P ((algebraMap R (CliffordAlgebra Q)) r)) →
    (∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)) →
      (∀ (x : CliffordAlgebra Q) (m : M), P x → P ((CliffordAlgebra.ι Q) m * x)) → ∀ (x : CliffordAlgebra Q), P x
-- Lean.Meta.Basic
/-- We save the `ref` at entry creation time. This is used for reporting errors back to the user.  -/
Lean.Meta.PostponedEntry.ref : Lean.Meta.PostponedEntry → Lean.Syntax
-- Mathlib.Combinatorics.SimpleGraph.VertexCover
/-- A set `c` is a vertex cover iff the complement of `c` is an independent set.  -/
SimpleGraph.isIndepSet_compl_iff_isVertexCover : ∀ {V : Type u_1} {G : SimpleGraph V} {c : Set V}, G.IsIndepSet cᶜ ↔ G.IsVertexCover c
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.instReprKey : Repr Lean.Meta.LazyDiscrTree.Key
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.iSup_iterate_eq_nfp : ∀ (f : Ordinal.{u} → Ordinal.{u}) (a : Ordinal.{u}), ⨆ n, f^[n] a = Ordinal.nfp f a
-- Mathlib.Control.Monad.Cont
ContT : Type u → (Type u → Type v) → Type w → Type (max v w)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
CategoryTheory.IsPushout.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P}
  {inr : Y ⟶ P},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {W : C} {k l : P ⟶ W},
      CategoryTheory.CategoryStruct.comp inl k = CategoryTheory.CategoryStruct.comp inl l →
        CategoryTheory.CategoryStruct.comp inr k = CategoryTheory.CategoryStruct.comp inr l → k = l
-- Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence
/-- The counit isomorphism of the equivalence
`ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C`.  -/
CategoryTheory.ShortComplex.FunctorEquivalence.counitIso : (J : Type u_1) →
  (C : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          (CategoryTheory.ShortComplex.FunctorEquivalence.inverse J C).comp
              (CategoryTheory.ShortComplex.FunctorEquivalence.functor J C) ≅
            CategoryTheory.Functor.id (CategoryTheory.Functor J (CategoryTheory.ShortComplex C))
-- Init.Data.Option.Attach
Option.unattach_attachWith : ∀ {α : Type u_1} {p : α → Prop} {o : Option α} {H : ∀ (a : α), o = some a → p a}, (o.attachWith p H).unattach = o
-- Mathlib.Analysis.Analytic.Inverse
/-- Second technical lemma to control the growth of coefficients of the inverse. Bound the explicit
expression for `∑_{k<n+1} aᵏ Qₖ` in terms of a sum of powers of the same sum one step before,
in the specific setup we are interesting in, by reducing to the general bound in
`radius_rightInv_pos_of_radius_pos_aux1`.  -/
FormalMultilinearSeries.radius_rightInv_pos_of_radius_pos_aux2 : ∀ {𝕜 : 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] {x : E} {n : ℕ},
  2 ≤ n + 1 →
    ∀ (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) {r a C : ℝ},
      0 ≤ r →
        0 ≤ a →
          0 ≤ C →
            (∀ (n : ℕ), ‖p n‖ ≤ C * r ^ n) →
              ∑ k ∈ Finset.Ico 1 (n + 1), a ^ k * ‖p.rightInv i x k‖ ≤
                ‖↑i.symm‖ * a +
                  ‖↑i.symm‖ * C * ∑ k ∈ Finset.Ico 2 (n + 1), (r * ∑ j ∈ Finset.Ico 1 n, a ^ j * ‖p.rightInv i x j‖) ^ k
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_eq_one : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, Associates.mk a = 1 ↔ IsUnit a
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.addCommute_coe_neg : ∀ {α : Type u} [inst : AddMonoid α] (a : AddUnits α), AddCommute ↑a ↑(-a)
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.antidiagonal_eq_map_powerset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.antidiagonal = Multiset.map (fun t => (s - t, t)) s.powerset
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Composition with a continuous linear equiv on the right is a continuous linear map on
Schwartz space.  -/
SchwartzMap.compCLMOfContinuousLinearEquiv : (𝕜 : Type u_2) →
  {D : Type u_4} →
    {E : Type u_5} →
      {F : Type u_6} →
        [inst : NormedAddCommGroup E] →
          [inst_1 : NormedSpace ℝ E] →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                [inst_4 : RCLike 𝕜] →
                  [inst_5 : NormedAddCommGroup D] →
                    [inst_6 : NormedSpace ℝ D] →
                      [inst_7 : NormedSpace 𝕜 F] → (D ≃L[ℝ] E) → SchwartzMap E F →L[𝕜] SchwartzMap D F
-- Mathlib.Combinatorics.Extremal.RuzsaSzemeredi
rothNumberNat_le_ruzsaSzemerediNumberNat : ∀ (n : ℕ), (2 * n + 1) * rothNumberNat n ≤ ruzsaSzemerediNumberNat (6 * n + 3)
-- Mathlib.Order.SymmDiff
symmDiff_comm : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (a b : α), symmDiff a b = symmDiff b a
-- Batteries.Tactic.Case
/-- The body of a `case ... | ...` tactic that's an exact term.  -/
Batteries.Tactic.casePattExpr : Lean.ParserDescr
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.localRingHom_comp : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Type u_3} [inst_1 : CommSemiring P] (I : Ideal R) [hI : I.IsPrime]
  {S : Type u_4} [inst_2 : CommSemiring S] (J : Ideal S) [hJ : J.IsPrime] (K : Ideal P) [hK : K.IsPrime] (f : R →+* S)
  (hIJ : I = Ideal.comap f J) (g : S →+* P) (hJK : J = Ideal.comap g K),
  Localization.localRingHom I K (g.comp f) ⋯ =
    (Localization.localRingHom J K g hJK).comp (Localization.localRingHom I J f hIJ)
-- Std.Sat.CNF.Literal
/-- CNF literals identified by some type `α`. The `Bool` is the polarity of the literal.
`true` means positive polarity.
 -/
Std.Sat.Literal : Type u → Type (max u 0)
-- Lean.Data.KVMap
Lean.KVMap.update : {α : Type} → [Lean.KVMap.Value α] → Lean.KVMap → Lean.Name → (Option α → Option α) → Lean.KVMap
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instOne.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : Nonempty ι]
  [inst_5 : (i : ι) → One (G i)], DirectLimit.instOne = { one := DirectLimit.map₀ f fun x => 1 }
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.sup_apply : ∀ {E : Type u_3} [inst : Group E] (p q : GroupNorm E) (x : E), (p ⊔ q) x = max (p x) (q x)
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
/-- The function `x ↦ - x * log x` from `ℝ` to `ℝ`.  -/
Real.negMulLog : ℝ → ℝ
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.instIsAddMonHomToAddUnit : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D]
  (M : D) [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.IsAddMonHom (CategoryTheory.SemiCartesianMonoidalCategory.toUnit M)
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
/-- A morphism `f : X ⟶ Y` satisfies the existence part of the valuative criterion if
every valuative commutative square over `f` has (at least) a lift.  -/
AlgebraicGeometry.ValuativeCriterion.Existence : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme
-- Mathlib.Algebra.Group.Action.Defs
/-- One is the neutral element for `•`  -/
MulAction.one_smul : ∀ {α : Type u_9} {β : Type u_10} {inst : Monoid α} [self : MulAction α β] (b : β), 1 • b = b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_inter_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₂.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Mathlib.Data.Set.Prod
/-- **Alias** of the reverse direction of `Set.offDiag_nonempty`. -/
Set.Nontrivial.offDiag_nonempty : ∀ {α : Type u_1} {s : Set α}, s.Nontrivial → s.offDiag.Nonempty
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.eq_of_fromFunctionField_eq : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsIntegral X] (f g : X.RationalMap Y),
  f.fromFunctionField = g.fromFunctionField → f = g
-- Mathlib.GroupTheory.Commutator.Basic
commutatorRepresentatives.eq_1 : ∀ (G : Type u_1) [inst : Group G], commutatorRepresentatives G = Set.range fun g => (Exists.choose ⋯, ⋯.choose)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.CooperSplit),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.cooper₁ c) = 1 + sizeOf c
-- Mathlib.Algebra.Lie.Matrix
Matrix.lie_apply : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (A : Matrix n n R)
  (v : n → R), ⁅A, v⁆ = A.mulVec v
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of `x - y` is at most `2 ^ totalWeight K`
times the product of the multiplicative heights of `x` and `y`.  -/
Height.mulHeight₁_sub_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.mulHeight₁ (x - y) ≤ 2 ^ Height.totalWeight K * Height.mulHeight₁ x * Height.mulHeight₁ y
-- Mathlib.CategoryTheory.Monoidal.Closed.Cartesian
/-- Morphisms from an exponentiable object.  -/
CategoryTheory.CartesianClosed.«term_^^_» : Lean.TrailingParserDescr
-- Mathlib.Topology.Basic
isOpen_compl_iff : ∀ {X : Type u} {s : Set X} [inst : TopologicalSpace X], IsOpen sᶜ ↔ IsClosed s
-- Mathlib.MeasureTheory.Integral.Average
/-- **First moment method**. The maximum of an integrable function is greater than its mean, while
avoiding a null set.  -/
MeasureTheory.exists_notMem_null_average_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {N : Set α} {f : α → ℝ}
  [MeasureTheory.IsFiniteMeasure μ], μ ≠ 0 → MeasureTheory.Integrable f μ → μ N = 0 → ∃ x ∉ N, ⨍ (a : α), f a ∂μ ≤ f x
-- Std.Http.Data.Status
/-- 505 HTTP Version Not Supported
 -/
Std.Http.Status.httpVersionNotSupported : Std.Http.Status
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- A function is `m`-`AEMeasurable` with respect to a measure `μ` if it coincides almost everywhere
with a `m`-measurable function.  -/
MeasureTheory.«termAEMeasurable[_]» : Lean.ParserDescr
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectOutput.below.direct : ∀ {α β : Type w} [inst : Std.Iterator α Id β]
  {motive : (a : Std.Iter β) → (a_1 : β) → a.IsPlausibleIndirectOutput a_1 → Prop} {it : Std.Iter β} {out : β}
  (a : it.IsPlausibleOutput out), Std.Iter.IsPlausibleIndirectOutput.below ⋯
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
Polynomial.mem_iff_eq_smul_annIdealGenerator : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] {p : Polynomial 𝕜} (a : A),
  p ∈ Polynomial.annIdeal 𝕜 a ↔ ∃ s, p = s • Polynomial.annIdealGenerator 𝕜 a
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.disjoint_smul_set_smul : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X} {s : Set G} {g : G},
  MulAction.IsBlock G B → ¬g • B ⊆ s • B → Disjoint (g • B) (s • B)
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.mk : (carrier : Type u) → [str : Group carrier] → GrpCat
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm.eq_1 : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : ∀ (x : B), Nonempty (E x)] (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) (b : B) (y : F),
  e.symm b y = if hb : b ∈ e.baseSet then cast ⋯ (↑e.symm (b, y)).snd else Classical.arbitrary (E b)
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.algebraFunctorOfMonadHomId_hom_app_f : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T₁ : CategoryTheory.Monad C} (X : T₁.Algebra),
  (CategoryTheory.Monad.algebraFunctorOfMonadHomId.hom.app X).f =
    (CategoryTheory.Iso.refl
        ((CategoryTheory.Monad.algebraFunctorOfMonadHom (CategoryTheory.CategoryStruct.id T₁)).obj X).A).hom
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.commGrpEquivalence_inverse_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  (X : CategoryTheory.CommGrp C), CategoryTheory.Preadditive.commGrpEquivalence.inverse.obj X = X.X
-- Lean.Language.Basic
Lean.Language.SnapshotTree.brecOn_2.go : {motive_1 : Lean.Language.SnapshotTree → Sort u} →
  {motive_2 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
    {motive_3 : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Sort u} →
      {motive_4 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree → Sort u} →
        {motive_5 : Task Lean.Language.SnapshotTree → Sort u} →
          (t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
            ((t : Lean.Language.SnapshotTree) → t.below → motive_1 t) →
              ((t : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                  Lean.Language.SnapshotTree.below_1 t → motive_2 t) →
                ((t : List (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)) →
                    Lean.Language.SnapshotTree.below_2 t → motive_3 t) →
                  ((t : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) →
                      Lean.Language.SnapshotTree.below_3 t → motive_4 t) →
                    ((t : Task Lean.Language.SnapshotTree) → Lean.Language.SnapshotTree.below_4 t → motive_5 t) →
                      motive_3 t ×' Lean.Language.SnapshotTree.below_2 t