mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {g : β →ₙ+* γ} {f₁ f₂ : α →ₙ+* β},
  Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.mapL_id_id : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G],
  TensorProduct.mapL (ContinuousLinearMap.id 𝕜 E) (ContinuousLinearMap.id 𝕜 G) =
    ContinuousLinearMap.id 𝕜 (TensorProduct 𝕜 E G)
-- Mathlib.RingTheory.Algebraic.Basic
/-- A fraction `(a : S) / (b : S)` can be reduced to `(c : S) / (d : R)`,
if `b` is algebraic over `R`.  -/
Algebra.IsAlgebraic.exists_smul_eq_mul : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [NoZeroDivisors S]
  [Algebra.IsAlgebraic R S] (a : S) {b : S}, b ≠ 0 → ∃ c d, d ≠ 0 ∧ d • a = b * c
-- Mathlib.CategoryTheory.GradedObject
/-- If `X : GradedObject I C` and `p : I → J`, `X.mapObjFun p j` is the family of objects `X i`
for `i : I` such that `p i = j`.  -/
CategoryTheory.GradedObject.mapObjFun : {I : Type u_1} →
  {J : Type u_2} → {C : Type u_4} → CategoryTheory.GradedObject I C → (p : I → J) → (j : J) → ↑(p ⁻¹' {j}) → C
-- Mathlib.Analysis.Calculus.FDeriv.Add
/-- **Alias** of the reverse direction of `hasFDerivAt_const_add_iff`. -/
HasFDerivAt.const_add : ∀ {𝕜 : 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] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} (c : F), HasFDerivAt f f' x → HasFDerivAt (fun x => c + f x) f' x
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.Δ_of_isCharThreeJNeZeroNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3],
  W.Δ = -W.a₂ ^ 3 * W.a₆
-- Mathlib.Data.Finsupp.Basic
Finsupp.restrictSupportEquiv_symm_apply_coe : ∀ {α : Type u_1} (s : Set α) (M : Type u_12) [inst : AddCommMonoid M] [inst_1 : DecidablePred fun x => x ∈ s]
  (f : ↑s →₀ M), ↑((Finsupp.restrictSupportEquiv s M).symm f) = f.extendDomain
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.uniqueDiffOn_preimage_iff : ∀ {𝕜 : 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] {s : Set E}
  (e : F ≃L[𝕜] E), UniqueDiffOn 𝕜 (⇑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s
-- Init.Data.List.Count
List.countP_go_eq_add : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {l : List α}, List.countP.go p l n = n + List.countP.go p l 0
-- Mathlib.Tactic.Abel
/-- The universe level for `α`.  -/
Mathlib.Tactic.Abel.Context.univ : Mathlib.Tactic.Abel.Context → Lean.Level
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.map_preΨ : ∀ {R : Type r} {S : Type s} [inst : CommRing R] [inst_1 : CommRing S] (W : WeierstrassCurve R) (f : R →+* S) (n : ℤ),
  (W.map f).preΨ n = Polynomial.map f (W.preΨ n)
-- Mathlib.RingTheory.Etale.StandardEtale
/-- A `StandardEtalePair R` is a pair `f g : R[X]` such that `f` is monic,
and `f'` is invertible in `R[X][1/g]/f`.  -/
StandardEtalePair : (R : Type u_1) → [CommRing R] → Type u_1
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.image_symm_apply_coe : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (e : X ≃ₜ Y) (s : Set X)
  (y : ↑(⇑e.toEquiv '' s)), ↑((e.image s).symm y) = e.symm ↑y
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α} {h' : k ∈ Std.TreeMap.map f t}, (Std.TreeMap.map f t)[k] = f k t[k]
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.zero_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.Relation F (RingCat.Colimits.Prequotient.zero.mul x) RingCat.Colimits.Prequotient.zero
-- Mathlib.Data.Sum.Order
Sum.Lex.inr_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], Monotone (⇑toLex ∘ Sum.inr)
-- Mathlib.GroupTheory.Abelianization.Defs
/-- Equivalent groups have equivalent abelianizations  -/
MulEquiv.abelianizationCongr : {G : Type u} → [inst : Group G] → {H : Type v} → [inst_1 : Group H] → G ≃* H → Abelianization G ≃* Abelianization H
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.fst_snd_eq_p₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) (hf₁.snd f₂) =
    CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₂ hf₁ f₂ f₃
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.M.mk_inj : ∀ {F : PFunctor.{uA, uB}} {x y : ↑F F.M}, PFunctor.M.mk x = PFunctor.M.mk y → x = y
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] {X Y : C} (f : X ⟶ Y) (X' : C) {Z : D}
  (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y X') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X')
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')) h)
-- Mathlib.Algebra.Category.Ring.Constructions
/-- Verify that the `pushout_cocone` is indeed the colimit.  -/
CommRingCat.pushoutCoconeIsColimit : (R A B : Type u) →
  [inst : CommRing R] →
    [inst_1 : CommRing A] →
      [inst_2 : CommRing B] →
        [inst_3 : Algebra R A] →
          [inst_4 : Algebra R B] → CategoryTheory.Limits.IsColimit (CommRingCat.pushoutCocone R A B)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.app_shift : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    ∀ (X : C),
      τ.app ((CategoryTheory.shiftFunctor C a).obj X) =
        CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).hom.app X)
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X))
            ((CategoryTheory.Functor.commShiftIso F₂ a).inv.app X))
