mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.instIsIsoMImageMonoFactorisationOfHasZeroObjectOfEpi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  CategoryTheory.IsIso (CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation f).m
-- Mathlib.Data.Real.ConjExponents
ENNReal.HolderConjugate.conj_eq : ∀ {p q : ENNReal} [h : p.HolderConjugate q], q = 1 + (p - 1)⁻¹
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_add_toIcoDiv_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R), toIcoMod hp a b + ↑(toIcoDiv hp a b) * p = b
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey?_le_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : k ∈ t), t.minKey?.get ⋯ = km → (cmp km k).isLE = true
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.foldM_eq_foldlM_toArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : δ → (a : α) → β a → m' δ} {init : δ},
  m.WF → Std.DHashMap.Raw.foldM f init m = Array.foldlM (fun a b => f a b.fst b.snd) init m.toArray
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.right_comp_retraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B : C} (f g : A ⟶ B)
  [inst_1 : CategoryTheory.IsCoreflexivePair f g],
  CategoryTheory.CategoryStruct.comp g (CategoryTheory.commonRetraction f g) = CategoryTheory.CategoryStruct.id A
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.coe_copy : ∀ {α : Type u_1} [inst : CompleteLattice α] (L : CompleteSublattice α) (s : Set α) (hs : s = ↑L), ↑(L.copy s hs) = s
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.associator_inv_apply : ∀ {R : Type u} [inst : CommSemiring R] {M N K : SemimoduleCat R} (m : ↑M) (n : ↑N) (k : ↑K),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.associator M N K).inv)
      (m ⊗ₜ[R] (n ⊗ₜ[R] k)) =
    m ⊗ₜ[R] n ⊗ₜ[R] k
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.comap_id : ∀ {M : Type u_1} [inst : Add M] (c : AddCon M), AddCon.comap id ⋯ c = c
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.instIsIntCastApply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : IsTopologicalAddGroup M], IsIntCastApply (M →L[R] M) M
-- Lean.MetavarContext
Lean.MetavarContext.mk : ℕ →
  ℕ →
    ℕ →
      ℕ →
        Lean.PersistentHashMap Lean.LMVarId Lean.LevelMetavarDecl →
          Lean.PersistentHashMap Lean.MVarId Lean.MetavarDecl →
            Lean.PersistentHashMap Lean.Name Lean.MVarId →
              Lean.PersistentHashMap Lean.LMVarId Lean.Level →
                Lean.PersistentHashMap Lean.MVarId Lean.Expr →
                  Lean.PersistentHashMap Lean.MVarId Lean.DelayedMetavarAssignment → Lean.MetavarContext
-- Aesop.Forward.RuleInfo
/-- Is this rule a constant rule (i.e., does it have neither premises nor a rule
pattern)? Note: the rule may still have instance arguments.  -/
Aesop.ForwardRuleInfo.isConstant : Aesop.ForwardRuleInfo → Bool
-- Lean.Expr
/-- `mkAppRevRange f b e args == mkAppRev f (revArgs.extract b e)`  -/
Lean.Expr.mkAppRevRange : Lean.Expr → ℕ → ℕ → Array Lean.Expr → Lean.Expr
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_inj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.MonoCoprod C] {I : Type u_2}
  (X : I → C) (c : CategoryTheory.Limits.Cofan X) (h : CategoryTheory.Limits.IsColimit c) (i : I)
  [CategoryTheory.Limits.HasCoproduct fun k => X ↑k], CategoryTheory.Mono (c.inj i)
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type r}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC] {J : Type w}
  [inst_3 : CategoryTheory.Category.{t, w} J] (F : CategoryTheory.Functor J C)
  [CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)] {D : CategoryTheory.Limits.Cone F}
  (hD : CategoryTheory.Limits.IsLimit D),
  Function.Injective fun x j => (CategoryTheory.ConcreteCategory.hom (D.π.app j)) x
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.succ_iSup_le_lsub_iff : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}), Order.succ (iSup f) ≤ Ordinal.lsub f ↔ ∃ i, f i = iSup f
-- Mathlib.GroupTheory.ResiduallyFinite
AddGroup.instResiduallyFiniteSum : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] [AddGroup.ResiduallyFinite G]
  [AddGroup.ResiduallyFinite G'], AddGroup.ResiduallyFinite (G × G')
