mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Module.Defs
smul_lt_smul_iff_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero β] [SMulPosStrictMono α β] [SMulPosReflectLT α β], 0 < b → (a₁ • b < a₂ • b ↔ a₁ < a₂)
-- Mathlib.Algebra.Homology.Embedding.Restriction
/-- The isomorphism `(K.restriction e).X i ≅ K.X i'` when `e.f i = i'`.  -/
HomologicalComplex.restrictionXIso : {ι : 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] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsRelIff] → {i : ι} → {i' : ι'} → e.f i = i' → ((K.restriction e).X i ≅ K.X i')
-- Init.System.IO
/-- Terminates the child process using the `SIGTERM` signal or a platform analogue.

If the process was started using `SpawnArgs.setsid`, terminates the entire process group instead.
 -/
IO.Process.Child.kill : {cfg : IO.Process.StdioConfig} → IO.Process.Child cfg → IO Unit
-- Mathlib.RepresentationTheory.Basic
Representation.asAlgebraHom_single : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (g : G) (r : k), ρ.asAlgebraHom (MonoidAlgebra.single g r) = r • ρ g
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.Hom.comm₁₂_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq₁ sq₂ : CategoryTheory.Square C} (self : sq₁.Hom sq₂)
  {Z : C} (h : sq₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp sq₁.f₁₂ (CategoryTheory.CategoryStruct.comp self.τ₂ h) =
    CategoryTheory.CategoryStruct.comp self.τ₁ (CategoryTheory.CategoryStruct.comp sq₂.f₁₂ h)
-- Lean.Meta.LazyDiscrTree
/-- Constant that import failed on.  -/
Lean.Meta.LazyDiscrTree.ImportFailure.const : Lean.Meta.LazyDiscrTree.ImportFailure → Lean.Name
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {F : CategoryTheory.Functor C D} {preimage : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)}
  {map_preimage :
    autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f)
      CategoryTheory.Functor.FullyFaithful.map_preimage._autoParam}
  {preimage_map :
    autoParam (∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f)
      CategoryTheory.Functor.FullyFaithful.preimage_map._autoParam}
  {preimage_1 : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y)}
  {map_preimage_1 :
    autoParam (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage_1 f) = f)
      CategoryTheory.Functor.FullyFaithful.map_preimage._autoParam}
  {preimage_map_1 :
    autoParam (∀ {X Y : C} (f : X ⟶ Y), preimage_1 (F.map f) = f)
      CategoryTheory.Functor.FullyFaithful.preimage_map._autoParam},
  { preimage := preimage, map_preimage := map_preimage, preimage_map := preimage_map } =
      { preimage := preimage_1, map_preimage := map_preimage_1, preimage_map := preimage_map_1 } →
    preimage = preimage_1
-- Lean.SubExpr
/-- Fold over the position starting at the leaf and heading to the root -/
Lean.SubExpr.Pos.foldr : {α : Type} → (ℕ → α → α) → Lean.SubExpr.Pos → α → α
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.basis_inl : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) [inst_3 : Nontrivial S],
  (Algebra.Generators.PresentationOfFreeCotangent.Aux.basis✝ D) (Sum.inl ()) =
    (Algebra.Generators.PresentationOfFreeCotangent.Aux.cotangentEquivProd✝ D).symm
      (Algebra.Generators.cMulXSubOneCotangent S (Algebra.Generators.PresentationOfFreeCotangent.Aux.gbar✝ D), 0)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
/-- An `M`-equivariant morphism induces an equivariant function on hom types.  -/
CategoryTheory.IsModHom.mulActionHom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {M : C} →
        [inst_2 : CategoryTheory.MonObj M] →
          {X : C} →
            [inst_3 : CategoryTheory.ModObj M X] →
              {Y : C} →
                [inst_4 : CategoryTheory.ModObj M Y] →
                  (f : X ⟶ Y) → [CategoryTheory.IsModHom M f] → (Z : C) → (Z ⟶ X) →ₑ[id] Z ⟶ Y
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.mapM.map.eq_def : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (f : α → m β) (as : Array α) (i : ℕ) (bs : Array β),
  Array.mapM.map✝ f as i bs =
    if hlt : i < as.size then do
      let __do_lift ← f as[i]
      Array.mapM.map✝ f as (i + 1) (bs.push __do_lift)
    else pure bs