-- Std.Internal.Do.Triple.Basic
/-- Hoare triple notation with an exception postcondition:
`⦃ P ⦄ x ⦃ Q; E ⦄ := Triple x P Q E`.  -/
Std.Internal.Do.tripleEPost : Lean.ParserDescr
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : β}, (t.erase k).getD k fallback = fallback
-- Mathlib.Algebra.Ring.Commute
/-- **Alias** of `neg_sq`. -/
neg_pow_two : ∀ {R : Type u} [inst : Monoid R] [inst_1 : HasDistribNeg R] (a : R), (-a) ^ 2 = a ^ 2
-- Mathlib.Topology.Category.Profinite.Basic
Profinite.toCompHaus.createsLimits : CategoryTheory.CreatesLimits profiniteToCompHaus
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).get? k' = if h : cmp k k' = Ordering.eq then cast ⋯ (f (t.get? k)) else t.get? k'
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- See `le_inv_mul_iff₀'` for a version with multiplication on the other side.  -/
le_inv_mul_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 < c → (a ≤ c⁻¹ * b ↔ c * a ≤ b)
-- Mathlib.MeasureTheory.Group.Prod
MeasurableEquiv.shearDivRight.eq_1 : ∀ (G : Type u_1) [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : MeasurableMul₂ G] [inst_3 : MeasurableInv G],
  MeasurableEquiv.shearDivRight G =
    { toEquiv := (Equiv.refl G).prodShear Equiv.divRight, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensParams.mk.sizeOf_spec : ∀ (textDocument : Lean.Lsp.TextDocumentIdentifier), sizeOf { textDocument := textDocument } = 1 + sizeOf textDocument
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
/-- The condition of being a pointwise right Kan extension at an object `Y` is
unchanged by replacing `Y` by an isomorphic object `Y'`.  -/
CategoryTheory.Functor.RightExtension.isPointwiseRightKanExtensionAtOfIso' : {C : Type u_1} →
  {D : Type u_2} →
    {H : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} H] →
            {L : CategoryTheory.Functor C D} →
              {F : CategoryTheory.Functor C H} →
                (E : L.RightExtension F) →
                  {Y : D} →
                    E.IsPointwiseRightKanExtensionAt Y → {Y' : D} → (Y ≅ Y') → E.IsPointwiseRightKanExtensionAt Y'