-- Mathlib.Dynamics.SymbolicDynamics.Basic
SymbolicDynamics.FullShift.MulSubshift.mk.sizeOf_spec : ∀ {A : Type u_1} [inst : TopologicalSpace A] {G : Type u_2} [inst_1 : Monoid G] [inst_2 : SizeOf A] [inst_3 : SizeOf G]
  (carrier : Set (G → A)) (isClosed : IsClosed carrier)
  (mapsTo : ∀ (g : G), Set.MapsTo (SymbolicDynamics.FullShift.mulShift g) carrier carrier),
  sizeOf { carrier := carrier, isClosed := isClosed, mapsTo := mapsTo } = 1 + sizeOf isClosed
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- Given a class of morphisms `P`, this is the class of pullbacks
of morphisms in `P`.  -/
CategoryTheory.MorphismProperty.pullbacks : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.instHasZeroObjectPullbackShift : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.Limits.HasZeroObject (CategoryTheory.PullbackShift C φ)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.le_le_combine_cert.eq_1 : ∀ (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.le_le_combine_cert p₁ p₂ p₃ =
    (p₃ == (p₁.mul ↑p₂.leadCoeff.natAbs).combine (p₂.mul ↑p₁.leadCoeff.natAbs))
-- Mathlib.RingTheory.RingHom.Etale
RingHom.Etale.ofLocalizationSpan : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] => RingHom.Etale
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsHaarMeasure.toIsFiniteMeasureOnCompacts : ∀ {G : Type u_3} {inst : Group G} {inst_1 : TopologicalSpace G} {inst_2 : MeasurableSpace G}
  {μ : MeasureTheory.Measure G} [self : μ.IsHaarMeasure], MeasureTheory.IsFiniteMeasureOnCompacts μ
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the value for the key `k`, or `fallback` if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.getD : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → [Std.LawfulEqOrd α] → Std.DTreeMap.Internal.Impl α β → (k : α) → β k → β k
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.Std.DHashMap.Internal.Raw₀.emptyWithCapacity.eq_1 : ∀ {α : Type u} {β : α → Type v} (capacity : ℕ),
  Std.DHashMap.Internal.Raw₀.emptyWithCapacity capacity =
    ⟨{ size := 0,
        buckets :=
          Array.replicate (Std.DHashMap.Internal.numBucketsForCapacity✝ capacity).nextPowerOfTwo
            Std.DHashMap.Internal.AssocList.nil },
      ⋯⟩
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k k' fallback : α}, compare k k' = Ordering.eq → t.getKeyD k fallback = t.getKeyD k' fallback
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.conj_adjoint : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] {T : E →L[𝕜] E},
  T.IsPositive → ∀ (S : E →L[𝕜] F), (S ∘SL T ∘SL ContinuousLinearMap.adjoint S).IsPositive
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `antivary_inv_right₀`. -/
Monovary.inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, StrongLT 0 g → Monovary f g → Antivary f g⁻¹
-- Mathlib.Data.Set.Semiring
SetSemiring.mul_def : ∀ {α : Type u_1} [inst : Mul α] (s t : SetSemiring α), s * t = Set.up (SetSemiring.down s * SetSemiring.down t)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_div_eq_of_divAll : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.Poly.divAll k p = true →
    Int.Internal.Linear.Poly.denote ctx (Int.Internal.Linear.Poly.div k p) * k = Int.Internal.Linear.Poly.denote ctx p
