mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainRingEquiv_trans : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} {O : Type u_8} [inst : Semiring R] [inst_1 : Monoid M]
  [inst_2 : Monoid N] [inst_3 : Monoid O] (e₁ : M ≃* N) (e₂ : N ≃* O),
  MonoidAlgebra.mapDomainRingEquiv R (e₁.trans e₂) =
    (MonoidAlgebra.mapDomainRingEquiv R e₁).trans (MonoidAlgebra.mapDomainRingEquiv R e₂)
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.j_of_isShortNF : ∀ {F : Type u_2} [inst : Field F] (W : WeierstrassCurve F) [inst_1 : W.IsElliptic] [W.IsShortNF],
  W.j = 6912 * W.a₄ ^ 3 / (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coe_add : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} [inst : Add M] (f g : α → M), ↑(f + g) = ↑f + ↑g
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.sdiff_eq_inter_compl : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α), s \ t = s ∩ tᶜ
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey? k = m₂.getKey? k
-- Mathlib.Topology.Order.WithTop
WithBot.continuous_coe : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  Continuous WithBot.some
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instMulOne : {α : Type u_1} → [MulOne α] → MulOne αᵐᵒᵖ
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
/-- Each element of `GL(2, ℝ)⁺` defines a complex-differentiable map `ℍ → ℍ`.  -/
UpperHalfPlane.mdifferentiable_smul : ∀ {g : GL (Fin 2) ℝ}, 0 < ↑(Matrix.GeneralLinearGroup.det g) → MDiff fun τ => g • τ
-- Mathlib.Data.PNat.Factors
PrimeMultiset.coeNat_injective : Function.Injective PrimeMultiset.toNatMultiset
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertList.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)), Std.Internal.List.insertList l [] = l
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The object of `C` represented by `x : MonoidalOpposite C`.  -/
CategoryTheory.MonoidalOpposite.unmop : {C : Type u₁} → Cᴹᵒᵖ → C
-- Init.Data.Array.MapIdx
Array.mapFinIdx_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α} {f : (i : ℕ) → α → i < 1 → β},
  #[a].mapFinIdx f = #[f 0 a Array.mapFinIdx_singleton._proof_1]
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.AContext.mk.sizeOf_spec : ∀ (fvars : Array Lean.Expr) (propToFVar : Lean.ExprMap Lean.Expr) (depth : ℕ) (initLCtx : Lean.LocalContext)
  (config : Batteries.Tactic.GeneralizeProofs.Config),
  sizeOf { fvars := fvars, propToFVar := propToFVar, depth := depth, initLCtx := initLCtx, config := config } =
    1 + sizeOf fvars + sizeOf propToFVar + sizeOf depth + sizeOf initLCtx + sizeOf config
-- Mathlib.Algebra.Order.Antidiag.Finsupp
Finset.finsuppAntidiag_empty_of_ne_zero : ∀ {ι : Type u_1} {μ : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid μ] [inst_2 : Finset.HasAntidiagonal μ]
  [inst_3 : DecidableEq μ] {n : μ}, n ≠ 0 → ∅.finsuppAntidiag n = ∅