-- Mathlib.LinearAlgebra.AnnihilatingPolynomial
/-- If a monic generates the annihilating ideal, it must match our choice
of the annihilating ideal generator.  -/
Polynomial.monic_generator_eq_minpoly : ∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A) (p : Polynomial 𝕜),
  p.Monic → Ideal.span {p} = Polynomial.annIdeal 𝕜 a → Polynomial.annIdealGenerator 𝕜 a = p
-- Mathlib.Combinatorics.SimpleGraph.Girth
/-- **Alias** of the reverse direction of `SimpleGraph.girth_eq_zero`. -/
SimpleGraph.IsAcyclic.girth_eq_zero : ∀ {α : Type u_1} {G : SimpleGraph α}, G.IsAcyclic → G.girth = 0
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.Compacts.t3Space_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α], T3Space (TopologicalSpace.Compacts α) ↔ T3Space α
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.rightDeriv_mul_log : ∀ {x : ℝ}, x ≠ 0 → derivWithin (fun x => x * Real.log x) (Set.Ioi x) x = Real.log x + 1
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.symm : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Reachable u v → G.Reachable v u
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.drain_eq_map_toArray : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β},
  it.drain = (fun x => PUnit.unit) <$> it.toList
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_mul_eq_of_coprime_right : ∀ {R : Type u} [inst : Semiring R] {I J K : Ideal R} [J.IsTwoSided], I ⊔ K = ⊤ → I ⊔ J * K = I ⊔ J
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.insertManyIfNewUnit_list_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtDHashMap α fun x => Unit} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List α}, Std.ExtDHashMap.Const.insertManyIfNewUnit m l = ∅ ↔ m = ∅ ∧ l = []
-- Std.Http.Data.Headers
/-- Retrieves all `Header.Value` entries for the given key.
 -/
Std.Http.Headers.getAll : (headers : Std.Http.Headers) → (name : Std.Http.Header.Name) → name ∈ headers → Array Std.Http.Header.Value
-- Mathlib.Data.Matrix.Mul
Matrix.one_mulVec : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (v : m → α),
  Matrix.mulVec 1 v = v
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.pullbackIsRightAdjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f], (CategoryTheory.Over.pullback f).IsRightAdjoint
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.coeff_apply_lt : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRootMonic S f) (z : S) (i : ℕ) (hi : i < f.natDegree), h.coeff z i = (h.basis.repr z) ⟨i, hi⟩
-- Mathlib.CategoryTheory.Products.Unitor
CategoryTheory.prod.rightUnitorEquivalence_inverse : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  (CategoryTheory.prod.rightUnitorEquivalence C).inverse = CategoryTheory.prod.rightInverseUnitor C
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_inter_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.isEmpty = true → (m₁ ∩ m₂).isEmpty = true
-- Std.Do.SPred.Laws
Std.Do.SPred.and_elim_l : ∀ {σs : List (Type u)} {P Q : Std.Do.SPred σs}, P ∧ Q ⊢ₛ P
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_nat : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : NatCast M] (n : ℕ), ↑↑n = ↑n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_insertIfNew!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).minKey! = k
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.conjTranspose_hadamard : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} [inst : Mul α] [inst_1 : StarMul α] (A B : Matrix m n α),
  (A.hadamard B).conjTranspose = B.conjTranspose.hadamard A.conjTranspose
-- Aesop.Script.StructureDynamic
Aesop.Script.DynStructureM.run : {α : Type} → Aesop.Script.DynStructureM α → Aesop.Script.UScript → Lean.MetaM (α × Bool)
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight_ne_top : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [I.FiniteHeight] [inst_2 : I.IsPrime], Ideal.primeHeight✝ I ≠ ⊤
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEq_hom_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} {f g : β → γ} (h : f = g)
  (X : CategoryTheory.GradedObject γ C) (b : β),
  (CategoryTheory.GradedObject.comapEq C h).hom.app X b = CategoryTheory.eqToHom ⋯
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Equiv.tprod_eq_tprod_of_mulSupport : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α}
  {g : γ → α} (e : ↑(Function.mulSupport f) ≃ ↑(Function.mulSupport g)),
  (∀ (x : ↑(Function.mulSupport f)), g ↑(e x) = f ↑x) → ∏' (x : β), f x = ∏' (y : γ), g y
