mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Action.Defs
instIsLeftCancelVAdd : ∀ (G : Type u_9) (P : Type u_10) [inst : AddGroup G] [inst_1 : AddAction G P], IsLeftCancelVAdd G P
-- Mathlib.Data.List.Sublists
List.sublists_eq_sublists' : ∀ {α : Type u} (l : List α), l.sublists = List.map List.reverse l.reverse.sublists'
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.instBEqPoly.beq.match_1.eq_2 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) (a : ℤ) (a_1 : Lean.Grind.Linarith.Var)
  (a_2 : Lean.Grind.Linarith.Poly) (b : ℤ) (b_1 : Lean.Grind.Linarith.Var) (b_2 : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (a : ℤ) →
      (a_3 : Lean.Grind.Linarith.Var) →
        (a_4 : Lean.Grind.Linarith.Poly) →
          (b : ℤ) →
            (b_3 : Lean.Grind.Linarith.Var) →
              (b_4 : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a a_3 a_4) (Lean.Grind.Linarith.Poly.add b b_3 b_4))
  (h_3 : (x x_1 : Lean.Grind.Linarith.Poly) → motive x x_1),
  (match Lean.Grind.Linarith.Poly.add a a_1 a_2, Lean.Grind.Linarith.Poly.add b b_1 b_2 with
    | Lean.Grind.Linarith.Poly.nil, Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add a a_3 a_4, Lean.Grind.Linarith.Poly.add b b_3 b_4 => h_2 a a_3 a_4 b b_3 b_4
    | x, x_1 => h_3 x x_1) =
    h_2 a a_1 a_2 b b_1 b_2
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.l2_opNorm_conjTranspose_mul_self : ∀ {𝕜 : Type u_1} {m : Type u_2} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq n] (A : Matrix m n 𝕜), ‖A.conjTranspose * A‖ = ‖A‖ * ‖A‖
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
/-- The `c₆` coefficient of a Weierstrass curve.  -/
WeierstrassCurve.c₆ : {R : Type u} → [CommRing R] → WeierstrassCurve R → R
-- Mathlib.Algebra.Order.Monovary
MonovaryOn.sub_right : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : AddCommGroup β] [inst_2 : LinearOrder β]
  [IsOrderedAddMonoid β] {s : Set ι} {f : ι → α} {g₁ g₂ : ι → β},
  MonovaryOn f g₁ s → AntivaryOn f g₂ s → MonovaryOn f (g₁ - g₂) s