-- Mathlib.RingTheory.Etale.Weakly
Algebra.weaklyEtale_iff : ∀ (R : Type u_3) (S : Type u_4) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  Algebra.WeaklyEtale R S ↔
    autoParam (Module.Flat R S) Algebra.WeaklyEtale.flat._autoParam ∧ (Algebra.TensorProduct.lmul' R).Flat
-- Mathlib.Order.Bounded
Set.unbounded_le_Ici : ∀ {α : Type u_1} [inst : SemilatticeSup α] [NoMaxOrder α] (a : α), Set.Unbounded (fun x1 x2 => x1 ≤ x2) (Set.Ici a)
-- Init.Data.List.ToArray
List.erase_toArray : ∀ {α : Type u_1} [inst : BEq α] {as : List α} {a : α}, as.toArray.erase a = (as.erase a).toArray
-- Mathlib.CategoryTheory.Limits.Skeleton
CategoryTheory.Limits.hasColimitsOfShape_skeleton : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  [CategoryTheory.Limits.HasColimitsOfShape J C], CategoryTheory.Limits.HasColimitsOfShape J (CategoryTheory.Skeleton C)
-- Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ
_private.Mathlib.AlgebraicGeometry.EllipticCurve.IsomOfJ.0.WeierstrassCurve.exists_variableChange_of_char_two : ∀ {F : Type u_1} [inst : Field F] [IsSepClosed F] (E E' : WeierstrassCurve F) [inst_2 : E.IsElliptic]
  [inst_3 : E'.IsElliptic] [CharP F 2], E.j = E'.j → ∃ C, C • E = E'
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.contractibleTriangle_mor₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C),
  (CategoryTheory.Pretriangulated.contractibleTriangle X).mor₁ = CategoryTheory.CategoryStruct.id X
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleIdIso_hom_app_hom₁ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Functor.mapTriangleIdIso C).hom.app X).hom₁ = CategoryTheory.CategoryStruct.id X.obj₁
-- Lean.Syntax
Lean.Syntax.TopDown.stx : Lean.Syntax.TopDown → Lean.Syntax
-- Mathlib.Order.Heyting.Basic
/-- `true → p ↔ p`  -/
top_himp : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a : α}, ⊤ ⇨ a = a
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The category of types has `Π j, f j` as the product of a type family `f : J → Type max v u`.
 -/
CategoryTheory.Limits.Types.productLimitCone : {J : Type v} → (F : J → Type (max v u)) → CategoryTheory.Limits.LimitCone (CategoryTheory.Discrete.functor F)
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_eq_top_iff : ∀ (S : Type u_1) (R : Type u_2) (M : Type u_3) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M] {p : Submodule R M},
  Submodule.restrictScalars S p = ⊤ ↔ p = ⊤
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.isUltrametricDist_of_forall_norm_mul_le_max_norm : ∀ {S' : Type u_2} [inst : SeminormedGroup S'], (∀ (x y : S'), ‖x * y‖ ≤ max ‖x‖ ‖y‖) → IsUltrametricDist S'
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabTypeStx : Lean.Elab.Term.TermElab
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel.name : String → Lean.Elab.InlayHintLabel
-- Mathlib.Algebra.GroupWithZero.Action.Opposite
MulOpposite.instMulActionWithZero : {M : Type u_1} →
  {α : Type u_2} →
    [inst : MonoidWithZero M] → [inst_1 : AddMonoid α] → [MulActionWithZero M α] → MulActionWithZero M αᵐᵒᵖ
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.ext_of_adjoin_eq_top : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B]
  [inst_7 : StarRing B] [inst_8 : StarModule R A] [inst_9 : FunLike F A B] [AlgHomClass F R A B] [StarHomClass F A B]
  {s : Set A}, StarAlgebra.adjoin R s = ⊤ → ∀ ⦃f g : F⦄, Set.EqOn (⇑f) (⇑g) s → f = g
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α} {fallback : β}, (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Init.Data.String.Lemmas.Modify
String.mapAux.induct_unfolding : ∀ (f : Char → Char) (motive : (s : String) → s.Pos → String → Prop),
  (∀ (s : String), motive s s.endPos s) →
    (∀ (s : String) (p : s.Pos) (h : ¬p = s.endPos),
        motive (p.modify f h) (p.pastModify f h) (String.mapAux f (p.modify f h) (p.pastModify f h)) →
          motive s p (String.mapAux f (p.modify f h) (p.pastModify f h))) →
      ∀ (s : String) (p : s.Pos), motive s p (String.mapAux f s p)
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.instIteratorLoop.loop.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α] {n : Type u → Type w}
  [inst_5 : Monad n] (γ : Type u) (Pl : α → γ → ForInStep γ → Prop) (LargeEnough : α → Prop)
  (hl : ∀ (a b : α), a ≤ b → LargeEnough a → LargeEnough b) (upperBound : α) (acc : γ) (next : α) (h : LargeEnough next)
  (f : (out : α) → LargeEnough out → out ≤ upperBound → (c : γ) → n (Subtype (Pl out c))),
  Std.Rxc.Iterator.instIteratorLoop.loop γ Pl LargeEnough hl upperBound acc next h f =
    WellFounded.extrinsicFix₃
      (InvImage (Std.IteratorLoop.rel (Std.Rxc.Iterator α) Id Pl) fun x =>
        ({ internalState := { next := some x.fst, upperBound := upperBound } }, x.snd.fst))
      (fun next acc h G =>
        if hu : next ≤ upperBound then do
          let __do_lift ← f next h hu acc
          match __do_lift with
            | ⟨ForInStep.yield acc', h'⟩ =>
              match hs : Std.PRange.succ? next with
              | some next' => G next' acc' ⋯ ⋯
              | none => pure acc'
            | ⟨ForInStep.done acc', property⟩ => pure acc'
        else pure acc)
      next acc h