-- Mathlib.Data.Nat.Digits.Lemmas
Nat.lt_of_mem_digitsAppend : ∀ {n b : ℕ}, 1 < b → ∀ (l i : ℕ), i ∈ b.digitsAppend l n → i < b
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_const_add : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ →
    ∀ (c : ℝ), ProbabilityTheory.variance (fun ω => c + X ω) μ = ProbabilityTheory.variance X μ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get_eq_get_get? : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h : m.WF) {a : α} {h' : a ∈ m},
  Std.DHashMap.Raw.Const.get m a h' = (Std.DHashMap.Raw.Const.get? m a).get ⋯
-- Mathlib.Logic.IsEmpty.Basic
isEmpty_ulift : ∀ {α : Type u_4}, IsEmpty (ULift.{u_5, u_4} α) ↔ IsEmpty α
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.X_mul_modMonomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (i : σ) (x : MvPolynomial σ R),
  ((MvPolynomial.X i * x).modMonomial fun₀ | i => 1) = 0
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
IsAssociatedPrime.map_of_injective : ∀ {R : Type u_1} [inst : CommSemiring R] {I : Ideal R} {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  IsAssociatedPrime I M → Function.Injective ⇑f → IsAssociatedPrime I M'
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.foldTR.loop.congr_simp : ∀ {α : Type u} (n : ℕ) (f f_1 : (i : ℕ) → i < n → α → α),
  f = f_1 →
    ∀ (j j_1 : ℕ) (e_j : j = j_1) (a : j ≤ n) (a_1 a_2 : α),
      a_1 = a_2 → Nat.foldTR.loop✝ n f j a a_1 = Nat.foldTR.loop✝ n f_1 j_1 ⋯ a_2
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.codeActionProvider? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.CodeActionOptions
-- Lean.Meta.Tactic.Grind.Util
/-- Converts `Grind.PreMatchCond` into `Grind.MatchCond`.
Recall that `Grind.PreMatchCond` uses default reducibility setting, but
`Grind.MatchCond` does not.
 -/
Lean.Meta.Grind.replacePreMatchCond : Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.inverse_eq_rpow_neg_one : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] {a : A},
  autoParam (IsStrictlyPositive a) CFC.inverse_eq_rpow_neg_one._auto_1 → Ring.inverse a = a ^ (-1)
-- Mathlib.Data.Sym.Sym2
Set.sym2_iInter : ∀ {α : Type u_1} {ι : Type u_4} (f : ι → Set α), (⋂ i, f i).sym2 = ⋂ i, (f i).sym2
-- Std.Http.Data.Status
/-- 423 Locked
 -/
Std.Http.Status.locked : Std.Http.Status
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.lift_apply_of : ∀ {G : Type u} [inst : Group G] {A : Type v} [inst_1 : CommGroup A] (f : G →* A) (x : G),
  (Abelianization.lift f) (Abelianization.of x) = f x
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_apply₀ : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet t (μ.restrict s) → (μ.restrict s) t = μ (t ∩ s)
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.totalAux.d₁_eq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  {i₁ i₁' : I₁},
  c₁.Rel i₁ i₁' →
    ∀ (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂),
      K.d₁ c₁₂ i₁ i₂ i₁₂ =
        c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
          CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂)
            (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h')
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.degree_integralNormalization : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.integralNormalization.degree = p.degree
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
/-- A version of `galLift` for `AlgEquiv`.
 -/
galLiftEquiv : {A : Type u_1} →
  (K : Type u_2) →
    (L : Type u_3) →
      (L₂ : Type u_4) →
        {B : Type u_6} →
          {B₂ : Type u_7} →
            [inst : CommRing A] →
              [inst_1 : CommRing B] →
                [inst_2 : CommRing B₂] →
                  [inst_3 : Algebra A B] →
                    [inst_4 : Algebra A B₂] →
                      [inst_5 : Field K] →
                        [inst_6 : Field L] →
                          [inst_7 : Field L₂] →
                            [inst_8 : Algebra A K] →
                              [IsFractionRing A K] →
                                [inst_10 : Algebra K L] →
                                  [inst_11 : Algebra A L] →
                                    [IsScalarTower A K L] →
                                      [inst_13 : Algebra K L₂] →
                                        [inst_14 : Algebra A L₂] →
                                          [IsScalarTower A K L₂] →
                                            [inst_16 : Algebra B L] →
                                              [IsScalarTower A B L] →
                                                [IsIntegralClosure B A L] →
                                                  [inst_19 : Algebra B₂ L₂] →
                                                    [IsScalarTower A B₂ L₂] →
                                                      [IsIntegralClosure B₂ A L₂] →
                                                        [Algebra.IsAlgebraic K L] →
                                                          [Algebra.IsAlgebraic K L₂] → (B ≃ₐ[A] B₂) → L ≃ₐ[K] L₂
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- Two n-simplices among cospherical points in n-space have the same
circumsphere.  -/
EuclideanGeometry.circumsphere_eq_of_cospherical : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {ps : Set P} {n : ℕ} [FiniteDimensional ℝ V],
  Module.finrank ℝ V = n →
    EuclideanGeometry.Cospherical ps →
      ∀ {sx₁ sx₂ : Affine.Simplex ℝ P n},
        Set.range sx₁.points ⊆ ps → Set.range sx₂.points ⊆ ps → sx₁.circumsphere = sx₂.circumsphere
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Cycle.formPerm_subsingleton : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (h : s.Subsingleton), s.formPerm ⋯ = 1
-- Mathlib.RingTheory.Coalgebra.Convolution
TensorProduct.map_convMul_map : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {C : Type u_5} [inst : CommSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A] [inst_3 : SMulCommClass R A A]
  [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C] [inst_6 : Module R C] [inst_7 : CoalgebraStruct R C]
  {D : Type u_7} [inst_8 : AddCommMonoid B] [inst_9 : Module R B] [inst_10 : CoalgebraStruct R B]
  [inst_11 : NonUnitalNonAssocSemiring D] [inst_12 : Module R D] [inst_13 : SMulCommClass R D D]
  [inst_14 : IsScalarTower R D D] {f h : WithConv (C →ₗ[R] A)} {g k : WithConv (B →ₗ[R] D)},
  WithConv.toConv (TensorProduct.map f.ofConv g.ofConv) * WithConv.toConv (TensorProduct.map h.ofConv k.ofConv) =
    WithConv.toConv (TensorProduct.map (f * h).ofConv (g * k).ofConv)
-- Mathlib.LinearAlgebra.Prod
LinearMap.snd_apply : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (x : M × M₂), (LinearMap.snd R M M₂) x = x.2
-- Mathlib.Order.Heyting.Boundary
/-- The boundary of an element of a co-Heyting algebra.  -/
Heyting.«term∂_» : Lean.ParserDescr
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.nsmul_pos_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.NatModule M] [Lean.Grind.OrderedAdd M]
  [inst_4 : LT M] [Std.LawfulOrderLT M] {k : ℕ} {a : M}, 0 < a → (0 < k • a ↔ 0 < k)
-- Mathlib.Topology.Covering.Basic
/-- If `x` is evenly covered by `f` with nonempty fiber `I`, then we can construct a
trivialization of `f` at `x` with fiber `I`.  -/
IsEvenlyCovered.toTrivialization' : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {I : Type u_3} →
            [inst_2 : TopologicalSpace I] → {x : X} → [Nonempty I] → IsEvenlyCovered f x I → Bundle.Trivialization I f
-- Mathlib.NumberTheory.LSeries.RiemannZeta
HurwitzZeta.hurwitzZetaEven_zero : HurwitzZeta.hurwitzZetaEven 0 = riemannZeta
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.evalConvSeq : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat
GenContFract.IntFractPair.coe_of_rat_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] [IsStrictOrderedRing K] {v : K}
  {q : ℚ},
  v = ↑q → GenContFract.IntFractPair.mapFr Rat.cast (GenContFract.IntFractPair.of q) = GenContFract.IntFractPair.of v
