mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- Isomorphic functors `Over Y ⥤ Over X` lift to isomorphic functors `MonoOver Y ⥤ MonoOver X`.
 -/
CategoryTheory.MonoOver.liftIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} →
      {D : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          {Y : D} →
            {F₁ F₂ : CategoryTheory.Functor (CategoryTheory.Over Y) (CategoryTheory.Over X)} →
              (h₁ :
                  ∀ (f : CategoryTheory.MonoOver Y),
                    CategoryTheory.Mono (F₁.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom) →
                (h₂ :
                    ∀ (f : CategoryTheory.MonoOver Y),
                      CategoryTheory.Mono (F₂.obj ((CategoryTheory.MonoOver.forget Y).obj f)).hom) →
                  (F₁ ≅ F₂) → (CategoryTheory.MonoOver.lift F₁ h₁ ≅ CategoryTheory.MonoOver.lift F₂ h₂)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.measure_botSet : ∀ {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], f.measure botSet = 0
-- Mathlib.LinearAlgebra.Matrix.ToLin
Matrix.toLinAlgEquiv_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) (A B : Matrix n n R),
  (Matrix.toLinAlgEquiv v₁) (A * B) = (Matrix.toLinAlgEquiv v₁) A ∘ₗ (Matrix.toLinAlgEquiv v₁) B
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableSet.disjointed : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : ℕ → Set α},
  (∀ (i : ℕ), MeasurableSet (f i)) → ∀ (n : ℕ), MeasurableSet (disjointed f n)
-- Mathlib.CategoryTheory.Category.RelCat
/-- A relation is an isomorphism in `RelCat` iff it is the image of an isomorphism in
`Type u`.  -/
CategoryTheory.RelCat.rel_iso_iff : ∀ {X Y : CategoryTheory.RelCat} (r : X ⟶ Y),
  CategoryTheory.IsIso r ↔ ∃ f, CategoryTheory.RelCat.graphFunctor.map f.hom = r