-- Mathlib.Data.Nat.Digits.Div
Nat.modEq_nine_digits_sum : ∀ (n : ℕ), n ≡ (Nat.digits 10 n).sum [MOD 9]
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arctan`.  -/
EuclideanGeometry.angle_eq_arctan_of_angle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 →
    p₃ ≠ p₂ → EuclideanGeometry.angle p₂ p₃ p₁ = Real.arctan (dist p₁ p₂ / dist p₃ p₂)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcConnectParams.fromJson : Lean.Json → Except String Lean.Lsp.RpcConnectParams
-- Mathlib.Topology.Algebra.Ring.Basic
IsSemitopologicalSemiring.toContinuousAdd : ∀ {R : Type u_2} {inst : TopologicalSpace R} {inst_1 : NonUnitalNonAssocSemiring R}
  [self : IsSemitopologicalSemiring R], ContinuousAdd R
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
Monotone.mul_antitone : ∀ {R : Type u} {α : Type u_1} [inst : Semiring R] [inst_1 : Preorder R] [inst_2 : Preorder α] {f g : α → R}
  [ExistsAddOfLE R] [PosMulMono R] [MulPosMono R] [AddRightMono R] [AddRightReflectLE R],
  Monotone f → Antitone g → (∀ (x : α), 0 ≤ f x) → (∀ (x : α), g x ≤ 0) → Antitone (f * g)
-- Batteries.Data.Array.Scan
Array.toList_scanlM : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} {init : β} [inst : Monad m] [LawfulMonad m] {f : β → α → m β}
  {as : Array α}, Array.toList <$> Array.scanlM f init as = List.scanlM f init as.toList
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_lt_iff_of_nonempty_compact : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [Nonempty α]
  [CompactSpace α] {f : BoundedContinuousFunction α β} {M : ℝ}, ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.prod_smul_left : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {μ : MeasureTheory.Measure α} {R : Type u_4} [inst_3 : SMul R ENNReal]
  [inst_4 : IsScalarTower R ENNReal ENNReal] (c : R), (c • μ).prod ν = c • μ.prod ν
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.of_f : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] {f : (i j : ι) → i ≤ j → G i →ₗ[R] G j}
  [inst_4 : DecidableEq ι] {i j : ι} {hij : i ≤ j} {x : G i},
  (Module.DirectLimit.of R ι G f j) ((f i j hij) x) = (Module.DirectLimit.of R ι G f i) x
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.SmallShiftedHom.comp.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] [inst_3 : W.IsCompatibleWithShift M] {X Y Z : C}
  {a b c : M} [inst_4 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y]
  [inst_5 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Y Z]
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Z]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M Z Z]
  (f f_1 : CategoryTheory.Localization.SmallShiftedHom W X Y a),
  f = f_1 →
    ∀ (g g_1 : CategoryTheory.Localization.SmallShiftedHom W Y Z b),
      g = g_1 → ∀ (h : b + a = c), f.comp g h = f_1.comp g_1 h
-- Mathlib.Algebra.Lie.Nilpotent
Function.Surjective.lieAlgebra_isNilpotent : ∀ {R : Type u} {L : Type v} {L' : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing L'] [inst_4 : LieAlgebra R L'] [h₁ : LieRing.IsNilpotent L] {f : L →ₗ⁅R⁆ L'},
  Function.Surjective ⇑f → LieRing.IsNilpotent L'
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx p =
    match p with
    | Lean.Grind.CommRing.Poly.num k => ↑k
    | Lean.Grind.CommRing.Poly.add k m p =>
      k • Lean.Grind.CommRing.Mon.denote ctx m + Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.GroupTheory.Order.Min
AddMonoid.minOrder.eq_1 : ∀ (α : Type u_2) [inst : AddMonoid α],
  AddMonoid.minOrder α = ⨅ a, ⨅ (_ : a ≠ 0), ⨅ (_ : IsOfFinAddOrder a), ↑(addOrderOf a)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
iteratedDerivWithin_eq_iteratedFDerivWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : ℕ} {f : 𝕜 → F} {s : Set 𝕜} {x : 𝕜},
  iteratedDerivWithin n f s x = (iteratedFDerivWithin 𝕜 n f s x) fun x => 1
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop_of_subsingleton : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} [Subsingleton R],
  x.orderTop = ⊤
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.isGroupoidPi : ∀ {I : Type u} {J : I → Type u₂} [inst : (i : I) → CategoryTheory.Category.{v, u₂} (J i)]
  [∀ (i : I), CategoryTheory.IsGroupoid (J i)], CategoryTheory.IsGroupoid ((i : I) → J i)
-- Mathlib.CategoryTheory.Retract
CategoryTheory.RetractArrow.i_w : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}
  (h : CategoryTheory.RetractArrow f g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.left h.i) g =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.Arrow.Hom.right h.i)
-- Mathlib.Data.Nat.DvdSequence
Nat.IsStrongDvdSequence.id : Nat.IsStrongDvdSequence id
-- Init.Prelude
/-- The `MacroM` monad is the main monad for macro expansion. It has the
information needed to handle hygienic name generation, and is the monad that
`macro` definitions live in.

Notably, this is a (relatively) pure monad: there is no `IO` and no access to
the `Environment`. That means that things like declaration lookup are
impossible here, as well as `IO.Ref` or other side-effecting operations.
For more capabilities, macros can instead be written as `elab` using `adaptExpander`.
 -/
Lean.MacroM : Type → Type
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_eq_get_getKey? : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h : m.WF) {a : α} {h' : a ∈ m}, m.getKey a h' = (m.getKey? a).get ⋯
-- Mathlib.Combinatorics.Additive.SmallTripling
_private.Mathlib.Combinatorics.Additive.SmallTripling.0.Finset.small_pos_pos_neg_add : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : AddGroup G] {A : Finset G} {K : ℝ},
  ↑(3 • A).card ≤ K * ↑A.card → ↑(A + A + -A).card ≤ K ^ 2 * ↑A.card
-- Mathlib.Analysis.Calculus.VectorField
/-- Product rule for Lie Brackets: given two vector fields `V W : E → E` and a function `f : E → 𝕜`,
we have `[f • V, W] = - (df W) • V + f • [V, W]`
 -/
VectorField.lieBracketWithin_smul_left : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s : Set E} {x : E} {f : E → 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    DifferentiableWithinAt 𝕜 V s x →
      UniqueDiffWithinAt 𝕜 s x →
        VectorField.lieBracketWithin 𝕜 (fun y => f y • V y) W s x =
          -(fderivWithin 𝕜 f s x) (W x) • V x + f x • VectorField.lieBracketWithin 𝕜 V W s x
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.lt_iff' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, μ < ν ↔ μ ≤ ν ∧ ∃ s, μ s < ν s
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.mk : {R : Type u_14} →
  {S : Type u_15} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {σ' : S →+* R} →
            [inst_2 : RingHomInvPair σ σ'] →
              [inst_3 : RingHomInvPair σ' σ] →
                {M : Type u_16} →
                  {M₂ : Type u_17} →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module S M₂] →
                            (toLinearMap : M →ₛₗ[σ] M₂) →
                              (invFun : M₂ → M) →
                                autoParam (Function.LeftInverse invFun toLinearMap.toFun) Equiv.left_inv._autoParam →
                                  autoParam (Function.RightInverse invFun toLinearMap.toFun)
                                      Equiv.right_inv._autoParam →
                                    M ≃ₛₗ[σ] M₂