-- Mathlib.Topology.MetricSpace.Dilation
Dilation.tendsto_cobounded : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [DilationClass F α β] (f : F),
  Filter.Tendsto (⇑f) (Bornology.cobounded α) (Bornology.cobounded β)
-- Lean.Environment
Lean.EnvExtension.idx : {σ : Type} → Lean.EnvExtension σ → ℕ
-- Mathlib.FieldTheory.Separable
Irreducible.separable : ∀ {F : Type u} [inst : Field F] [CharZero F] {f : Polynomial F}, Irreducible f → f.Separable
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.positionsFrom.eq_1 : ∀ {s : String.Slice} (p : s.Pos), String.Slice.positionsFrom p = { internalState := { currPos := p } }
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_of_nodup_add : ∀ {α : Type u_1} {s t : Multiset α}, (s + t).Nodup → Disjoint s t
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- `Multicofork.toSigmaCofork` as a functor.  -/
CategoryTheory.Limits.MultispanIndex.toSigmaCoforkFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MultispanShape} →
      (I : CategoryTheory.Limits.MultispanIndex J C) →
        {c : CategoryTheory.Limits.Cofan I.left} →
          (hc : CategoryTheory.Limits.IsColimit c) →
            {d : CategoryTheory.Limits.Cofan I.right} →
              CategoryTheory.Limits.IsColimit d →
                CategoryTheory.Functor (CategoryTheory.Limits.Multicofork I)
                  (CategoryTheory.Limits.Cofork (I.fstSigmaMapOfIsColimit d hc) (I.sndSigmaMapOfIsColimit d hc))
-- Lean.Language.Basic
Lean.Language.SnapshotTree.mk.inj : ∀ {element : Lean.Language.Snapshot} {children : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)}
  {element_1 : Lean.Language.Snapshot} {children_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)},
  { element := element, children := children } = { element := element_1, children := children_1 } →
    element = element_1 ∧ children = children_1
-- Mathlib.Algebra.Homology.HomotopyCategory
HomotopyCategory.instAdditiveHomologicalComplexQuotient : ∀ {ι : Type u_2} (V : Type u) [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  (c : ComplexShape ι), (HomotopyCategory.quotient V c).Additive
-- Lean.Meta.Tactic.Grind.Internalize
/-- Tries to eta-reduce the given expression.
If successful, pushes a new equality between the two terms.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.tryEta : Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.FiniteElement.mk_add_mk : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (x y : K)
  (hx : 0 ≤ ArchimedeanClass.mk x) (hy : 0 ≤ ArchimedeanClass.mk y),
  ArchimedeanClass.FiniteElement.mk x hx + ArchimedeanClass.FiniteElement.mk y hy =
    ArchimedeanClass.FiniteElement.mk (x + y) ⋯
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsInt.mk : ∀ {α : Type u} [inst : Ring α] {a : α} {n : ℤ}, a = ↑n → Mathlib.Meta.NormNum.IsInt a n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SignatureHelpTriggerKind.contentChange : Lean.Lsp.SignatureHelpTriggerKind
-- Init.Data.Iterators.Lemmas.Combinators.Append
Std.Iter.atIdxSlow?_append_of_productive : ∀ {α₁ α₂ β : Type w} [inst : Std.Iterator α₁ Id β] [inst_1 : Std.Iterator α₂ Id β] [Std.Iterators.Productive α₁ Id]
  [Std.Iterators.Productive α₂ Id] {it₁ : Std.Iter β} {it₂ : Std.Iter β} {n k : ℕ},
  Std.Iter.atIdxSlow? k it₁ = none →
    (∀ j < k, (Std.Iter.atIdxSlow? j it₁).isSome = true) →
      k ≤ n → Std.Iter.atIdxSlow? n (it₁.append it₂) = Std.Iter.atIdxSlow? (n - k) it₂
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {x y : S₁.HomotopyEquiv S₂},
  x.hom = y.hom →
    x.inv = y.inv → x.homotopyHomInvId ≍ y.homotopyHomInvId → x.homotopyInvHomId ≍ y.homotopyInvHomId → x = y
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
/-- A non-negative function with locally finite support is zero if and only if its logarithmic counting
functions is asymptotically bounded.
 -/
Function.locallyFinsuppWithin.zero_iff_logCounting_bounded : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {D : Function.locallyFinsuppWithin Set.univ ℤ},
  0 ≤ D → (D = 0 ↔ Function.locallyFinsuppWithin.logCounting D =O[Filter.atTop] 1)
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.involutiveNeg.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G], AddSubmonoid.involutiveNeg = Function.Injective.involutiveNeg SetLike.coe ⋯ ⋯
-- Mathlib.Algebra.Group.Defs
InvolutiveNeg.neg_neg : ∀ {A : Type u_2} [self : InvolutiveNeg A] (x : A), - -x = x
-- Mathlib.Analysis.Normed.Lp.LpEquiv
coe_algEquiv_lpBCF : ∀ {α : Type u_1} {A : Type u_4} {𝕜 : Type u_5} [inst : TopologicalSpace α] [inst_1 : DiscreteTopology α]
  [inst_2 : NormedRing A] [inst_3 : NormOneClass A] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A]
  (f : ↥(lp (fun x => A) ⊤)), ⇑((AlgEquiv.lpBCF α 𝕜) f) = ↑f