-- Init.Data.Int.Lemmas
Int.negSucc_mul_ofNat : ∀ (m n : ℕ), Int.negSucc m * ↑n = -↑(m.succ * n)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal
IsCyclotomicExtension.Rat.isPrime_span_zeta_sub_one : ∀ (p k : ℕ) [hp : Fact (Nat.Prime p)] {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  [hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  (Ideal.span {hζ.toInteger - 1}).IsPrime
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- Fintype of algebra homomorphism `F⟮α⟯ →ₐ[F] K`  -/
IntermediateField.fintypeOfAlgHomAdjoinIntegral : (F : Type u_1) →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {α : E} →
            {K : Type u} → [inst_3 : Field K] → [inst_4 : Algebra F K] → IsIntegral F α → Fintype (↥F⟮α⟯ →ₐ[F] K)
-- Mathlib.Data.Set.Basic
Set.forall_mem_const : ∀ {α : Type u} {s : Set α} {p : Prop} [Nonempty ↑s], (∀ x ∈ s, p) ↔ p
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.mk : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      {N : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L] →
            [inst_2 : AddCommGroup M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : LieRingModule L M] →
                      [inst_7 : LieRingModule L N] →
                        (toLinearMap : M →ₗ[R] N) →
                          (∀ {x : L} {m : M}, toLinearMap.toFun ⁅x, m⁆ = ⁅x, toLinearMap.toFun m⁆) → M →ₗ⁅R,L⁆ N
-- Init.Data.Rat.Lemmas
Rat.zero_num : Rat.num 0 = 0
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.subsingleton_coe_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] [Subsingleton G] (f : G →* N),
  (↑f.range).Subsingleton
-- Lean.PrettyPrinter.Parenthesizer
/-- Registers a parenthesizer for a syntax category.

`@[category_parenthesizer cat]` registers a declaration of type
`Lean.PrettyPrinter.CategoryParenthesizer` for the syntax category `cat`, which is used when
parenthesizing occurrences of `cat:prec` (`categoryParser cat prec`). Implementations should call
`maybeParenthesize` with the precedence and `cat`. If no category parenthesizer is registered, the
category will never be parenthesized, but still traversed for parenthesizing nested categories.
 -/
Lean.PrettyPrinter.categoryParenthesizerAttribute : Lean.KeyedDeclsAttribute Lean.PrettyPrinter.CategoryParenthesizer
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzeLet : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.CategoryTheory.Sites.LocallyBijective
CategoryTheory.GrothendieckTopology.W.isLocallySurjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {FA : A → A → Type u_1} {CA : A → Type w'}
  [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] [inst_3 : CategoryTheory.ConcreteCategory A FA]
  [J.WEqualsLocallyBijective A] {X Y : CategoryTheory.Functor Cᵒᵖ A} {f : X ⟶ Y},
  J.W f → CategoryTheory.Presheaf.IsLocallySurjective J f
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.map_smul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : CategoryTheory.HasShift D M] {X Y : C} {R : Type u_5}
  [inst_5 : Ring R] [inst_6 : CategoryTheory.Preadditive C] [inst_7 : CategoryTheory.Linear R C]
  [inst_8 : CategoryTheory.Preadditive D] [inst_9 : CategoryTheory.Linear R D] (r : R) {a : M}
  (α : CategoryTheory.ShiftedHom X Y a) (F : CategoryTheory.Functor C D) [inst_10 : F.CommShift M]
  [CategoryTheory.Functor.Linear R F], (r • α).map F = r • α.map F
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denote_concat : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (m₁ m₂ : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.Mon.denote ctx (m₁.concat m₂) =
    Lean.Grind.CommRing.Mon.denote ctx m₁ * Lean.Grind.CommRing.Mon.denote ctx m₂
-- Mathlib.Algebra.Star.SelfAdjoint
TrivialStar.isStarNormal : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] [TrivialStar R] {x : R}, IsStarNormal x
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instInfOpenNormalAddSubgroup : {G : Type u} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → Min (OpenNormalAddSubgroup G)
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {p : Polynomial R} (f : R →+* S),
  f p.leadingCoeff ≠ 0 → (Polynomial.map f p).leadingCoeff = f p.leadingCoeff
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.eqToHom_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Under X} (h : f = g),
  CategoryTheory.Under.Hom.right (CategoryTheory.eqToHom h) = CategoryTheory.eqToHom ⋯
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_mem_sub_iff : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, 0 ∈ s - t ↔ ¬Disjoint s t
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
/-- The set of associated primes of a module.  -/
associatedPrimes : (R : Type u_1) → [inst : CommSemiring R] → (M : Type u_2) → [inst_1 : AddCommMonoid M] → [Module R M] → Set (Ideal R)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.SimplexAlgorithm
/-- Check if the solution is found: the objective function is positive and all basic variables are
nonnegative.
 -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.checkSuccess : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    Mathlib.Tactic.Linarith.SimplexAlgorithm.SimplexAlgorithmM matType Bool
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.wl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (self : CategoryTheory.PreOneHypercover.Homotopy f g)
  (i : E.I₀), CategoryTheory.CategoryStruct.comp (self.a i) (F.p₁ (self.H i)) = f.h₀ i
-- Mathlib.NumberTheory.LSeries.Basic
/-- If `f` and `g` agree on large `n : ℕ`, then the `LSeries` of `f` converges at `s`
if and only if that of `g` does.  -/
LSeriesSummable_congr' : ∀ {f g : ℕ → ℂ} (s : ℂ), f =ᶠ[Filter.atTop] g → (LSeriesSummable f s ↔ LSeriesSummable g s)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionContext : Lean.FromJson Lean.Lsp.CodeActionContext
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.instBEqSign.beq_spec : ∀ (x y : Float.Model.UnpackedFloat.Sign), (x == y) = (x.ctorIdx == y.ctorIdx)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
preNormEDS'.eq_4 : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R), preNormEDS' b c d 3 = c
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
TopCat.toSSetObjEquiv_σ_apply : ∀ {X : TopCat} {n : ℕ} (x : (TopCat.toSSet.obj X).obj (Opposite.op { len := n })) (i : Fin (n + 1))
  (z : ↑(stdSimplex ℝ (Fin (n + 2)))),
  ((X.toSSetObjEquiv (Opposite.op { len := n + 1 }))
        ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.SimplicialObject.σ (TopCat.toSSet.obj X) i)) x))
      z =
    ((X.toSSetObjEquiv (Opposite.op { len := n })) x) (stdSimplex.map i.predAbove z)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.yoneda_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Limits.IndObjectPresentation.yoneda X).I = CategoryTheory.Discrete PUnit.{v + 1}