-- Init.Data.String.Substring
Substring.Raw.lt_next : ∀ (s : Substring.Raw) (i : String.Pos.Raw), i.byteIdx < s.bsize → i.byteIdx < (s.next i).byteIdx
-- Mathlib.Data.Multiset.Count
Multiset.count_eq_zero_of_notMem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∉ s → Multiset.count a s = 0
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.inter : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α x} {h : t₁.Balanced} (a : t₁.WF),
  Std.DTreeMap.Internal.Impl.WF.below a → motive t₁ a → Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Data.Nat.Basic
Nat.pow_left_injective : ∀ {n : ℕ}, n ≠ 0 → Function.Injective fun a => a ^ n
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.mk_neg : ∀ {M : Type u_1} [inst : Neg M] (a : M), DomAddAct.mk (-a) = -DomAddAct.mk a
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- The canonical isomorphism `F.rightDerived 0 ≅ F` when `F` is left exact
(i.e. preserves finite limits).  -/
CategoryTheory.Functor.rightDerivedZeroIsoSelf : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasInjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              (F : CategoryTheory.Functor C D) →
                [inst_5 : F.Additive] → [CategoryTheory.Limits.PreservesFiniteLimits F] → F.rightDerived 0 ≅ F
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.WF.tail? : ∀ {α : Type u_1} {s : Batteries.BinomialHeap.Imp.Heap α} {le : α → α → Bool} {n : ℕ}
  {tl : Batteries.BinomialHeap.Imp.Heap α},
  Batteries.BinomialHeap.Imp.Heap.WF le n s →
    Batteries.BinomialHeap.Imp.Heap.tail? le s = some tl → Batteries.BinomialHeap.Imp.Heap.WF le 0 tl
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_compl₀ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.NullMeasurableSet s μ → μ.real sᶜ = μ.real Set.univ - μ.real s
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the mapping for the given key, returning `fallback` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.DTreeMap.Raw.Const.getD : {α : Type u} → {cmp : α → α → Ordering} → {β : Type v} → Std.DTreeMap.Raw α (fun x => β) cmp → α → β → β
-- Init.Data.Int.DivMod.Lemmas
Int.bmod_zero : ∀ {m : ℤ}, m.bmod 0 = m
-- Mathlib.CategoryTheory.Adjunction.Lifting.Left
/-- Suppose we have a commutative square of functors