-- Mathlib.NumberTheory.NumberField.Basic
NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors : ∀ (K : Type u_1) [inst : Field K] [NumberField K],
  IsLocalization (Algebra.algebraMapSubmonoid (NumberField.RingOfIntegers K) (nonZeroDivisors ℤ)) K
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.toOuterMeasure : {α : Type u_6} → [inst : MeasurableSpace α] → MeasureTheory.Measure α → MeasureTheory.OuterMeasure α
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mem_toAddSubgroup : ∀ {R : Type u} [inst : NonAssocRing R] {s : Subring R} {x : R}, x ∈ s.toAddSubgroup ↔ x ∈ s
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.smul_mem_pointwise_smul : ∀ {K : Type u} [inst : Field K] {G : Type u_1} [inst_1 : Group G] [inst_2 : MulSemiringAction G K] (g : G) (x : K)
  (S : ValuationSubring K), x ∈ S → g • x ∈ g • S
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistribInvOfBasis_apply : ∀ {R : Type u_7} {M : Type u_8} {N : Type u_9} {ι : Type u_10} {κ : Type u_11} [inst : DecidableEq ι]
  [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] [inst_3 : Fintype κ] [inst_4 : CommSemiring R]
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : Module R M] [inst_8 : Module R N]
  (b : Module.Basis ι R M) (c : Module.Basis κ R N) (f : Module.Dual R (TensorProduct R M N)),
  (TensorProduct.dualDistribInvOfBasis b c) f = ∑ i, ∑ j, f (b i ⊗ₜ[R] c j) • b.dualBasis i ⊗ₜ[R] c.dualBasis j
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.coe_bot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N), ↑⊥ = ⊥
-- Mathlib.Topology.Algebra.InfiniteSum.Group
multipliable_iff_vanishing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] {f : β → α}
  [CompleteSpace α], Multipliable f ↔ ∀ e ∈ nhds 1, ∃ s, ∀ (t : Finset β), Disjoint t s → ∏ b ∈ t, f b ∈ e
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientInfEquivProdNormalizerQuotient.eq_1 : ∀ {G : Type u} [inst : Group G] (H N : Subgroup G) (hLE : H ≤ Subgroup.normalizer ↑N),
  QuotientGroup.quotientInfEquivProdNormalizerQuotient H N hLE =
    (QuotientGroup.quotientMulEquivOfEq ⋯).trans
      (QuotientGroup.quotientKerEquivOfSurjective
        ((QuotientGroup.mk' (N.subgroupOf (H ⊔ N))).comp (Subgroup.inclusion ⋯)) ⋯)
-- Mathlib.MeasureTheory.Measure.Regular
/-- Any locally finite measure on a second countable metrizable space
(or even a pseudometrizable space) is weakly regular.  -/
MeasureTheory.Measure.WeaklyRegular.of_pseudoMetrizableSpace_secondCountable_of_locallyFinite : ∀ {X : Type u_3} [inst : TopologicalSpace X] [TopologicalSpace.PseudoMetrizableSpace X] [SecondCountableTopology X]
  [inst_3 : MeasurableSpace X] [BorelSpace X] (μ : MeasureTheory.Measure X) [MeasureTheory.IsLocallyFiniteMeasure μ],
  μ.WeaklyRegular
-- Init.Data.String.Modify
String.Pos.offset_toSetOfLE : ∀ {s : String} {q p : s.Pos} {c : Char} {hp : p ≠ s.endPos} {hpq : q ≤ p}, (q.toSetOfLE p c hp hpq).offset = q.offset
-- Mathlib.CategoryTheory.Category.Cat
/-- Category of categories.  -/
CategoryTheory.Cat : Type (max (u + 1) u (v + 1))
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.instIsIsoHomInvCone : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d), CategoryTheory.IsIso f.inv.hom
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.le_mul_right : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : Associates M}, a ≤ a * b
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.algebraMap₀_mul : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ} (r : R)
  (a : TensorPower R n M), (TensorPower.cast R M ⋯) (GradedMonoid.GMul.mul (TensorPower.algebraMap₀ r) a) = r • a