-- Std.Do.Triple.SpecLemmas
List.Cursor.length_prefix_le_length : ∀ {α : Type u_1} {l : List α} {c : l.Cursor}, c.prefix.length ≤ l.length
-- Mathlib.Analysis.Seminorm
Seminorm.ext : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  {p q : Seminorm 𝕜 E}, (∀ (x : E), p x = q x) → p = q
-- Mathlib.Topology.CWComplex.Classical.Graph
Topology.CWComplex.OneSkeletonGraph.not_exists_isLoopAt_iff_nontrivial : ∀ {X : Type u_1} [inst : TopologicalSpace X] {C : Set X} [inst_1 : Topology.CWComplex C]
  (e : Topology.RelCWComplex.cell C 1),
  (¬∃ x, (Topology.CWComplex.OneSkeletonGraph C).IsLoopAt e x) ↔ (Topology.RelCWComplex.cellFrontier 1 e).Nontrivial
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonClientCapabilities.toJson : Lean.Lsp.ClientCapabilities → Lean.Json
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.Arrows.pullbackCompatible_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C}
  {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B)
  [inst_1 : (CategoryTheory.Presieve.ofArrows X π).HasPairwisePullbacks] (x : (i : I) → P.obj (Opposite.op (X i))),
  CategoryTheory.Presieve.Arrows.Compatible P π x ↔ CategoryTheory.Presieve.Arrows.PullbackCompatible P π x
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.isUnit_jacobian_iff_aevalDifferential_bijective : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ],
  IsUnit P.jacobian ↔ Function.Bijective ⇑P.aevalDifferential
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.le_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C} {X Y : CategoryTheory.Subobject B}
  (f : CategoryTheory.Subobject.underlying.obj X ⟶ CategoryTheory.Subobject.underlying.obj Y),
  CategoryTheory.CategoryStruct.comp f Y.arrow = X.arrow → X ≤ Y
-- Init.Data.SInt.Bitwise
instIdempotentOpInt64HAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
Std.Iter.toList_takeWhile_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {P : β → Bool} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.takeWhile P it).toList = List.takeWhile P it.toList
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.of_uncurry_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ}
  {f : α → β → γ}, Measurable (Function.uncurry f) → ∀ {y : β}, Measurable fun x => f x y
-- Mathlib.SetTheory.ZFC.Class
/-- `SetLike.coe` as an equivalence.  -/
ZFSet.coeEquiv : ZFSet.{u} ≃ { s // Small.{u, u + 1} ↑s }
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_laxMonoidalToMon_obj_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (F : CategoryTheory.Mon C),
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.id F.X)
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.selfEquivSigmaOrbitsQuotientStabilizer'.eq_1 : ∀ (G : Type u) (X : Type v) [inst : Group G] [inst_1 : MulAction G X] {φ : Quotient (MulAction.orbitRel G X) → X}
  (hφ : Function.LeftInverse Quotient.mk'' φ),
  MulAction.selfEquivSigmaOrbitsQuotientStabilizer' G X hφ =
    Trans.trans (MulAction.selfEquivSigmaOrbits' G X)
      (Equiv.sigmaCongrRight fun ω => (Equiv.setCongr ⋯).trans (MulAction.orbitEquivQuotientStabilizer G (φ ω)))
-- Mathlib.GroupTheory.Coset.Basic
QuotientAddGroup.orbit_mk_eq_vadd : ∀ {α : Type u_1} [inst : AddGroup α] {s : AddSubgroup α} (x : α), AddAction.orbitRel.Quotient.orbit ↑x = x +ᵥ ↑s
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.continuous_precomp : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] {E₁ : ι → Type u_5} [inst_8 : (i : ι) → TopologicalSpace (E₁ i)]
  [ContinuousConstSMul 𝕜 F] [inst_10 : (i : ι) → AddCommGroup (E₁ i)] [inst_11 : (i : ι) → Module 𝕜 (E₁ i)]
  (f : (i : ι) → E i →L[𝕜] E₁ i), Continuous fun g => g.compContinuousLinearMap f