-- Init.Core
/-- `∅` or `{}` is the empty set or empty collection.
It is supported by the `EmptyCollection` typeclass. 

Conventions for notations in identifiers:

 * The recommended spelling of `∅` in identifiers is `empty`. -/
«term∅» : Lean.ParserDescr
-- Mathlib.Data.List.Lemmas
_private.Mathlib.Data.List.Lemmas.0.List.mapAccumr.match_1.eq_2 : ∀ {α : Type u_1} {γ : Type u_3} (motive : List α → γ → Sort u_2) (y : α) (yr : List α) (c : γ)
  (h_1 : (c : γ) → motive [] c) (h_2 : (y : α) → (yr : List α) → (c : γ) → motive (y :: yr) c),
  (match y :: yr, c with
    | [], c => h_1 c
    | y :: yr, c => h_2 y yr c) =
    h_2 y yr c
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
/-- The tangent of a complex number is equal to zero
iff this number is equal to `k * π / 2` for an integer `k`.

Note that this lemma takes into account that we use zero as the junk value for division by zero.
See also `Complex.tan_eq_zero_iff'`.  -/
Complex.tan_eq_zero_iff : ∀ {θ : ℂ}, Complex.tan θ = 0 ↔ ∃ k, ↑k * ↑Real.pi / 2 = θ
-- Mathlib.Analysis.Normed.Group.AddTorsor
NormedAddTorsor.to_isIsIsometricVAdd : ∀ {V : Type u_2} {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P], IsIsometricVAdd V P
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Given a functor `F : C₀ ⥤ C`, Grothendieck topologies `J₀` on `C₀`, this is
the property that any object in `C` has a `1`-hypercover consisting of objects in `C₀`.  -/
CategoryTheory.Functor.IsOneHypercoverDense : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        CategoryTheory.Functor C₀ C →
          CategoryTheory.GrothendieckTopology C₀ → CategoryTheory.GrothendieckTopology C → Prop
-- Mathlib.Analysis.Complex.Conformal
IsConformalMap.is_complex_or_conj_linear : ∀ {g : ℂ →L[ℝ] ℂ},
  IsConformalMap g →
    (∃ map, ContinuousLinearMap.restrictScalars ℝ map = g) ∨
      ∃ map, ContinuousLinearMap.restrictScalars ℝ map = g ∘SL ↑Complex.conjCLE
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If orders are finite, the divisor of the scalar product of two meromorphic functions is the sum of
the divisors.

See `MeromorphicOn.exists_order_ne_top_iff_forall` and
`MeromorphicOn.order_ne_top_of_isPreconnected` for two convenient criteria to guarantee conditions
`h₂f₁` and `h₂f₂`.
 -/
