mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Widget.UserWidget
Lean.Widget.UserWidgetDefinition.mk.sizeOf_spec : ∀ (name javascript : String), sizeOf { name := name, javascript := javascript } = 1 + sizeOf name + sizeOf javascript
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.rightRelDecidable.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) [inst_1 : DecidablePred fun x => x ∈ s] (x y : α),
  QuotientAddGroup.rightRelDecidable s x y = ⋯.mpr (inst_1 (y + -x))
-- Mathlib.Algebra.Algebra.Pi
Pi.algebraMap_def : ∀ (ι : Type u_1) {R : Type u_2} (A : ι → Type u_3) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] (a : R), (algebraMap R ((i : ι) → A i)) a = fun i => (algebraMap R (A i)) a
-- Mathlib.Tactic.NormNum.Basic
/-- The result of multiplying two `norm_num` results.  -/
Mathlib.Meta.NormNum.Result.mul : {u : Lean.Level} →
  {α : Q(Type u)} →
    {a b : Q(«$α»)} →
      Mathlib.Meta.NormNum.Result q(«$a») →
        Mathlib.Meta.NormNum.Result q(«$b») →
          (inst : autoParam Q(Semiring «$α») Mathlib.Meta.NormNum.Result.mul._auto_1) →
            Lean.MetaM (Mathlib.Meta.NormNum.Result q(«$a» * «$b»))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey!_le_maxKey!_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.isEmpty = false → ∀ {k : α} {v : β}, (cmp t.maxKey! (t.insert k v).maxKey!).isLE = true
-- Mathlib.CategoryTheory.Bicategory.Extension
CategoryTheory.Bicategory.LeftExtension.whiskerIdCancel_right : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : a ⟶ b} {g : a ⟶ c}
  (s :
    CategoryTheory.Bicategory.LeftExtension f
      (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c)))
  {t : CategoryTheory.Bicategory.LeftExtension f g} (τ : s ⟶ t.whisker (CategoryTheory.CategoryStruct.id c)),
  (s.whiskerIdCancel τ).right =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.StructuredArrow.Hom.right τ)
      (CategoryTheory.Bicategory.rightUnitor t.extension).hom
