mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.monomial_modMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (s : σ →₀ ℕ), ((MvPolynomial.monomial s) 1).modMonomial s = 0
-- Mathlib.Algebra.Category.FGModuleCat.Limits
FGModuleCat.instHasLimitsOfShapeOfFinCategory : ∀ {k : Type u} [inst : Ring k] [IsNoetherianRing k] (J : Type) [inst_2 : CategoryTheory.SmallCategory J]
  [CategoryTheory.FinCategory J], CategoryTheory.Limits.HasLimitsOfShape J (FGModuleCat k)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.linearIndepOn_periods : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s), LinearIndepOn ℕ id (IsProperLinearSet.periods✝ hs)
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
/-- The reverse image of a measurable space under a function. `comap f m` contains the sets
`s : Set α` such that `s` is the `f`-preimage of a measurable set in `β`.  -/
MeasurableSpace.comap : {α : Type u_1} → {β : Type u_2} → (α → β) → MeasurableSpace β → MeasurableSpace α
-- Mathlib.Algebra.Homology.Embedding.StupidTrunc
HomologicalComplex.stupidTruncXIso.eq_1 : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c') (e : c.Embedding c')
  [inst_3 : e.IsRelIff] {i : ι} {i' : ι'} (hi' : e.f i = i'),
  K.stupidTruncXIso e hi' = (K.restriction e).extendXIso e hi' ≪≫ CategoryTheory.eqToIso ⋯
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.curry_vadd_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_4} {Z : Type u_5} [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {R : Type u_6} [inst_3 : VAdd R Z] [inst_4 : ContinuousConstVAdd R Z] (f : C(X × Y, Z))
  (r : R) (x : X), (r +ᵥ f).curry x = r +ᵥ f.curry x
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.iterateEquiv_symm_apply : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  (x : HahnSeries (Lex (Γ × Γ')) R), HahnSeries.iterateEquiv.symm x = x.toIterate
-- Mathlib.Logic.Function.Basic
/-- The inverse of a surjective function. (Unlike `invFun`, this does not require
`α` to be inhabited.)  -/
Function.surjInv : {α : Sort u} → {β : Sort v} → {f : α → β} → Function.Surjective f → β → α
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_inj : ∀ {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]
  {f g : A →A[R] B}, ↑f = ↑g ↔ f = g
-- Mathlib.Topology.Coherent
Topology.IsCoherentWith.continuous_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)} {Y : Type u_2} [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsCoherentWith S → (Continuous f ↔ ∀ s ∈ S, ContinuousOn f s)
-- Init.Data.SInt.Basic
/-- Converts an arbitrary-precision integer to a 16-bit signed integer, wrapping on overflow or underflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int16.ofInt 48 = 48`
* `Int16.ofInt (-129) = -129`
* `Int16.ofInt (128) = 128`
* `Int16.ofInt 70000 = 4464`
* `Int16.ofInt (-40000) = 25536`
 -/
Int16.ofInt : ℤ → Int16
-- Init.Data.Fin.Lemmas
Fin.lt_or_eq_of_le : ∀ {n : ℕ} {a b : Fin n}, a ≤ b → a < b ∨ a = b
-- Mathlib.CategoryTheory.Limits.Indization.Equalizers
/-- If `C` has equalizers. then ind-objects are closed under equalizers.

This is Proposition 6.1.17(i) in [Kashiwara2006].
 -/
CategoryTheory.Limits.isClosedUnderLimitsOfShape_isIndObject_walkingParallelPair : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasEqualizers C],
  CategoryTheory.ObjectProperty.IsClosedUnderLimitsOfShape CategoryTheory.Limits.IsIndObject
    CategoryTheory.Limits.WalkingParallelPair
-- Lean.Message
Lean.instBEqTraceResult : BEq Lean.TraceResult
-- Mathlib.Data.Part
_private.Mathlib.Data.Part.0.Part.ofOption.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((a : α) → motive (some a)) → motive x
-- Mathlib.Order.Bounds.Basic
isGLB_congr_of_antisymmRel : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} {a b : α},
  AntisymmRel (fun x1 x2 => x1 ≤ x2) a b → (IsGLB s a ↔ IsGLB s b)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is negative, the first vector is nonzero.  -/
Orientation.left_ne_zero_of_oangle_sign_eq_neg_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign = -1 → x ≠ 0
-- Mathlib.Algebra.Order.Quantale
AddQuantale.mk.sizeOf_spec : ∀ {α : Type u_1} [inst : AddSemigroup α] [inst_1 : CompleteLattice α] [inst_2 : IsAddQuantale α] [inst_3 : SizeOf α],
  sizeOf { } = 1
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.toList_getElem_zero : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x : α) (h : x ∈ p.support),
  (p.toList x)[0] = x
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- `CliffordAlgebra.involute` is analogous to `Complex.conj`.  -/
CliffordAlgebraComplex.toComplex_involute : ∀ (c : CliffordAlgebra CliffordAlgebraComplex.Q),
  CliffordAlgebraComplex.toComplex (CliffordAlgebra.involute c) = (starRingEnd ℂ) (CliffordAlgebraComplex.toComplex c)
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRoi.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : Std.Roi α) → Decidable (x = x_1)
-- Mathlib.Algebra.GradedMulAction
GradedMonoid.GMulAction.mk : {ιA : Type u_1} →
  {ιM : Type u_3} →
    {A : ιA → Type u_4} →
      {M : ιM → Type u_5} →
        [inst : AddMonoid ιA] →
          [inst_1 : VAdd ιA ιM] →
            [inst_2 : GradedMonoid.GMonoid A] →
              [toGSMul : GradedMonoid.GSMul A M] →
                (∀ (b : GradedMonoid M), 1 • b = b) →
                  (∀ (a a' : GradedMonoid A) (b : GradedMonoid M), (a * a') • b = a • a' • b) →
                    GradedMonoid.GMulAction A M
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.underscore : Lean.Meta.Match.Example
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.zsmul_modEq_zsmul : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} {z : ℤ} [IsAddTorsionFree G],
  z ≠ 0 → (z • a ≡ z • b [PMOD z • p] ↔ a ≡ b [PMOD p])
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
disjoint_closedBall_closedBall_iff : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {x y : E} {δ ε : ℝ},
  0 ≤ δ → 0 ≤ ε → (Disjoint (Metric.closedBall x δ) (Metric.closedBall y ε) ↔ δ + ε < dist x y)
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.rightCancelSemigroup : {α : Type u} → [AddRightCancelSemigroup α] → RightCancelSemigroup (Multiplicative α)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.skipSuffix?_slice_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → s.skipSuffix? pat = some s.endPos
-- Mathlib.Data.Fin.Fin2
/-- Converts a `Fin2` into a natural.  -/
Fin2.toNat : {n : ℕ} → Fin2 n → ℕ
-- Mathlib.CategoryTheory.Limits.Cones
/-- Whisker a cocone by precomposition of a functor. See `whiskering` for a functorial
version.
 -/
CategoryTheory.Limits.Cocone.whisker : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {K : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} K] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor J C} →
              (E : CategoryTheory.Functor K J) →
                CategoryTheory.Limits.Cocone F → CategoryTheory.Limits.Cocone (E.comp F)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- **Alias** of `MeasurableEquiv.setOfPred_apply`. -/
MeasurableEquiv.setOf_apply : ∀ {α : Type u_8} (p : α → Prop), MeasurableEquiv.setOfPred p = {a | p a}
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.coe_fn_coe' : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {R : Type u_10} [inst_2 : Semiring R]
  [inst_3 : MulSemiringAction M R] {S : Type u_12} [inst_4 : Semiring S] [inst_5 : MulSemiringAction N S]
  (f : R →ₑ+*[φ] S), ⇑↑f = ⇑f
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The second index  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₂ : {ι : Type u_2} →
  {κ : Type u_3} →
    [inst : Preorder ι] →
      {c : ℤ → ComplexShape κ} →
        {r₀ : ℤ} → CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ → κ → ι
-- Mathlib.CategoryTheory.Shift.SingleFunctorsLift
/-- Let `C`, `D` and `E` be categories. Let `A` be an additive monoid.
Assume that `D` and `E` have shifts by `A` and that we have
a fully faithful functor `G : D ⥤ A` which commutes with shifts.
Given `F : SingleFunctors C E A`, and a family of functors
`Φ a : C ⥤ D` with isomorphisms `Φ a ⋙ G ≅ F.functor a` for all `a : A`,
this is a term in `SingleFunctors C D A` which is given by the functors `Φ a`
for all `a`.  -/
CategoryTheory.SingleFunctors.lift : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{u_5, u_1} C] →
        [inst_1 : CategoryTheory.Category.{u_6, u_2} D] →
          [inst_2 : CategoryTheory.Category.{u_7, u_3} E] →
            {A : Type u_4} →
              [inst_3 : AddMonoid A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  [inst_5 : CategoryTheory.HasShift E A] →
                    (F : CategoryTheory.SingleFunctors C E A) →
                      (G : CategoryTheory.Functor D E) →
                        [G.CommShift A] →
                          [G.Full] →
                            [G.Faithful] →
                              (Φ : A → CategoryTheory.Functor C D) →
                                ((a : A) → (Φ a).comp G ≅ F.functor a) → CategoryTheory.SingleFunctors C D A
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Trie.node.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (values : Array α) (star : Lean.Meta.LazyDiscrTree.TrieIndex)
  (children : Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex)
  (pending : Array (Lean.Meta.LazyDiscrTree.LazyEntry α)),
  sizeOf { values := values, star := star, children := children, pending := pending } =
    1 + sizeOf values + sizeOf star + sizeOf children + sizeOf pending
-- Init.Data.Array.Lemmas
Array.size_rightpad : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs : Array α}, (Array.rightpad n a xs).size = max n xs.size
-- Lean.DocString.Parser
Lean.Doc.Parser.instReprOrderedListType.repr : Lean.Doc.Parser.OrderedListType → ℕ → Std.Format
-- Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus
CategoryTheory.Functor.instIsRightDerivedFunctorPlusPlusRightDerivedFunctorPlusRightDerivedFunctorPlusUnitQuasiIso : ∀ {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] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] [inst_4 : HasDerivedCategory C] [inst_5 : HasDerivedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Additive] [inst_7 : CategoryTheory.EnoughInjectives C],
  F.rightDerivedFunctorPlus.IsRightDerivedFunctor F.rightDerivedFunctorPlusUnit (HomotopyCategory.Plus.quasiIso C)
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_right_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).hom.toNatTrans.app X)
      ((F.mapComp g h).hom.toNatTrans.app ((F.map f).toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).hom.toNatTrans.app X)
        ((F.map h).toFunctor.map ((F.mapComp f g).hom.toNatTrans.app X)))
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instPartialOrder : {α : Type u_1} → [inst : LE α] → PartialOrder (UpperSet α)
-- Mathlib.Topology.Order.MonotoneConvergence
Pi.infConvergenceClass' : ∀ {α : Type u_1} {ι : Type u_3} [inst : Preorder α] [inst_1 : TopologicalSpace α] [InfConvergenceClass α],
  InfConvergenceClass (ι → α)
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
/-- The `Assignment` inductive datatype is used in the `assignments` field of default formulas (defined in
Formula.Implementation.lean) to store and quickly access information about whether unit literals are
contained in (or entailed by) a formula.

The elements of `Assignment` can be viewed as a lattice where `both` is top, satisfying both `hasPosAssignment`
and `hasNegAssignment`, `pos` satisfies only the former, `neg` satisfies only the latter, and `unassigned` is
bottom, satisfying neither. If one wanted to modify the default formula structure to use a BitArray rather than
an `Assignment Array` for the `assignments` field, a reasonable 2-bit representation of the `Assignment` type
would be:
- both: 11
- pos: 10
- neg: 01
- unassigned: 00

Then `hasPosAssignment` could simply query the first bit and `hasNegAssignment` could simply query the second bit.
 -/
Std.Tactic.BVDecide.LRAT.Internal.Assignment : Type
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.productIso_hom_comp_eval_apply : ∀ {J : Type v} (F : J → Type (max v u)) (j : J) (x : ∏ᶜ F),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.productIso F).hom) x j =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π F j)) x
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- The special case of the pairing integral in a set where the pairing is just the scalar
multiplication by `ℝ` on `F` and `f` is real-valued. The resulting integral is `F`-valued. -/
MeasureTheory.VectorMeasure.«term∫ᵛ_In_,_∂•_» : Lean.ParserDescr
-- Mathlib.Data.ENat.Lattice
ENat.biSup_add : ∀ {a : ℕ∞} {ι : Type u_4} {s : Set ι}, s.Nonempty → ∀ (f : ι → ℕ∞), (⨆ i ∈ s, f i) + a = ⨆ i ∈ s, f i + a
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.binaryBiproductData_bicone_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C) (hT : T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₀ : T.mor₃ = 0) (inr : T.obj₃ ⟶ T.obj₂)
  (inr_snd : CategoryTheory.CategoryStruct.comp inr T.mor₂ = CategoryTheory.CategoryStruct.id T.obj₃)
  (fst : T.obj₂ ⟶ T.obj₁)
  (total :
    CategoryTheory.CategoryStruct.comp fst T.mor₁ + CategoryTheory.CategoryStruct.comp T.mor₂ inr =
      CategoryTheory.CategoryStruct.id T.obj₂),
  (CategoryTheory.Pretriangulated.binaryBiproductData T hT hT₀ inr inr_snd fst total).bicone.snd = T.mor₂
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
RingEquiv.sofLeftInverse'_apply : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] {g : S → R} {f : F} (h : Function.LeftInverse g ⇑f)
  (x : R), ↑((RingEquiv.sofLeftInverse' h) x) = f x
-- Mathlib.Data.Num.Bitwise
/-- Bitwise `fun a b ↦ a && !b` for `Num`. For example, `ldiff 5 9 = 4`:
```
 101
1001
----
 100
```
 -/
Num.ldiff : Num → Num → Num
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.getEntryGE?_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ → ∀ {k : α}, Std.DTreeMap.Internal.Impl.getEntryGE? k t₁ = Std.DTreeMap.Internal.Impl.getEntryGE? k t₂
-- Init.Tactics
/-- Configuration options for tactics.  -/
Lean.Parser.Tactic.optConfig : Lean.ParserDescr
-- Mathlib.Topology.Semicontinuity.Defs
SemicontinuousAt.semicontinuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop} {x : α} (s : Set α),
  SemicontinuousAt r x → SemicontinuousWithinAt r s x
-- Mathlib.Data.Set.Restrict
/-- If `g` factors through `f` and `g` is injective, then `extend f g j` is injective on the
range of `f`.  -/
Function.FactorsThrough.extend_injOn : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : α → γ} {j : β → γ},
  Function.FactorsThrough g f → Function.Injective g → Set.InjOn (Function.extend f g j) (Set.range f)
-- Mathlib.Geometry.Manifold.Notation
Manifold.Elab.NormedSpaceInfo.mk.injEq : ∀ (normedSpace baseField normedSpace_1 baseField_1 : Lean.Expr),
  ({ normedSpace := normedSpace, baseField := baseField } =
      { normedSpace := normedSpace_1, baseField := baseField_1 }) =
    (normedSpace = normedSpace_1 ∧ baseField = baseField_1)
-- Std.Http.Protocol.H1.Event
Std.Http.Protocol.H1.instReprEvent.repr : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Event dir → ℕ → Std.Format
-- Mathlib.RingTheory.Valuation.ValuationRing
ValuationRing.instIsBezout : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [ValuationRing R], IsBezout R
-- Mathlib.Data.List.Sort
List.SortedGT.nodup : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedGT → l.Nodup
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose.inj : ∀ {k₁ : ℤ} {m₁ : Lean.Grind.CommRing.Mon} {c₁ : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k₂ : ℤ}
  {m₂ : Lean.Grind.CommRing.Mon} {c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k₁_1 : ℤ}
  {m₁_1 : Lean.Grind.CommRing.Mon} {c₁_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr} {k₂_1 : ℤ}
  {m₂_1 : Lean.Grind.CommRing.Mon} {c₂_1 : Lean.Meta.Grind.Arith.CommRing.EqCnstr},
  Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose k₁ m₁ c₁ k₂ m₂ c₂ =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.superpose k₁_1 m₁_1 c₁_1 k₂_1 m₂_1 c₂_1 →
    k₁ = k₁_1 ∧ m₁ = m₁_1 ∧ c₁ = c₁_1 ∧ k₂ = k₂_1 ∧ m₂ = m₂_1 ∧ c₂ = c₂_1
-- Mathlib.Algebra.Module.PUnit
PUnit.instVAdd_mathlib.eq_1 : ∀ {R : Type u_1}, PUnit.instVAdd_mathlib = { vadd := fun x x_1 => x_1 }
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {x : ↥X} (hxU : x ∈ U),
  hU.fromSpecStalk hxU = X.fromSpecStalk x
-- Mathlib.Data.Multiset.NatAntidiagonal
/-- The antidiagonal of `0` is the list `[(0, 0)]`  -/
Multiset.Nat.antidiagonal_zero : Multiset.Nat.antidiagonal 0 = {(0, 0)}
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalRingHom.mem_srange_self : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S] {F : Type u_1}
  [inst_2 : FunLike F R S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (x : R), f x ∈ NonUnitalRingHom.srange f
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.coe_mk' : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 → P2) (f' : V1 →ₗ[k] V2) (p : P1)
  (h : ∀ (p' : P1), f p' = f' (p' -ᵥ p) +ᵥ f p), ⇑(AffineMap.mk' f f' p h) = f
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.AddAndFinalizeContext.mk.sizeOf_spec : ∀ (views : Array Lean.Elab.Command.InductiveView) (elabs' : Array Lean.Elab.Command.InductiveElabStep2)
  (indFVars vars : Array Lean.Expr) (levelParams : List Lean.Name) (numVars numParams : ℕ)
  (indTypes : List Lean.InductiveType) (isUnsafe : Bool) (rs : Array Lean.Elab.Command.ElabHeaderResult)
  (params : Array Lean.Expr) (isCoinductive : Bool),
  sizeOf
      { views := views, elabs' := elabs', indFVars := indFVars, vars := vars, levelParams := levelParams,
        numVars := numVars, numParams := numParams, indTypes := indTypes, isUnsafe := isUnsafe, rs := rs,
        params := params, isCoinductive := isCoinductive } =
    1 + sizeOf views + sizeOf elabs' + sizeOf indFVars + sizeOf vars + sizeOf levelParams + sizeOf numVars +
                sizeOf numParams +
              sizeOf indTypes +
            sizeOf isUnsafe +
          sizeOf rs +
        sizeOf params +
      sizeOf isCoinductive
-- Mathlib.Topology.Algebra.Group.Extension
TopologicalGroup.IsSES.mk : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : Group A] [inst_1 : Group B] [inst_2 : Group C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] {φ : A →* B} {ψ : B →* C},
  Topology.IsClosedEmbedding ⇑φ → IsOpenQuotientMap ⇑ψ → Function.MulExact ⇑φ ⇑ψ → TopologicalGroup.IsSES φ ψ
-- Mathlib.GroupTheory.GroupAction.Basic
Additive.mulAction_orbit : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] (b : β), AddAction.orbit (Additive α) b = MulAction.orbit α b
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Internal.ofToSliceWithProof.match_1.splitter : {s : String} →
  (motive : { p // p ≠ s.toSlice.endPos } → Sort u_1) →
    (x : { p // p ≠ s.toSlice.endPos }) → ((p : s.toSlice.Pos) → (h : p ≠ s.toSlice.endPos) → motive ⟨p, h⟩) → motive x
-- Mathlib.Data.Finmap
/-- An equivalence between `Finmap β` and pairs `(keys : Finset α, lookup : ∀ a, Option (β a))` such
that `(lookup a).isSome ↔ a ∈ keys`.  -/
Finmap.keysLookupEquiv : {α : Type u} → {β : α → Type v} → [DecidableEq α] → Finmap β ≃ { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 }
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toArray_eq_empty_iff : ∀ {α : Type u} {r : Std.Rii α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.PRange.LawfulUpwardEnumerableLeast? α] [inst : Std.Rxi.IsAlwaysFinite α],
  r.toArray = #[] ↔ ¬Nonempty α
-- Mathlib.Combinatorics.Additive.CauchyDavenport
_private.Mathlib.Combinatorics.Additive.CauchyDavenport.0.devosAddRel_iff : ∀ {α : Type u_2} [inst : AddGroup α] [inst_1 : DecidableEq α] {x y : Finset α × Finset α},
  DevosAddRel✝ x y ↔
    (x.1 + x.2).card < (y.1 + y.2).card ∨
      (x.1 + x.2).card = (y.1 + y.2).card ∧ y.1.card + y.2.card < x.1.card + x.2.card ∨
        (x.1 + x.2).card = (y.1 + y.2).card ∧ x.1.card + x.2.card = y.1.card + y.2.card ∧ x.1.card < y.1.card
-- Mathlib.Tactic.Simps.NotationClass
Simps.AutomaticProjectionData.mk.sizeOf_spec : ∀ (className : Lean.Name) (isNotation : Bool) (findArgs : Lean.Name),
  sizeOf { className := className, isNotation := isNotation, findArgs := findArgs } =
    1 + sizeOf className + sizeOf isNotation + sizeOf findArgs
-- Mathlib.Topology.Closure
/-- **Alias** of `sdiff_subset_closure_iff`. -/
diff_subset_closure_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, s \ t ⊆ closure t ↔ s ⊆ closure t
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHomCompTriple.ids : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂},
  RingHomCompTriple (RingHom.id R₁) σ₁₂ σ₁₂
-- Mathlib.Topology.Homotopy.Lifting
IsQuotientCoveringMap.monodromyPerm_injective : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X} {G : Type u_4}
  [inst_2 : Group G] [inst_3 : MulAction G E] (hp : IsQuotientCoveringMap p G) {x : X} [SimplyConnectedSpace E],
  Function.Injective ⇑(⋯.monodromyPerm x)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq_lintegral_of_nonneg_ae : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ᵐ[μ] f → MeasureTheory.AEStronglyMeasurable f μ → ∫ (a : α), f a ∂μ = (∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ).toReal
-- Mathlib.Order.FixedPoints
OrderHom.le_map_sup_fixedPoints : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x y : ↑(Function.fixedPoints ⇑f)), ↑x ⊔ ↑y ≤ f (↑x ⊔ ↑y)