MeromorphicOn.divisor_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f₁ : 𝕜 → 𝕜} {f₂ : 𝕜 → E},
  MeromorphicOn f₁ U →
    MeromorphicOn f₂ U →
      (∀ z ∈ U, meromorphicOrderAt f₁ z ≠ ⊤) →
        (∀ z ∈ U, meromorphicOrderAt f₂ z ≠ ⊤) →
          MeromorphicOn.divisor (f₁ • f₂) U = MeromorphicOn.divisor f₁ U + MeromorphicOn.divisor f₂ U
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- The composition of morphisms with chosen pullbacks has a chosen pullback.  -/
CategoryTheory.ChosenPullbacksAlong.comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      (f : X ⟶ Y) →
        (g : Y ⟶ Z) →
          [CategoryTheory.ChosenPullbacksAlong f] →
            [CategoryTheory.ChosenPullbacksAlong g] →
              CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Algebra.Lie.Weights.Cartan
/-- Given a nilpotent Lie subalgebra `H ⊆ L`, the root space of the zero map `0 : H → R` is a Lie
subalgebra of `L`.  -/
LieAlgebra.zeroRootSubalgebra : (R : Type u_1) →
  (L : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] → (H : LieSubalgebra R L) → [LieRing.IsNilpotent ↥H] → LieSubalgebra R L
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.Sup.adjDecidable : (V : Type u_2) → (G H : Digraph V) → [DecidableRel G.Adj] → [DecidableRel H.Adj] → DecidableRel (G ⊔ H).Adj
-- Mathlib.Algebra.Module.Submodule.LinearMap
/-- The natural `R`-linear map from a submodule of an `R`-module `M` to `M`.  -/
SMulMemClass.subtype : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_1} →
            [inst_3 : SetLike A M] →
              [inst_4 : AddSubmonoidClass A M] → [inst_5 : SMulMemClass A R M] → (S' : A) → ↥S' →ₗ[R] M
-- Init.Data.String.Length
Char.length_toString : ∀ (c : Char), c.toString.length = 1
-- Init.Grind.Config
/-- When `true` (default: `true`), uses procedure for handling equalities over commutative rings.
This solver also support commutative semirings, fields, and normalizer non-commutative rings and
semirings.
 -/
Lean.Grind.Config.ring : Lean.Grind.Config → Bool
-- Init.Notation
/-- The less-equal relation: `x ≤ y` 

Conventions for notations in identifiers:

 * The recommended spelling of `≤` in identifiers is `le`. -/
«term_≤_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk_eq_of_leftFractionRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C}
  [inst_1 : W.HasLeftCalculusOfFractions] {X Y : C} (z₁ z₂ : W.LeftFraction X Y),
  CategoryTheory.MorphismProperty.LeftFractionRel z₁ z₂ →
    CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₁ =
      CategoryTheory.MorphismProperty.LeftFraction.Localization.homMk z₂
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.hom_inv_apply : ∀ {M N : SemiNormedGrp₁} (e : M ≅ N) (s : N.carrier),
  ↑(SemiNormedGrp₁.Hom.hom e.hom) (↑(SemiNormedGrp₁.Hom.hom e.inv) s) = s
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.comonFunctorCategoryEquivalence_inverse : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D],
  (CategoryTheory.Monoidal.comonFunctorCategoryEquivalence C D).inverse =
    CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.inverse✝