-- Mathlib.Logic.Basic
ite_prop_iff_or : ∀ {P Q R : Prop} [inst : Decidable P], (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
-- Mathlib.Data.Fin.Embedding
Fin.coe_castLEEmb : ∀ {m n : ℕ} (hmn : m ≤ n), ⇑(Fin.castLEEmb hmn) = Fin.castLE hmn
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHomClass.toNonUnitalRingHomClass : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {x : Monoid R} {x_1 : Monoid S}
  {φ : outParam (R →* S)} {x_2 : NonUnitalNonAssocSemiring A} [inst : DistribMulAction R A]
  {x_3 : NonUnitalNonAssocSemiring B} [inst_1 : DistribMulAction S B] [inst_2 : FunLike F A B]
  [NonUnitalAlgSemiHomClass F φ A B], NonUnitalRingHomClass F A B
-- Mathlib.Topology.Constructions
/-- Cofinite topology. A set is open if it's empty or cofinite.  -/
TopologicalSpace.cofinite : {X : Type u_5} → TopologicalSpace X
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.of_bounded_enorm : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [MeasureTheory.IsFiniteMeasure μ] {f : α → ε} {C : ENNReal},
  autoParam (‖C‖ₑ ≠ ⊤) MeasureTheory.HasFiniteIntegral.of_bounded_enorm._auto_1 →
    (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ ≤ C) → MeasureTheory.HasFiniteIntegral f μ
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Year.Offset` from a `PlainDateTime`, adjusting the day to the last valid day of the
resulting month.
 -/
Std.Time.PlainDateTime.subYearsClip : Std.Time.PlainDateTime → Std.Time.Year.Offset → Std.Time.PlainDateTime
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.eqToHom_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (h : f = g),
  CategoryTheory.Over.Hom.left (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.dfoldCast : {n : ℕ} →
  (α : (i : ℕ) → autoParam (i ≤ n) Nat.dfoldCast._auto_1✝ → Type u) →
    {i j : ℕ} → {hi : i ≤ n} → (w : i = j) → α i hi → α j ⋯
-- Mathlib.Algebra.Group.Units.Defs
IsUnit.unit_spec : ∀ {M : Type u_1} [inst : Monoid M] {a : M} (h : IsUnit a), ↑h.unit = a
-- Mathlib.Data.Ineq
Mathlib.Ineq.noConfusionType : Sort v✝ → Mathlib.Ineq → Mathlib.Ineq → Sort v✝
-- Mathlib.Data.Bracket
/-- The `Bracket` class has three intended uses:
1. for certain binary operations on structures, like the product `⁅x, y⁆` of two elements
  `x`, `y` in a Lie algebra or the commutator of two elements `x` and `y` in a group.
2. for certain actions of one structure on another, like the action `⁅x, m⁆` of an element `x`
  of a Lie algebra on an element `m` in one of its modules (analogous to `SMul` in the
  associative setting).
3. for binary operations on substructures, like the commutator `⁅H, K⁆` of two subgroups `H` and
   `K` of a group.
 -/
Bracket : Type u_1 → Type u_2 → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Limits.WeightedCone.IsLimit.fac : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {W : CategoryTheory.Functor J (Type w)} {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.WeightedCone W F}
  (hc : c.IsLimit) {Z : C} (π : ⦃j : J⦄ → W.obj j → (Z ⟶ F.obj j))
  (hπ :
    ∀ ⦃j₁ j₂ : J⦄ (x : W.obj j₁) (f : j₁ ⟶ j₂),
      CategoryTheory.CategoryStruct.comp (π x) (F.map f) = π ((CategoryTheory.ConcreteCategory.hom (W.map f)) x))
  {j : J} (x : W.obj j), CategoryTheory.CategoryStruct.comp (hc.lift π hπ) (c.π x) = π x
-- Mathlib.Data.SetLike.Basic
SetLike.coe_set_eq : ∀ {A : Type u_1} {B : Type u_2} [i : SetLike A B] {p q : A}, ↑p = ↑q ↔ p = q
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.supSet : {V : Type u} → SupSet (SimpleGraph V)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  k ∈ Std.ExtDHashMap.Const.insertMany m l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true
-- Mathlib.Algebra.Group.Action.Defs
Function.Surjective.mulAction.eq_1 : ∀ {M : Type u_1} {α : Type u_5} {β : Type u_6} [inst : Monoid M] [inst_1 : MulAction M α] [inst_2 : SMul M β]
  (f : α → β) (hf : Function.Surjective f) (smul : ∀ (c : M) (x : α), f (c • x) = c • f x),
  Function.Surjective.mulAction f hf smul = { toSMul := inst_2, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Order.LiminfLimsup
Filter.exists_forall_mem_of_hasBasis_mem_blimsup : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {l : Filter β} {b : ι → Set β} {q : ι → Prop},
  l.HasBasis q b →
    ∀ {u : β → Set α} {p : β → Prop} {x : α},
      x ∈ Filter.blimsup u l p → ∃ f, ∀ (i : ↑{i | q i}), x ∈ u (f i) ∧ p (f i) ∧ f i ∈ b ↑i
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.IndParallelPairPresentation.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} {f g : A ⟶ B}
  [inst_1 : SizeOf C] (I : Type v₁) [ℐ : CategoryTheory.SmallCategory I] [hI : CategoryTheory.IsFiltered I]
  (F₁ F₂ : CategoryTheory.Functor I C) (ι₁ : F₁.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj A)
  (isColimit₁ : CategoryTheory.Limits.IsColimit { pt := A, ι := ι₁ })
  (ι₂ : F₂.comp CategoryTheory.yoneda ⟶ (CategoryTheory.Functor.const I).obj B)
  (isColimit₂ : CategoryTheory.Limits.IsColimit { pt := B, ι := ι₂ }) (φ ψ : F₁ ⟶ F₂)
  (hf : f = isColimit₁.map { pt := B, ι := ι₂ } (CategoryTheory.Functor.whiskerRight φ CategoryTheory.yoneda))
  (hg : g = isColimit₁.map { pt := B, ι := ι₂ } (CategoryTheory.Functor.whiskerRight ψ CategoryTheory.yoneda)),
  sizeOf
      { I := I, ℐ := ℐ, hI := hI, F₁ := F₁, F₂ := F₂, ι₁ := ι₁, isColimit₁ := isColimit₁, ι₂ := ι₂,
        isColimit₂ := isColimit₂, φ := φ, ψ := ψ, hf := hf, hg := hg } =
    1 + sizeOf I + sizeOf ℐ + sizeOf hI + sizeOf F₁ + sizeOf F₂ + sizeOf ι₁ + sizeOf isColimit₁ + sizeOf ι₂ +
              sizeOf isColimit₂ +
            sizeOf φ +
          sizeOf ψ +
        sizeOf hf +
      sizeOf hg
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.varFinsetLeft.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} [inst : DecidableEq α] (l : ℕ) (_f : L.Functions l)
  (ts : Fin l → L.Term (α ⊕ β)),
  (FirstOrder.Language.func _f ts).varFinsetLeft = Finset.univ.biUnion fun i => (ts i).varFinsetLeft
-- Init.Data.BitVec.Lemmas
BitVec.toInt_sub : ∀ {w : ℕ} {x y : BitVec w}, (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w)
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instSup : {α : Type u_1} → [inst : MeasurableSpace α] → Max (Subtype MeasurableSet)
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
CategoryTheory.Presheaf.preservesLimit_eq_isLocal_single : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} J]
  [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] {F : CategoryTheory.Functor J Cᵒᵖ}
  {c : CategoryTheory.Limits.Cone F}
  {c' : CategoryTheory.Limits.Cocone (F.leftOp.comp CategoryTheory.shrinkYoneda.{w, v, u})}
  (hc : CategoryTheory.Limits.IsLimit c) (hc' : CategoryTheory.Limits.IsColimit c'),
  CategoryTheory.ObjectProperty.preservesLimit F =
    (CategoryTheory.MorphismProperty.single (CategoryTheory.Presheaf.coconePtToShrinkYoneda c hc')).isLocal
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_snd : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B],
  ↑(ContinuousAlgHom.snd R A B) = AlgHom.snd R A B
-- Mathlib.MeasureTheory.Function.EssSup
OrderIso.essSup_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice β] {x : MeasurableSpace α} {γ : Type u_3}
  [inst_1 : ConditionallyCompleteLattice γ] (f : α → β) (μ : MeasureTheory.Measure α) (g : β ≃o γ),
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) OrderIso.essSup_apply._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) f) OrderIso.essSup_apply._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) fun x => g (f x))
          OrderIso.essSup_apply._auto_5 →
        autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) (MeasureTheory.ae μ) fun x => g (f x))
            OrderIso.essSup_apply._auto_7 →
          g (essSup f μ) = essSup (fun x => g (f x)) μ
-- Mathlib.GroupTheory.Congruence.Hom
Con.ker_mkMulHom_eq : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), Con.ker c.mkMulHom = c
-- Mathlib.NumberTheory.LSeries.Linearity
LSeriesSummable.neg_iff : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeriesSummable (-f) s ↔ LSeriesSummable f s
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformity_translate_mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] (a : α),
  Filter.map (fun x => (x.1 * a, x.2 * a)) (uniformity α) = uniformity α
-- Mathlib.CategoryTheory.ObjectProperty.SiteLocal
CategoryTheory.ObjectProperty.IsLocal.of_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
  {K L : CategoryTheory.Precoverage C} [P.IsLocal L], K ≤ L → P.IsLocal K
-- Init.Data.List.Nat.TakeDrop
List.getElem?_take : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, (List.take i l)[j]? = if j < i then l[j]? else none
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infiniteNeg_iff : ∀ {x : ℝ*}, x.InfiniteNeg ↔ x < 0 ∧ ArchimedeanClass.mk x < 0
-- Std.Http.Data.Status
/-- Attempts to create a `CustomStatus` from a numeric code and a reason phrase string, returning
`none` if the phrase contains invalid characters.
 -/
Std.Http.CustomStatus.ofCodeAndPhrase? : UInt16 → String → Option Std.Http.CustomStatus
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- `MonoOver.map` commutes with composition (up to a natural isomorphism).  -/
CategoryTheory.MonoOver.mapComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          [inst_1 : CategoryTheory.Mono f] →
            [inst_2 : CategoryTheory.Mono g] →
              CategoryTheory.MonoOver.map (CategoryTheory.CategoryStruct.comp f g) ≅
                (CategoryTheory.MonoOver.map f).comp (CategoryTheory.MonoOver.map g)
-- Init.Data.Int.Lemmas
Int.instAssociativeHAdd : Std.Associative fun x1 x2 => x1 + x2
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCallsParams.mk.sizeOf_spec : ∀ (item : Lean.Lsp.CallHierarchyItem), sizeOf { item := item } = 1 + sizeOf item
-- Mathlib.LinearAlgebra.TensorProduct.Basis
Module.Basis.tensorProduct_apply' : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} {ι : Type u_5} {κ : Type u_6} [inst : CommSemiring R]
  [inst_1 : Semiring S] [inst_2 : Algebra R S] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M]
  [inst_6 : IsScalarTower R S M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] (b : Module.Basis ι S M)
  (c : Module.Basis κ R N) (i : ι × κ), (b.tensorProduct c) i = b i.1 ⊗ₜ[R] c i.2
-- Mathlib.Data.DFinsupp.BigOperators
AddMonoidHom.dfinsuppSum_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddZeroClass R] [inst_4 : AddCommMonoid S]
  (f : Π₀ (i : ι), β i) (g : (i : ι) → β i → R →+ S) (r : R), (f.sum g) r = f.sum fun a b => (g a b) r
-- Mathlib.LinearAlgebra.Matrix.Reindex
/-- `Matrix.reindex` as an `AddEquiv` between `R`-matrices.  -/
Matrix.reindexAddEquiv : {m : Type u_2} →
  {n : Type u_3} →
    {m' : Type u_6} →
      {n' : Type u_7} → (R : Type u_11) → [inst : Add R] → m ≃ m' → n ≃ n' → Matrix m n R ≃+ Matrix m' n' R
-- Init.Tactics
/-- `mspec` is an `apply`-like tactic that applies a Hoare triple specification to the target of the
stateful goal.

Given a stateful goal `H ⊢ₛ wp⟦prog⟧ Q'`, `mspec foo_spec` will instantiate
`foo_spec : ... → ⦃P⦄ foo ⦃Q⦄`, match `foo` against `prog` and produce subgoals for
the verification conditions `?pre : H ⊢ₛ P` and `?post : Q ⊢ₚ Q'`.

* If `prog = x >>= f`, then `mspec Specs.bind` is tried first so that `foo` is matched against `x`
  instead. Tactic `mspec_no_bind` does not attempt to do this decomposition.
* If `?pre` or `?post` follow by `.rfl`, then they are discharged automatically.
* `?post` is automatically simplified into constituent `⊢ₛ` entailments on
  success and failure continuations.
* `?pre` and `?post.*` goals introduce their stateful hypothesis under an inaccessible name.
  You can give it a name with the `mrename_i` tactic.
* Any uninstantiated MVar arising from instantiation of `foo_spec` becomes a new subgoal.
* If the target of the stateful goal looks like `fun s => _` then `mspec` will first `mintro ∀s`.
* If `P` has schematic variables that can be instantiated by doing `mintro ∀s`, for example
  `foo_spec : ∀(n:Nat), ⦃fun s => ⌜n = s⌝⦄ foo ⦃Q⦄`, then `mspec` will do `mintro ∀s` first to
  instantiate `n = s`.
* Right before applying the spec, the `mframe` tactic is used, which has the following effect:
  Any hypothesis `Hᵢ` in the goal `h₁:H₁, h₂:H₂, ..., hₙ:Hₙ ⊢ₛ T` that is
  pure (i.e., equivalent to some `⌜φᵢ⌝`) will be moved into the pure context as `hᵢ:φᵢ`.

Additionally, `mspec` can be used without arguments or with a term argument:

* `mspec` without argument will try and look up a spec for `x` registered with `@[spec]`.
* `mspec (foo_spec blah ?bleh)` will elaborate its argument as a term with expected type
  `⦃?P⦄ x ⦃?Q⦄` and introduce `?bleh` as a subgoal.
  This is useful to pass an invariant to e.g., `Specs.forIn_list` and leave the inductive step
  as a hole.
 -/
Lean.Parser.Tactic.mspecMacro : Lean.ParserDescr
-- Mathlib.Data.DFinsupp.Order
DFinsupp.bot_eq_zero : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → AddCommMonoid (α i)] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : ∀ (i : ι), IsBotZeroClass (α i)], ⊥ = 0
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.LawfulMonadLiftBindFunction : {m : Type u → Type v} →
  {n : Type w → Type x} → [Monad m] → [Monad n] → ((γ : Type u) → (δ : Type w) → (γ → n δ) → m γ → n δ) → Prop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
  {fallback : β k}, (List.map Sigma.fst l).contains k = false → (t.insertMany l).getD k fallback = t.getD k fallback
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.lipschitzWith_cos : LipschitzWith 1 Real.cos
-- Mathlib.Order.Hom.Bounded
TopHom.instMin.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : SemilatticeInf β] [inst_2 : OrderTop β],
  TopHom.instMin = { min := fun f g => { toFun := ⇑f ⊓ ⇑g, map_top' := ⋯ } }
-- Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
/-- The canonical map from a direct sum of tensor powers to the tensor algebra.  -/
TensorAlgebra.ofDirectSum : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] → (DirectSum ℕ fun n => TensorPower R n M) →ₐ[R] TensorAlgebra R M
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.self_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {kmi : α}, (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Init.Data.Nat.Div.Basic
Nat.mod.eq_1 : ∀ (x : ℕ), Nat.mod 0 x = 0
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.inducedMap_rat : ∀ (α : Type u_2) (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (q : ℚ),
  ConditionallyCompleteLinearOrderedField.inducedMap α β ↑q = ↑q
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A convex cone is salient if it doesn't include `x` and `-x` for any nonzero `x`.  -/
ConvexCone.Salient : {R : Type u_2} →
  {G : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommGroup G] → [inst_3 : SMul R G] → ConvexCone R G → Prop
-- Mathlib.RingTheory.LocalRing.LocalSubring
LocalSubring.le_ofPrime : ∀ {K : Type u_3} [inst : Field K] (A : Subring K) (P : Ideal ↥A) [inst_1 : P.IsPrime],
  A ≤ (LocalSubring.ofPrime A P).toSubring
-- Mathlib.Analysis.Calculus.FDeriv.Mul
DifferentiableOn.const_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a : E → 𝔸}, DifferentiableOn 𝕜 a s → ∀ (b : 𝔸), DifferentiableOn 𝕜 (fun y => b * a y) s
-- Mathlib.Algebra.BigOperators.Associated
/-- **Alias** of `Prime.dvd_finsetProd_iff`. -/
Prime.dvd_finset_prod_iff : ∀ {M₀ : Type u_3} {M : Type u_4} [inst : CommMonoidWithZero M] {S : Finset M₀} {p : M},
  Prime p → ∀ (g : M₀ → M), p ∣ S.prod g ↔ ∃ a ∈ S, p ∣ g a
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.toFilter_neBot : ∀ {ι : Type u_1} [inst : Fintype ι] (l : BoxIntegral.IntegrationParams) (I : BoxIntegral.Box ι), (l.toFilter I).NeBot
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : m.WF)
  {hc : k' ∈ Std.DHashMap.Raw.Const.alter m k f},
  Std.DHashMap.Raw.Const.get (Std.DHashMap.Raw.Const.alter m k f) k' hc =
    if heq : (k == k') = true then (f (Std.DHashMap.Raw.Const.get? m k)).get ⋯ else Std.DHashMap.Raw.Const.get m k' ⋯
-- Init.Data.UInt.Lemmas
USize.toNat_toBitVec : ∀ (x : USize), x.toBitVec.toNat = x.toNat
-- Mathlib.Topology.Separation.Basic
r1Space_iff_inseparable_or_disjoint_nhds : ∀ {X : Type u_3} [inst : TopologicalSpace X], R1Space X ↔ ∀ (x y : X), Inseparable x y ∨ Disjoint (nhds x) (nhds y)
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Construct a term of `ProfiniteGrp` from a type endowed with the structure of a
compact and totally disconnected topological group.
(The condition of being Hausdorff can be omitted here because totally disconnected implies that
`{1}` is a closed set, thus implying Hausdorff in a topological group.)  -/
ProfiniteGrp.of : (G : Type u) →
  [inst : Group G] →
    [inst_1 : TopologicalSpace G] →
      [IsTopologicalGroup G] → [CompactSpace G] → [TotallyDisconnectedSpace G] → ProfiniteGrp.{u}
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_neg_left : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  (t : Finset ι) {w : ι → R} (z : ι → E), t.centerMass (-w) z = t.centerMass w z
-- Mathlib.RingTheory.Congruence.Basic
/-- There is a Galois insertion of congruence relations on a type with multiplication and addition
`R` into binary relations on `R`.  -/
RingCon.gi : (R : Type u_3) → [inst : Add R] → [inst_1 : Mul R] → GaloisInsertion ringConGen DFunLike.coe
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The type of TM2 configurations used by this machine.  -/
Turing.PartrecToTM2.Cfg' : Type
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_ofReal_mul : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ) (z : K), RCLike.re (↑r * z) = r * RCLike.re z
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.parenthesizeCommand : Lean.Syntax → Lean.CoreM Lean.Syntax
-- Init.Core
not_true : ¬True ↔ False
-- Mathlib.Analysis.RCLike.Basic
RCLike.natCast_im : ∀ {K : Type u_1} [inst : RCLike K] (n : ℕ), RCLike.im ↑n = 0
-- Mathlib.Probability.Decision.BayesEstimator
/-- An argmin estimator is a Bayes estimator: that is, it minimizes the Bayesian risk.  -/
ProbabilityTheory.IsArgminEstimator.isBayesEstimator : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {π : MeasureTheory.Measure Θ}
  [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ] {f : 𝓧 → 𝓨} [inst_2 : ProbabilityTheory.IsFiniteKernel P]
  [inst_3 : MeasureTheory.IsFiniteMeasure π] (hf : ProbabilityTheory.IsArgminEstimator ℓ P π f),
  Measurable (Function.uncurry ℓ) → ProbabilityTheory.IsBayesEstimator ℓ P hf.kernel π
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey!_eq_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  [inst_1 : Inhabited α] {k : α}, k ∈ m → m.getKey! k = k
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.trailingDegree_eq_natTrailingDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p ≠ 0 → p.trailingDegree = ↑p.natTrailingDegree
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₂.get k ⋯
-- Mathlib.Algebra.Lie.Basis.Basic
/-- Lemma 4.5 from [Geck](Geck2017).  -/
LieAlgebra.Basis.iSup_cartan_borelLower_borelUpper_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H),
  iSup ![H.toLieSubmodule, b.borelLower, b.borelUpper] = ⊤
-- Init.Data.SInt.Bitwise
Int8.toISize_or : ∀ (a b : Int8), (a ||| b).toISize = a.toISize ||| b.toISize