-- Mathlib.Computability.Primrec.Basic
Primrec₂.unpaired' : ∀ {f : ℕ → ℕ → ℕ}, Nat.Primrec (Nat.unpaired f) ↔ Primrec₂ f
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.HeadCheck.unconditional.sizeOf_spec : sizeOf Lean.Elab.Term.Quotation.HeadCheck.unconditional = 1
-- Mathlib.Analysis.Convex.Deriv
ConvexOn.hasDerivWithinAt_rightDeriv_of_mem_interior : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x : ℝ},
  ConvexOn ℝ S f → x ∈ interior S → HasDerivWithinAt f (derivWithin f (Set.Ioi x) x) (Set.Ioi x) x
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.isPFilter_gabrielComposition : ∀ {A : Type u_1} [inst : Ring A] (F G : IdealFilter A), Order.IsPFilter {L | ∃ K ∈ G, F.IsTorsionQuot L K}
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach.0.Std.Iterators.Types.Attach.Monadic.modifyStep.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] {P : β → Prop}
  (it : Std.IterM m { out // P out }) (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM m β)
  (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) →
        (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' out)) →
          motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 :
    (it' : Std.IterM m β) →
      (h : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get?_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, k ∉ t₂ → Std.DTreeMap.Const.get? (t₁ ∩ t₂) k = none
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.lt_of_lt_stdPart : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K} (f : ℝ →+*o K) {r : ℝ},
  0 ≤ ArchimedeanClass.mk x → r < ArchimedeanClass.stdPart x → f r < x
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Mon.mul.go.match_1.eq_2 : ∀ (motive : Lean.Grind.CommRing.Mon → Lean.Grind.CommRing.Mon → Sort u_1) (m₂ : Lean.Grind.CommRing.Mon)
  (h_1 : (m₁ : Lean.Grind.CommRing.Mon) → motive m₁ Lean.Grind.CommRing.Mon.unit)
  (h_2 : (m₂ : Lean.Grind.CommRing.Mon) → motive Lean.Grind.CommRing.Mon.unit m₂)
  (h_3 :
    (pw₁ : Lean.Grind.CommRing.Power) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (pw₂ : Lean.Grind.CommRing.Power) →
          (m₂ : Lean.Grind.CommRing.Mon) →
            motive (Lean.Grind.CommRing.Mon.mult pw₁ m₁) (Lean.Grind.CommRing.Mon.mult pw₂ m₂)),
  (m₂ = Lean.Grind.CommRing.Mon.unit → False) →
    (match Lean.Grind.CommRing.Mon.unit, m₂ with
      | m₁, Lean.Grind.CommRing.Mon.unit => h_1 m₁
      | Lean.Grind.CommRing.Mon.unit, m₂ => h_2 m₂
      | Lean.Grind.CommRing.Mon.mult pw₁ m₁, Lean.Grind.CommRing.Mon.mult pw₂ m₂ => h_3 pw₁ m₁ pw₂ m₂) =
      h_2 m₂
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.toCocone_ι_app_right : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (c : CategoryTheory.Limits.BinaryBicone P Q),
  c.toCocone.ι.app { as := CategoryTheory.Limits.WalkingPair.right } = c.inr
-- Mathlib.Analysis.Normed.Lp.Finsupp
Finsupp.edist_def : ∀ {ι : Type u_1} {X : Type u_2} [inst : Zero X] [inst_1 : PseudoEMetricSpace X] {p : NNReal} [inst_2 : Fact (1 ≤ p)]
  (f g : WithLp (↑p) (ι →₀ X)), edist f g = ((Finsupp.zipWith edist ⋯ f.ofLp g.ofLp).sum fun _i r => r ^ ↑p) ^ (↑p)⁻¹
-- Mathlib.Topology.UniformSpace.Basic
_private.Mathlib.Topology.UniformSpace.Basic.0.«term_∘₂_» : Lean.TrailingParserDescr
-- Std.Sync.RecursiveMutex
/-- `mutex.tryAtomically k` tries to lock `mutex` and runs `k` on it if it succeeds. On success the
return value of `k` is returned as `some`, on failure `none` is returned.

This function does not block on the `mutex`. Additionally `mutex.tryAtomically`, while already
holding the underlying `BaseRecursiveMutex` in the same thread, does not block.
 -/
Std.RecursiveMutex.tryAtomically : {m : Type → Type} →
  {α β : Type} →
    [Monad m] → [MonadLiftT BaseIO m] → [MonadFinally m] → Std.RecursiveMutex α → Std.AtomicT α m β → m (Option β)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGT_obj_obj₂ : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (j : C), ((t.triangleLEGT n).obj j).obj₂ = j
-- Mathlib.Order.CompleteLattice.Basic
unary_relation_sInf_iff : ∀ {α : Type u_8} (s : Set (α → Prop)) {a : α}, sInf s a ↔ ∀ r ∈ s, r a
-- Std.Time.Zoned
/-- Converts a `DateTime` to a `PlainDate`
 -/
Std.Time.DateTime.toPlainDate : Std.Time.DateTime → Std.Time.PlainDate
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.CommandCodeActionEntry.mk.inj : ∀ {declName : Lean.Name} {cmdKinds : Array Lean.Name} {declName_1 : Lean.Name} {cmdKinds_1 : Array Lean.Name},
  { declName := declName, cmdKinds := cmdKinds } = { declName := declName_1, cmdKinds := cmdKinds_1 } →
    declName = declName_1 ∧ cmdKinds = cmdKinds_1
-- Lean.Meta.Hint
/-- The syntax to render in the inline diff preview. This syntax must have valid position information
and must contain the span at which the edit occurs.
 -/
Lean.Meta.Hint.Suggestion.previewSpan? : Lean.Meta.Hint.Suggestion → Option Lean.Syntax
-- Init.Data.Ord.Basic
Ordering.isLT_iff_eq_lt : ∀ {o : Ordering}, o.isLT = true ↔ o = Ordering.lt
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
Submodule.reflection_orthogonal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection],
  Kᗮ.reflection = K.reflection.trans (LinearIsometryEquiv.neg 𝕜)
-- Mathlib.Topology.Category.Profinite.Extend
Profinite.Extend.cocone_pt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profiniteᵒᵖ C)
  (S : Profinite), (Profinite.Extend.cocone G S).pt = G.obj (Opposite.op S)
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousLinearMap.analyticOn_uncurry_of_multilinear : ∀ {𝕜 : Type u_1} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] {ι : Type u_5}
  {Em : ι → Type u_6} [inst_5 : (i : ι) → NormedAddCommGroup (Em i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_7 : Fintype ι] (f : G →L[𝕜] ContinuousMultilinearMap 𝕜 Em F) {s : Set (G × ((i : ι) → Em i))},
  AnalyticOn 𝕜 (fun p => (f p.1) p.2) s
-- Mathlib.Algebra.Homology.HomologicalBicomplex
HomologicalComplex₂.d_comm_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (i₁ i₁' : I₁) (i₂ i₂' : I₂) {Z : C} (h : (K.X i₁').X i₂' ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (CategoryTheory.CategoryStruct.comp ((K.X i₁').d i₂ i₂') h) =
    CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂') h)
-- Mathlib.Data.Real.ConjExponents
Real.HolderTriple.of_pos : ∀ {p q : ℝ}, 0 < p → 0 < q → p.HolderTriple q (p⁻¹ + q⁻¹)⁻¹
-- Mathlib.Data.List.DropRight
List.rtakeWhile_idempotent : ∀ {α : Type u_1} (p : α → Bool) (l : List α), List.rtakeWhile p (List.rtakeWhile p l) = List.rtakeWhile p l
-- Mathlib.RingTheory.Adjoin.PowerBasis
PowerBasis.ofAdjoinEqTop_dim : ∀ {K : Type u_1} {S : Type u_2} [inst : Field K] [inst_1 : CommRing S] [inst_2 : Algebra K S] {x : S}
  (hx : IsIntegral K x) (hx' : K[x] = ⊤), (PowerBasis.ofAdjoinEqTop hx hx').dim = (minpoly K x).natDegree
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.antilipschitzWith_addEquiv : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A], AntilipschitzWith 2 ⇑(Unitization.addEquiv 𝕜 A)
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.mul_apply : ∀ {S : Type u_1} {R : Type u_2} [inst : Mul R] [inst_1 : Add R] [inst_2 : Star R] [inst_3 : SMul S R] (f g : R ≃⋆ₐ[S] R)
  (x : R), (f * g) x = f (g x)
-- Init.Data.Nat.Div.Basic
Nat.modCore_eq : ∀ (x y : ℕ), x.modCore y = if 0 < y ∧ y ≤ x then (x - y).modCore y else x
-- Init.Data.Vector.Lemmas
Vector.getElem_set : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} {x : α} (hi : i < n) {j : ℕ} (hj : j < n),
  (xs.set i x hi)[j] = if i = j then x else xs[j]
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trLList.eq_def : ∀ (x : List (List ℕ)),
  Turing.PartrecToTM2.trLList x =
    match x with
    | [] => []
    | l :: ls => Turing.PartrecToTM2.trList l ++ Turing.PartrecToTM2.Γ'.consₗ :: Turing.PartrecToTM2.trLList ls