-- Mathlib.AlgebraicGeometry.Sites.Etale
/-- Big étale site: the étale topology on the category of schemes.  -/
AlgebraicGeometry.Scheme.etaleTopology : CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_injective : ∀ {α : Type u_1}, Function.Injective PMF.toOuterMeasure
-- Mathlib.Analysis.Normed.Module.Bases
/-- The basis constant for Schauder bases (supremum over projections) as `nnnorm`.
Requires completeness to guarantee the supremum is finite,
see lemma `bddAbove_range_nnnorm_proj` below.  -/
SchauderBasis.nnnormProjBound : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} → [inst_1 : NormedAddCommGroup X] → [inst_2 : NormedSpace 𝕜 X] → SchauderBasis 𝕜 X → NNReal
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k : α}, k ∈ Std.ExtTreeMap.unitOfList l cmp ↔ l.contains k = true
-- Mathlib.CategoryTheory.Shift.Basic
/-- compatibility with the associativity  -/
CategoryTheory.ShiftMkCore.assoc_hom_app : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (self : CategoryTheory.ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C),
  CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X)
      ((self.F m₃).map ((self.add m₁ m₂).hom.app X)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X)
        ((self.add m₂ m₃).hom.app ((self.F m₁).obj X)))
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_smul : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {S : Type u_3} [inst_1 : SMulZeroClass S k] (a : S) (b : G →₀ k),
  { coeff := a • b } = a • { coeff := b }
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.algebraMap_im : ∀ {R : Type u_1} {a b : R} (r : R) [inst : CommSemiring R], ((algebraMap R (QuadraticAlgebra R a b)) r).im = 0
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Mul M] (S : ι → Subsemigroup M), (iSup S).op = ⨆ i, (S i).op
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.instFullUliftFunctor : ∀ (R : Type u) [inst : Ring R], (ModuleCat.uliftFunctor.{v', v, u} R).Full
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.WF.below.insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {motive : (a : RBTree.RBNode α) → RBTree.RBNode.WF cmp a → Prop}
  {t : RBTree.RBNode α} {a : α} (a_1 : RBTree.RBNode.WF cmp t),
  RBTree.RBNode.WF.below a_1 → motive t a_1 → RBTree.RBNode.WF.below ⋯
-- Mathlib.Algebra.Polynomial.Bivariate
AdjoinRoot.evalEval_mk : ∀ {R : Type u_1} [inst : CommRing R] {x y : R} {p : Polynomial (Polynomial R)} (h : Polynomial.evalEval x y p = 0)
  (g : Polynomial (Polynomial R)), (AdjoinRoot.evalEval h) ((AdjoinRoot.mk p) g) = Polynomial.evalEval x y g
-- Mathlib.Order.ModularLattice
IsModularLattice.complementedLattice_Icc : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a b : α} [inst_2 : BoundedOrder α] [ComplementedLattice α]
  [inst_4 : Fact (a ≤ b)], ComplementedLattice ↑(Set.Icc a b)
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.restr_toPartialEquiv' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), IsOpen s → (e.restr s).toPartialEquiv = e.restr s
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFunOn.uniformContinuousConstSMul : ∀ (M : Type u_1) (α : Type u_2) (X : Type u_3) [inst : SMul M X] [inst_1 : UniformSpace X]
  [UniformContinuousConstSMul M X] {𝔖 : Set (Set α)}, UniformContinuousConstSMul M (UniformOnFun α X 𝔖)
-- Mathlib.Algebra.Algebra.Hom
AlgHom.toLinearMap_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (p : A), φ.toLinearMap p = φ p
-- Init.Data.Range.Polymorphic.UInt
UInt8.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE UInt8
-- Mathlib.MeasureTheory.Integral.IntegrableOn
/-- A function which is continuous on a set `s` is almost everywhere strongly measurable with
respect to `μ.restrict s` when either the source space or the target space is second-countable.  -/
ContinuousOn.aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [h : SecondCountableTopologyEither α β] [OpensMeasurableSpace α] [TopologicalSpace.PseudoMetrizableSpace β]
  {f : α → β} {s : Set α} {μ : MeasureTheory.Measure α},
  ContinuousOn f s → MeasurableSet s → MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
-- Mathlib.Algebra.Regular.Defs
IsLeftRegular.eq_1 : ∀ {R : Type u_1} [inst : Mul R] (c : R), IsLeftRegular c = Function.Injective fun x => c * x
-- Mathlib.Algebra.BigOperators.Ring.List
List.sum_zipWith_distrib_left : ∀ {ι : Type u_1} {κ : Type u_2} {R : Type u_5} [inst : NonUnitalNonAssocSemiring R] (f : ι → κ → R) (a : R)
  (l₁ : List ι) (l₂ : List κ), (List.zipWith (fun i j => a * f i j) l₁ l₂).sum = a * (List.zipWith f l₁ l₂).sum
-- Mathlib.Tactic.CategoryTheory.Monoidal.Normalize
Mathlib.Tactic.Monoidal.evalWhiskerRight_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {f g : C}
  {η : f ⟶ g}
  {η₁ : f ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj g (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)}
  {η₂ :
    CategoryTheory.MonoidalCategoryStruct.tensorObj f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
      CategoryTheory.MonoidalCategoryStruct.tensorObj g (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)},
  CategoryTheory.CategoryStruct.comp η (CategoryTheory.MonoidalCategoryStruct.rightUnitor g).inv = η₁ →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor f).hom η₁ = η₂ →
      CategoryTheory.MonoidalCategoryStruct.whiskerRight η (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) = η₂