```
      Q
    A → B
  U ↓   ↓ V
    C → D
      R
```

where `U` has a left adjoint, `A` has reflexive coequalizers and `V` is monadic.
Then `Q` has a left adjoint if `R` has a left adjoint.

See https://ncatlab.org/nlab/show/adjoint+lifting+theorem
 -/
CategoryTheory.isRightAdjoint_square_lift_monadic : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (Q : CategoryTheory.Functor A B) (V : CategoryTheory.Functor B D)
  (U : CategoryTheory.Functor A C) (R : CategoryTheory.Functor C D) (comm : U.comp R ≅ Q.comp V) [U.IsRightAdjoint]
  [CategoryTheory.MonadicRightAdjoint V] [R.IsRightAdjoint] [CategoryTheory.Limits.HasReflexiveCoequalizers A],
  Q.IsRightAdjoint
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Return the maximum element of the tree, if it exists.

```
findMax {1, 2, 3} = some 3
findMax ∅ = none
```  -/
Ordnode.findMax : {α : Type u_1} → Ordnode α → Option α
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.const_mul : ∀ {a b : ℝ} {f : ℝ → ℝ} (α : ℝ),
  AbsolutelyContinuousOnInterval f a b → AbsolutelyContinuousOnInterval (fun x => α * f x) a b
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.quotEquivOfEq_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p p' : Submodule R M)
  (h : p = p') (x : M), (p.quotEquivOfEq p' h) (Submodule.Quotient.mk x) = Submodule.Quotient.mk x
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.mem_image_support_coeff_finSuccEquiv : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} {f : MvPolynomial (Fin (n + 1)) R} {i : ℕ} {x : Fin (n + 1) →₀ ℕ},
  x ∈ Finsupp.cons i '' ↑(((MvPolynomial.finSuccEquiv R n) f).coeff i).support ↔ x ∈ f.support ∧ x 0 = i
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.tryCatch_OptionT_lift : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε α : Type u}
  [inst_4 : MonadExceptOf ε m] (x : OptionT m α) (h : ε → OptionT m α) (post : α → Pred)
  (epost : EPost.Cons✝ Pred EPred),
  ⦃ Std.Internal.Do.wp (MonadExceptOf.tryCatch x h) (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail ⦄
    MonadExceptOf.tryCatch x h ⦃ post; epost ⦄
-- Mathlib.Combinatorics.SimpleGraph.IncMatrix
SimpleGraph.sum_incMatrix_apply_of_mem_edgeSet : ∀ {R : Type u_1} {α : Type u_2} (G : SimpleGraph α) [inst : NonAssocSemiring R] [inst_1 : DecidableEq α]
  [inst_2 : DecidableRel G.Adj] {e : Sym2 α} [inst_3 : Fintype α],
  e ∈ G.edgeSet → ∑ a, SimpleGraph.incMatrix R G a e = 2
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instOne : {α : Type u_1} → [One α] → One αᵒᵈ