-- Mathlib.Topology.Order.Bornology
Bornology.IsBounded.bddBelow : ∀ {α : Type u_1} {s : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  Bornology.IsBounded s → BddBelow s
-- Lean.Meta.Tactic.Induction
_private.Lean.Meta.Tactic.Induction.0.Lean.Meta.getTargetArity : Lean.Expr → ℕ
-- Std.Data.DHashMap.Internal.AssocList.Iterator
_private.Std.Data.DHashMap.Internal.AssocList.Iterator.0.Std.DHashMap.Internal.AssocList.AssocListIterator.finitenessRelation : {α : Type u_1} →
  {β : α → Type u_2} → Std.Iterators.FinitenessRelation (Std.DHashMap.Internal.AssocList.AssocListIterator α β) Id
-- Mathlib.Algebra.Group.Equiv.Defs
/-- An additive isomorphism of additive monoids sends `0` to `0`
(and is hence an additive monoid isomorphism).  -/
AddEquiv.map_zero : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (h : M ≃+ N), h 0 = 0
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mkIso_inv_hom_toLinearMap : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (e : ρ.Equiv σ), (Rep.Hom.hom (Rep.mkIso e).inv).toLinearMap = (↑e.symm).toLinearMap
-- Init.Data.Int.Bitwise.Lemmas
_private.Init.Data.Int.Bitwise.Lemmas.0.Int.shiftRight.match_1.eq_1 : ∀ (motive : ℤ → ℕ → Sort u_1) (n s : ℕ) (h_1 : (n s : ℕ) → motive (Int.ofNat n) s)
  (h_2 : (n s : ℕ) → motive (Int.negSucc n) s),
  (match Int.ofNat n, s with
    | Int.ofNat n, s => h_1 n s
    | Int.negSucc n, s => h_2 n s) =
    h_1 n s
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_12 : HAdd Std.Time.Second.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra : ∀ (R : Type u_1) (L : Type u_3) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [LieAlgebra.IsKilling R L] [Module.Free R L] [Module.Finite R L] [IsDomain R] [IsPrincipalIdealRing R]
  [IsArtinian R L] (H : LieSubalgebra R L) [H.IsCartanSubalgebra], IsLieAbelian ↥H
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonSemanticTokensParams.toJson : Lean.Lsp.SemanticTokensParams → Lean.Json
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If Cᵒᵖ is filtered, then C is cofiltered.  -/
CategoryTheory.isCofiltered_of_isFiltered_op : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFiltered Cᵒᵖ], CategoryTheory.IsCofiltered C
-- Mathlib.CategoryTheory.Triangulated.Triangulated
/-- The second morphism of triangles given an octahedron.  -/
CategoryTheory.Triangulated.Octahedron.triangleMorphism₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} →
                {u₁₂ : X₁ ⟶ X₂} →
                  {u₂₃ : X₂ ⟶ X₃} →
                    {u₁₃ : X₁ ⟶ X₃} →
                      {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} →
                        {v₁₂ : X₂ ⟶ Z₁₂} →
                          {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                            {h₁₂ :
                                CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈
                                  CategoryTheory.Pretriangulated.distinguishedTriangles} →
                              {v₂₃ : X₃ ⟶ Z₂₃} →
                                {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂} →
                                  {h₂₃ :
                                      CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈
                                        CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                    {v₁₃ : X₃ ⟶ Z₁₃} →
                                      {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁} →
                                        {h₁₃ :
                                            CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈
                                              CategoryTheory.Pretriangulated.distinguishedTriangles} →
                                          CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃ →
                                            (CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ⟶
                                              CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_updateCol_add_self : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R)
  {i j : n}, i ≠ j → (A.updateCol i fun k => A k i + A k j).det = A.det
-- Mathlib.CategoryTheory.Monoidal.Center
CategoryTheory.HalfBraiding.monoidal_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (self : CategoryTheory.HalfBraiding X) (U U' : C) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj U U') X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.β U).hom U')
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (self.β U').hom)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv h))))
-- Mathlib.ModelTheory.Arithmetic.Presburger.Definability
/-- The graph of multiplication is not Presburger definable in `ℕ`.  -/
FirstOrder.Language.presburger.mul_not_definable : ∀ {A : Set ℕ}, ¬A.Definable FirstOrder.Language.presburger {v | v 0 = v 1 * v 2}
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C] (Ω₀ Ω : C) (truth : Ω₀ ⟶ Ω)
  (mono_truth : autoParam (CategoryTheory.Mono truth) CategoryTheory.Subobject.Classifier.mono_truth._autoParam)
  (χ₀ : (U : C) → U ⟶ Ω₀) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω)
  (isPullback :
    ∀ {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (χ₀ U) (χ m) truth)
  (uniq :
    ∀ {U X : C} (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m] {χ₀' : U ⟶ Ω₀} {χ' : X ⟶ Ω},
      CategoryTheory.IsPullback m χ₀' χ' truth → χ' = χ m),
  sizeOf
      { Ω₀ := Ω₀, Ω := Ω, truth := truth, mono_truth := mono_truth, χ₀ := χ₀, χ := χ, isPullback := isPullback,
        uniq := uniq } =
    1 + sizeOf Ω₀ + sizeOf Ω + sizeOf truth + sizeOf mono_truth
-- Mathlib.Order.Category.Preord
_private.Mathlib.Order.Category.Preord.0.Preord.Hom.mk : {X Y : Preord} → (↑X →o ↑Y) → X.Hom Y
-- Mathlib.Algebra.Group.Ext
RightCancelMonoid.ext_iff : ∀ {M : Type u} {m₁ m₂ : RightCancelMonoid M}, m₁ = m₂ ↔ HMul.hMul = HMul.hMul
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- Two functions are independent if the two measurable space structures they generate are
independent. For a function `f` with codomain having measurable space structure `m`, the generated
measurable space structure is `MeasurableSpace.comap f m`.  -/
ProbabilityTheory.Kernel.IndepFun : {α : Type u_1} →
  {Ω : Type u_2} →
    {β : Type u_4} →
      {γ : Type u_6} →
        {mα : MeasurableSpace α} →
          {mΩ : MeasurableSpace Ω} →
            [mβ : MeasurableSpace β] →
              [mγ : MeasurableSpace γ] →
                (Ω → β) →
                  (Ω → γ) →
                    ProbabilityTheory.Kernel α Ω →
                      autoParam (MeasureTheory.Measure α) ProbabilityTheory.Kernel.IndepFun._auto_1 → Prop
-- Mathlib.Tactic.TacticAnalysis.Declarations
_private.Mathlib.Tactic.TacticAnalysis.Declarations.0.Mathlib.TacticAnalysis.TerminalReplacementOutcome.success.inj : ∀ {stx stx_1 : Lean.TSyntax `tactic},
  Mathlib.TacticAnalysis.TerminalReplacementOutcome.success✝ stx =
      Mathlib.TacticAnalysis.TerminalReplacementOutcome.success✝ stx_1 →
    stx = stx_1
-- Mathlib.Algebra.GCDMonoid.Basic
/-- **Alias** of `dvd_lcm_of_dvd_right`. -/
Dvd.dvd.lcm_left : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ lcm c b
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- Vertical composition of strong natural transformations.  -/
CategoryTheory.Oplax.StrongTrans.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.OplaxFunctor B C} →
          CategoryTheory.Oplax.StrongTrans F G →
            CategoryTheory.Oplax.StrongTrans G H → CategoryTheory.Oplax.StrongTrans F H
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_comap_le : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {S : AddSubmonoid N} {f : F},
  AddSubmonoid.map f (AddSubmonoid.comap f S) ≤ S
-- Std.Data.ExtDTreeMap.Lemmas
/-- Simpler variant of `get!_filterMap` when `LawfulEqCmp` is available.  -/
Std.ExtDTreeMap.Const.get!_filterMap' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] [inst_2 : Inhabited γ] {f : α → β → Option γ} {k : α},
  Std.ExtDTreeMap.Const.get! (Std.ExtDTreeMap.filterMap f t) k = ((Std.ExtDTreeMap.Const.get? t k).bind (f k)).get!
-- Mathlib.Algebra.GroupWithZero.Defs
noZeroDivisors_iff : ∀ (M₀ : Type u_2) [inst : Mul M₀] [inst_1 : Zero M₀], NoZeroDivisors M₀ ↔ ∀ {a b : M₀}, a * b = 0 → a = 0 ∨ b = 0
-- Mathlib.RingTheory.Valuation.Extension
/-- When `K` is a field, if the preimage of the valuation integers of `A` equals to the valuation
integers of `K`, then the valuation on `A` is an extension of the valuation on `K`.
 -/
Valuation.HasExtension.ofComapInteger : ∀ {A : Type u_2} [inst : Ring A] {K : Type u_5} [inst_1 : Field K] [inst_2 : Algebra K A] {ΓA : Type u_7}
  {ΓK : Type u_8} [inst_3 : LinearOrderedCommGroupWithZero ΓK] [inst_4 : LinearOrderedCommGroupWithZero ΓA]
  {vK : Valuation K ΓK} {vA : Valuation A ΓA},
  Subring.comap (algebraMap K A) vA.integer = vK.integer → vK.HasExtension vA
-- Mathlib.Order.RelSeries
LTSeries.mk_toFun : ∀ {α : Type u_1} [inst : Preorder α] (length : ℕ) (toFun : Fin (length + 1) → α) (strictMono : StrictMono toFun)
  (a : Fin (length + 1)), (LTSeries.mk length toFun strictMono).toFun a = toFun a
-- Lean.Elab.PreDefinition.TerminationMeasure
_private.Lean.Elab.PreDefinition.TerminationMeasure.0.Array.map_unattach.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : Subtype P → Sort u_2) (x : α) (h : P x)
  (h_1 : (x : α) → (h : P x) → motive ⟨x, h⟩),
  (match ⟨x, h⟩ with
    | ⟨x, h⟩ => h_1 x h) =
    h_1 x h
-- Mathlib.Data.Int.Bitwise
/-- Compare with `Int.shiftRight_add`, which doesn't have the coercions `ℕ → ℤ`.  -/
Int.shiftRight_add' : ∀ (m : ℤ) (n k : ℕ), m >>> (↑n + ↑k) = m >>> ↑n >>> ↑k
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.empty_equiv_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp},
  Std.DTreeMap.empty.Equiv t ↔ t.isEmpty = true
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.mem_coeffs_iff : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {c : R},
  c ∈ p.coeffs ↔ ∃ n ∈ p.support, c = MvPolynomial.coeff n p
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.Z : Std.Time.GenericFormat.DateBuilder✝ → Option Std.Time.TimeZone.Offset
-- Mathlib.Analysis.Calculus.VectorField
/-- The Lie bracket of vector fields in vector spaces satisfies the Leibniz identity
`[U, [V, W]] = [[U, V], W] + [V, [U, W]]`.  -/
VectorField.leibniz_identity_lieBracketWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E],
  minSmoothness 𝕜 2 ≤ n →
    ∀ {U V W : E → E} {s : Set E} {x : E},
      UniqueDiffOn 𝕜 s →
        x ∈ closure (interior s) →
          x ∈ s →
            ContDiffWithinAt 𝕜 n U s x →
              ContDiffWithinAt 𝕜 n V s x →
                ContDiffWithinAt 𝕜 n W s x →
                  VectorField.lieBracketWithin 𝕜 U (VectorField.lieBracketWithin 𝕜 V W s) s x =
                    VectorField.lieBracketWithin 𝕜 (VectorField.lieBracketWithin 𝕜 U V s) W s x +
                      VectorField.lieBracketWithin 𝕜 V (VectorField.lieBracketWithin 𝕜 U W s) s x
-- Mathlib.AlgebraicGeometry.LimitsOver
AlgebraicGeometry.instCreatesColimitOverSchemeTopMorphismPropertyOverForget : (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme) →
  [AlgebraicGeometry.IsZariskiLocalAtSource P] →
    {S : AlgebraicGeometry.Scheme} →
      {J : Type u_1} →
        [inst : CategoryTheory.Category.{v_1, u_1} J] →
          (F : CategoryTheory.Functor J (P.Over ⊤ S)) →
            [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f).left] →
              [(F.comp
                      ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp
                        ((CategoryTheory.Over.forget S).comp AlgebraicGeometry.Scheme.forget))).IsLocallyDirected] →
                [Quiver.IsThin J] →
                  [Small.{u, u_1} J] →
                    CategoryTheory.CreatesColimit F (CategoryTheory.MorphismProperty.Over.forget P ⊤ S)
-- Mathlib.Analysis.Convex.Quasiconvex
QuasiconcaveOn.monotone_comp : ∀ {𝕜 : Type u_4} {E : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {β : Type u_6} {γ : Type u_7} [inst_4 : LinearOrder β] [inst_5 : Preorder γ] {s : Set E}
  {f : E → β} {g : β → γ}, Monotone g → QuasiconcaveOn 𝕜 s f → QuasiconcaveOn 𝕜 s (g ∘ f)
-- Init.Classical
Classical.or_iff_not_imp_right : ∀ {a b : Prop}, a ∨ b ↔ ¬b → a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : Inhabited α] [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).getKey! k = m₂.getKey! k
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwInfo.mk.sizeOf_spec : ∀ (rootExpr subExpr : Lean.Expr) (rflTarget? : Option Lean.Expr) (pos : Lean.SubExpr.Pos)
  (rwKind : Mathlib.Tactic.ClickSuggestions.RwKind),
  sizeOf { rootExpr := rootExpr, subExpr := subExpr, rflTarget? := rflTarget?, pos := pos, rwKind := rwKind } =
    1 + sizeOf rootExpr + sizeOf subExpr + sizeOf rflTarget? + sizeOf pos + sizeOf rwKind
-- Mathlib.RingTheory.Localization.Integral
isAlgebraic_of_isFractionRing : ∀ (R : Type u_5) (S : Type u_6) (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Field K] [inst_3 : CommRing L] [inst_4 : Algebra R S] [inst_5 : Algebra R K] [inst_6 : Algebra R L]
  [inst_7 : Algebra S L] [inst_8 : Algebra K L] [IsScalarTower R S L] [IsScalarTower R K L] [IsFractionRing S L]
  [Algebra.IsIntegral R S], Algebra.IsAlgebraic K L
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.whiskerLeft_curry_ihom_ev_app_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A X : C) {Y : C}
  [inst_2 : CategoryTheory.Closed A] (g : CategoryTheory.MonoidalCategoryStruct.tensorObj A Y ⟶ X) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A (CategoryTheory.MonoidalClosed.curry g))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ihom.ev A).app X) h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Algebra.Group.Nat.Hom
/-- If `M` is commutative, `powersHom` is a multiplicative equivalence.  -/
powersMulHom : (M : Type u_1) → [inst : CommMonoid M] → M ≃* (Multiplicative ℕ →* M)
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.processConstructor : Lean.Meta.Match.Problem → Lean.MetaM (Array Lean.Meta.Match.Problem)
-- Mathlib.NumberTheory.Pell
/-- Two solutions are equal if their `x` and `y` components are equal.  -/
Pell.Solution₁.ext : ∀ {d : ℤ} {a b : Pell.Solution₁ d}, a.x = b.x → a.y = b.y → a = b
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.dp_sum : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] (s : Finset ι) (q : ℕ) (x : ι → M),
  DividedPowerAlgebra.dp R q (s.sum x) = ∑ k ∈ s.sym q, ∏ i ∈ s, DividedPowerAlgebra.dp R (Multiset.count i ↑k) (x i)
-- Mathlib.RingTheory.LocalRing.Module
Module.IsLocalRing.linearCombination_bijective_of_flat : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsLocalRing R] [Module.Finite R M] [Module.Flat R M] {ι : Type u} (v : ι → M),
  Function.Bijective
      ⇑(Finsupp.linearCombination (IsLocalRing.ResidueField R)
          (⇑((TensorProduct.mk R (IsLocalRing.ResidueField R) M) 1) ∘ v)) →
    Function.Bijective ⇑(Finsupp.linearCombination R v)
-- Mathlib.Data.Complex.Basic
Complex.re_zsmul : ∀ (n : ℤ) (z : ℂ), (n • z).re = n • z.re
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_i : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_i._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.cyclesIso_inv_i._auto_3),
  CategoryTheory.CategoryStruct.comp (X.cyclesIso f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).inv
      (X.shortComplex f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂).iCycles =
    X.iCycles f₁ f₂ n₁
-- Mathlib.Algebra.Ring.Subsemiring.Order
/-- The set of nonnegative elements in an ordered semiring, as a subsemiring.  -/
Subsemiring.nonneg : (R : Type u_1) → [inst : Semiring R] → [inst_1 : PartialOrder R] → [IsOrderedRing R] → Subsemiring R
-- Mathlib.Topology.Algebra.ConstMulAction
/-- The quotient map by a group action is open, i.e. the quotient by a group action is an open
quotient.  -/
isOpenMap_quotient_mk'_mul : ∀ {Γ : Type u_4} [inst : Group Γ] {T : Type u_5} [inst_1 : TopologicalSpace T] [inst_2 : MulAction Γ T]
  [ContinuousConstSMul Γ T], IsOpenMap Quotient.mk'
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantTo.isoMap_hom_inv_id_assoc : ∀ {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] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantTo i₀) {i j : J} (φ : i ⟶ j) (hφ : Nonempty (j ⟶ i₀)) {Z : C} (h_1 : F.obj i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map φ) (CategoryTheory.CategoryStruct.comp (h.isoMap φ hφ).inv h_1) = h_1
-- Mathlib.Data.Complex.Basic
Complex.re_qsmul : ∀ (q : ℚ) (z : ℂ), (q • z).re = q • z.re
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- An extension is purely inseparable if and only if it has finite separable degree one.  -/
isPurelyInseparable_iff_finSepDegree_eq_one : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsPurelyInseparable F E ↔ Field.finSepDegree F E = 1
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.smul_def : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (l : FreeMonoid α) (b : β), l • b = List.foldr f b (FreeMonoid.toList l)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.map_fst_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {W X Y Z : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct W X]
  [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct Y Z] (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Tactic.SplitIfs
/-- `Simp.Discharge` strategy to use in `reduceIfsAt`. Delegates to
`SplitIf.discharge?`, and additionally supports discharging `True`, to
better match the behavior of mathlib3's `split_ifs`.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.discharge? : Lean.Expr → Lean.Meta.SimpM (Option Lean.Expr)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
hasSumLocallyUniformly_of_forall_compact : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β] [LocallyCompactSpace β],
  (∀ (K : Set β), IsCompact K → HasSumUniformlyOn f g K) → HasSumLocallyUniformly f g
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.map_iSup : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] {ι : Sort u_1} (f : R →+* S)
  (s : ι → Subring R), Subring.map f (iSup s) = ⨆ i, Subring.map f (s i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.isUnit_addU_of_Y_ne : ∀ {F : Type u} [inst : Field F] {P Q : Fin 3 → F},
  P 2 ≠ 0 → Q 2 ≠ 0 → P 1 * Q 2 ≠ Q 1 * P 2 → IsUnit (WeierstrassCurve.Projective.addU P Q)
-- Mathlib.GroupTheory.Generators
Group.Generators.ofSet_val : ∀ {G : Type u_1} [inst : Group G] {S : Set G} (hS : Subgroup.closure S = ⊤),
  (Group.Generators.ofSet hS).val = Subtype.val