-- Mathlib.CategoryTheory.MorphismProperty.LiftingProperty
CategoryTheory.MorphismProperty.rlp_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (T : CategoryTheory.MorphismProperty C), T.rlp.llp.rlp = T.rlp
-- Init.Data.Option.Lemmas
Option.elim_none : ∀ {β : Sort u_1} {α : Type u_2} (x : β) (f : α → β), none.elim x f = x
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_singleton : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] (a : R),
  f.measure {a} = ENNReal.ofReal (↑f a - Function.leftLim (↑f) a)
-- Mathlib.Order.Defs.PartialOrder
PartialOrder.mk : {α : Type u_2} → [toPreorder : Preorder α] → (∀ (a b : α), a ≤ b → b ≤ a → a = b) → PartialOrder α
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
/-- `℘'(z)² = 4 ℘(z)³ - g₂ ℘(z) - g₃`  -/
PeriodPair.derivWeierstrassP_sq : ∀ (L : PeriodPair),
  ∀ z ∉ L.lattice, L.derivWeierstrassP z ^ 2 = 4 * L.weierstrassP z ^ 3 - L.g₂ * L.weierstrassP z - L.g₃
-- Mathlib.Logic.Function.Basic
Function.extend_comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Injective f → ∀ (g : α → γ) (e' : β → γ), Function.extend f g e' ∘ f = g
-- Mathlib.Algebra.Group.Action.TransferInstance
/-- Transfer `VAddCommClass` across an `Equiv`  -/
Equiv.vaddCommClass : ∀ (M : Type u_1) (N : Type u_2) {α : Type u_4} {β : Type u_5} [inst : VAdd M β] [inst_1 : VAdd N β] (e : α ≃ β)
  [VAddCommClass M N β], VAddCommClass M N α
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.hasFiniteLimits : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasFiniteLimits T],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Arrow T)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.Const.get!ₘ.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (a : α),
  Std.DHashMap.Internal.Raw₀.Const.get!ₘ m a = (Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a).get!
-- Mathlib.Topology.NhdsSet
mem_nhdsSet_empty : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, s ∈ nhdsSet ∅
-- Mathlib.LinearAlgebra.Matrix.Basis
Module.Basis.toLin_toMatrix : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : Module.Basis ι R M) [inst_3 : Finite ι] [inst_4 : Fintype ι'] [inst_5 : DecidableEq ι']
  (v : Module.Basis ι' R M), (Matrix.toLin v e) (e.toMatrix ⇑v) = LinearMap.id
-- Lean.Elab.Term.TermElabM
/-- We can optionally associate an error context with metavariables.
 -/
Lean.Elab.Term.MVarErrorInfo : Type