-- Mathlib.Analysis.Calculus.Deriv.Basic
HasDerivWithinAt.congr_deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' g' : F} {x : 𝕜} {s : Set 𝕜},
  HasDerivWithinAt f f' s x → f' = g' → HasDerivWithinAt f g' s x
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_add_of_nonneg_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddLeftMono α] {a b : α}, 0 ≤ b → a ≤ a + b
-- Mathlib.Analysis.SpecialFunctions.Stirling
Stirling.stirlingSeq_one : Stirling.stirlingSeq 1 = Real.exp 1 / √2
-- Mathlib.Dynamics.FixedPoints.Basic
/-- If `x` is a fixed point of `f` and `g`, then it is a fixed point of `f ∘ g`.  -/
Function.IsFixedPt.comp : ∀ {α : Type u_1} {f g : α → α} {x : α}, Function.IsFixedPt f x → Function.IsFixedPt g x → Function.IsFixedPt (f ∘ g) x
-- Batteries.Data.Random.MersenneTwister
/-- 64 bit Mersenne Twister (MT19937-64) configuration.  -/
Batteries.Random.MersenneTwister.mt19937_64 : Batteries.Random.MersenneTwister.Config
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.TauPackage.index.congr_simp : ∀ {α : Type u_1} [inst : MetricSpace α] {β : Type u} [inst_1 : Nonempty β] (p p_1 : Besicovitch.TauPackage β α),
  p = p_1 → ∀ (a a_1 : Ordinal.{u}), a = a_1 → p.index a = p_1.index a_1
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.hasHomology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.Exact → S.HasHomology
-- Lean.Elab.MutualInductive
Lean.Elab.Command.ComputedFieldView.type : Lean.Elab.Command.ComputedFieldView → Lean.Term
-- Mathlib.CategoryTheory.Monoidal.Bimod
π_tensor_id_preserves_coequalizer_inv_colimMap_desc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {X Y Z X' Y' Z' : C} (f g : X ⟶ Y) (f' g' : X' ⟶ Y') (p : CategoryTheory.MonoidalCategoryStruct.tensorObj X Z ⟶ X')
  (q : CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z ⟶ Y')
  (wf :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) q =
      CategoryTheory.CategoryStruct.comp p f')
  (wg :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) q =
      CategoryTheory.CategoryStruct.comp p g')
  (h : Y' ⟶ Z') (wh : CategoryTheory.CategoryStruct.comp f' h = CategoryTheory.CategoryStruct.comp g' h),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.coequalizer.π f g) Z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.PreservesCoequalizer.iso (CategoryTheory.MonoidalCategory.tensorRight Z) f g).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimMap
            (CategoryTheory.Limits.parallelPairHom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z)
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight g Z) f' g' p q wf wg))
          (CategoryTheory.Limits.coequalizer.desc h wh))) =
    CategoryTheory.CategoryStruct.comp q h
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_zero_iff_zero : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (L' : LieSubalgebra R L)
  (x : ↥L'), ↑x = 0 ↔ x = 0
-- Init.Data.Bool
Bool.decide_iff_dist : ∀ (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q], decide (p ↔ q) = (decide p == decide q)
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- Auxiliary definition for `ProjectiveResolution.of`.  -/
CategoryTheory.ProjectiveResolution.ofComplex : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → [CategoryTheory.EnoughProjectives C] → C → ChainComplex C ℕ
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofNat' : ∀ (n : ℕ), (UInt16.ofNat n).toUInt8 = UInt8.ofNat n
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT_eq_getEntryGT : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β} {k : α}
  {hto : t.Ordered} {he : ∃ a ∈ t, compare a k = Ordering.gt},
  Std.DTreeMap.Internal.Impl.getKeyGT k t hto he = (Std.DTreeMap.Internal.Impl.getEntryGT k t hto he).fst
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (self : CategoryTheory.TwistShiftData C A) (a b c : A),
  self.z (a + b) c * self.z a b = self.z a (b + c) * self.z b c
-- Mathlib.Tactic.HigherOrder
/-- From a lemma of the shape `∀ x, f (g x) = h x`
derive an auxiliary lemma of the form `f ∘ g = h`
for reasoning about higher-order functions.
 -/
Mathlib.Tactic.mkHigherOrderType : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- A minimal Weierstrass equation has additive reduction if and only if
the valuation of its discriminant is less than 1 and the valuation of `a₄` is less than 1.  -/
WeierstrassCurve.HasAdditiveReduction : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → Prop
-- Init.Data.SInt.Basic
/-- Arithmetic right shift for 32-bit signed integers. Usually accessed via the `<<<` operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.shiftRight : Int32 → Int32 → Int32
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_orElse_Except_apply_eq : ∀ {ε : Type u_1} {α : Type u_2} {post : α → Prop} {epost : EPost⟨ε → Prop⟩} (x : Except ε α) (h : Unit → Except ε α),
  Std.Internal.Do.wp (OrElse.orElse x h) post epost =
    Std.Internal.Do.wp x post epost⟨fun x => Std.Internal.Do.wp (h ()) post epost⟩
-- Mathlib.Data.Sigma.Basic
/-- Map the left and right components of a sigma  -/
Sigma.map : {α₁ : Type u_2} →
  {α₂ : Type u_3} →
    {β₁ : α₁ → Type u_5} → {β₂ : α₂ → Type u_6} → (f₁ : α₁ → α₂) → ((a : α₁) → β₁ a → β₂ (f₁ a)) → Sigma β₁ → Sigma β₂
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_inv_hom_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) {Z : a ⟶ c}
  (h_1 : CategoryTheory.CategoryStruct.comp f h ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.hom) h_1) =
    h_1
-- Mathlib.RingTheory.Ideal.Colon
Submodule.colon_univ : ∀ {R : Type u_1} [inst : Semiring R] {I : Ideal R} [I.IsTwoSided], Submodule.colon I Set.univ = I
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.main : Lean.Meta.Sym.Pattern → Lean.Expr → Bool → Bool → Lean.Meta.Sym.SymM (Option Lean.Meta.Sym.MatchUnifyResult)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_mul_C_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R) (i : σ) (c : R),
  MvPolynomial.degreeOf i (p * MvPolynomial.C c) ≤ MvPolynomial.degreeOf i p
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- Composition by continuous linear maps on the left preserves `C^n` functions on domains.  -/
ContDiffOn.continuousLinearMap_comp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {s : Set E} {f : E → F} {n : WithTop ℕ∞} (g : F →L[𝕜] G),
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n (⇑g ∘ f) s
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_zero_zero : Nat.digits 0 0 = []
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_ediv_of_dvd : ∀ {a b : ℤ}, b ∣ a → a.fdiv b = a / b
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.minEntry?.induct_unfolding : ∀ {α : Type u} {β : Type v} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β) → Prop),
  motive Std.DTreeMap.Internal.Impl.leaf none →
    (∀ (size : ℕ) (k : α) (v : β) (r : Std.DTreeMap.Internal.Impl α fun x => β),
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) (some (k, v))) →
      (∀ (size : ℕ) (k : α) (v : β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
          (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β),
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
              (Std.DTreeMap.Internal.Impl.Const.minEntry? (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              (Std.DTreeMap.Internal.Impl.Const.minEntry? (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r))) →
        ∀ (a : Std.DTreeMap.Internal.Impl α fun x => β), motive a (Std.DTreeMap.Internal.Impl.Const.minEntry? a)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots.congr_simp : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] (p p_1 : Polynomial R), p = p_1 → p.roots = p_1.roots
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.DeclNameGenerator.mkUniqueName.curr : Lean.Environment → Lean.DeclNameGenerator → Lean.Name → Lean.Name