mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.SplitIfs
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.SplitPosition.hyp : Lean.FVarId → Mathlib.Tactic.SplitPosition✝
-- Std.Tactic.BVDecide.Bitblast.BoolExpr.Basic
Std.Tactic.BVDecide.BoolExpr.eval : {α : Type} → (α → Bool) → Std.Tactic.BVDecide.BoolExpr α → Bool
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Retrieve the underlying value from a `MulArchimedeanOrder` element.  -/
MulArchimedeanOrder.val : {M : Type u_1} → MulArchimedeanOrder M ≃ M
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `s : Cone F` whiskered by an equivalence `e` is a limit cone, so is `s`.  -/
CategoryTheory.Limits.IsLimit.ofWhiskerEquivalence : {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} →
              {s : CategoryTheory.Limits.Cone F} →
                (e : K ≌ J) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Cone.whisker e.functor s) →
                    CategoryTheory.Limits.IsLimit s
-- Lean.Elab.Tactic.Basic
/-- Declaration name of the executing elaborator, used by `mkTacticInfo` to persist it in the info tree  -/
Lean.Elab.Tactic.Context.elaborator : Lean.Elab.Tactic.Context → Lean.Name
-- Mathlib.LinearAlgebra.QuadraticForm.Radical
QuadraticMap.Nondegenerate.radical_eq_bot : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_4} [inst : AddCommGroup M] [inst_1 : AddCommGroup P] [inst_2 : CommRing R]
  [inst_3 : Module R M] [inst_4 : Module R P] {Q : QuadraticMap R M P}, QuadraticMap.Nondegenerate → Q.radical = ⊥
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.shiftFunctor_of_induced : ∀ {C : Type u_3} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_2} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a : A),
  CategoryTheory.shiftFunctor D a = s a
-- Lean.Parser.Extra
Lean.Parser.numLit.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.toAdditiveLeft_symm_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : AddZeroClass β] (a : Additive α →+ β) (a_1 : α),
  (MonoidHom.toAdditiveLeft.symm a) a_1 = Multiplicative.ofAdd (a (Additive.ofMul a_1))
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
/-- If a function is analytic on a set `s`, so are its successive derivatives.  -/
AnalyticOnNhd.iterated_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} [CompleteSpace F],
  AnalyticOnNhd 𝕜 f s → ∀ (n : ℕ), AnalyticOnNhd 𝕜 (deriv^[n] f) s
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_mul : ∀ {K : Type u_1} [inst : RCLike K] (r s : ℝ), ↑(r * s) = ↑r * ↑s
-- Mathlib.Algebra.Ring.Associator
/-- An a priori non-associative semiring is associative if the `AddMonoidHom` versions of
the multiplications `(x * y) * z` and `x * (y * z)` agree.  -/
AddMonoidHom.mulLeft₃_eq_mulRight₃_iff_associative : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R],
  AddMonoidHom.mulLeft₃ = AddMonoidHom.mulRight₃ ↔ Std.Associative fun x y => x * y
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Functor.IsLeftAdjoint.exists_rightAdjoint : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
  {left : CategoryTheory.Functor C D} [self : left.IsLeftAdjoint], ∃ right, Nonempty (left ⊣ right)
-- Mathlib.CategoryTheory.Preadditive.Projective.Basic
/-- A category "has enough projectives" if for every object `X` there is a projective object `P` and
an epimorphism `P ↠ X`.  -/
CategoryTheory.EnoughProjectives : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.to_double_hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} {hi₀₁ : c.Rel i₀ i₁} {K : HomologicalComplex C c} {φ φ' : K ⟶ HomologicalComplex.double f hi₀₁},
  φ.f i₀ = φ'.f i₀ → φ.f i₁ = φ'.f i₁ → φ = φ'
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_zero : ∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α], Matrix.IsHermitian 0
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
SSet.Subcomplex.PairingCore.WeakRankFunction.mk.sizeOf_spec : ∀ {X : SSet} {A : X.Subcomplex} {h : A.PairingCore} {α : Type v} [inst : PartialOrder α] [inst_1 : SizeOf α]
  (rank : h.ι → α) (lt : ∀ {x y : h.ι}, h.AncestralRel x y → h.dim x = h.dim y → rank x < rank y),
  sizeOf { rank := rank, lt := lt } = 1
-- Mathlib.CategoryTheory.Functor.TwoSquare
/-- Notation for the vertical identity 2-square.  -/
CategoryTheory.TwoSquare.«term𝟙ᵥ» : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT?ₘ'.match_1.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} [inst : Ord α] (k : α)
  (motive :
    Option ((a : α) × β a) →
      (Std.DTreeMap.Internal.Impl.ExplorationStep α β fun k' => (compare k k').then Ordering.gt) → Sort u_3)
  (base : Option ((a : α) × β a)) (a : List ((a : α) × β a))
  (a_1 : Std.DTreeMap.Internal.Cell α β fun k' => (compare k k').then Ordering.gt) (r : List ((a : α) × β a))
  (h_1 :
    (x : Option ((a : α) × β a)) →
      (k' : α) →
        (a : (compare k k').then Ordering.gt = Ordering.lt) →
          (v : β k') →
            (a_2 : List ((a : α) × β a)) → motive x (Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_2))
  (h_2 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_2 : Std.DTreeMap.Internal.Cell α β fun k' => (compare k k').then Ordering.gt) →
          (r : List ((a : α) × β a)) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_2 r))
  (h_3 :
    (base : Option ((a : α) × β a)) →
      (a : List ((a : α) × β a)) →
        (a_2 : α) →
          (a_3 : (compare k a_2).then Ordering.gt = Ordering.gt) →
            (a_4 : β a_2) → motive base (Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_2 a_3 a_4)),
  (match base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_1 r with
    | x, Std.DTreeMap.Internal.Impl.ExplorationStep.lt k' a v a_2 => h_1 x k' a v a_2
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.eq a a_2 r => h_2 base a a_2 r
    | base, Std.DTreeMap.Internal.Impl.ExplorationStep.gt a a_2 a_3 a_4 => h_3 base a a_2 a_3 a_4) =
    h_2 base a a_1 r
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.omega_strictMono : StrictMono ⇑Ordinal.omega
-- Mathlib.Tactic.ClearExcept
/-- Clears all hypotheses it can, except those provided after a minus sign, class instances, and
hidden auxiliary declarations (for example recursive hypotheses). Example:
```
  clear * - h₁ h₂
```
The intent is that `clear * -` only clears user-visible local declarations; hidden auxiliary
declarations should be handled by more specific mechanisms when needed.  -/
Lean.Elab.Tactic.clearExceptTactic : Lean.ParserDescr
-- Lean.Data.Lsp.Basic
Lean.Lsp.DeleteFile.instToJsonOptions.toJson : Lean.Lsp.DeleteFile.Options → Lean.Json
-- Lean.Parser.Basic
Lean.Parser.instReprLeadingIdentBehavior : Repr Lean.Parser.LeadingIdentBehavior
-- Mathlib.Condensed.Light.Small
/-- The equivalence of categories from light condensed objects to sheaves on a small site
equivalent to light profinite sets.
 -/
LightCondensed.equivSmall : (C : Type w) →
  [inst : CategoryTheory.Category.{v, w} C] →
    LightCondensed C ≌
      CategoryTheory.Sheaf
        ((CategoryTheory.equivSmallModel LightProfinite).inverse.inducedTopology
          (CategoryTheory.coherentTopology LightProfinite))
        C
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.coe_lieSpan_eq_span_of_forall_lie_eq_zero : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {s : Set L},
  (∀ x ∈ s, ∀ y ∈ s, ⁅x, y⁆ = 0) → (LieSubalgebra.lieSpan R L s).toSubmodule = Submodule.span R s
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_neg : ∀ {R : Type u} [inst : Ring R] (n : ℕ) (a : R), (Polynomial.monomial n) (-a) = -(Polynomial.monomial n) a
-- Mathlib.Topology.Algebra.Algebra
RingHom.copy.congr_simp : ∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f f_1 : α →+* β) (e_f : f = f_1)
  (f' f'_1 : α → β) (e_f' : f' = f'_1) (h : f' = ⇑f), f.copy f' h = f_1.copy f'_1 ⋯
-- Mathlib.CategoryTheory.Bicategory.Coherence
CategoryTheory.FreeBicategory.preinclusion_obj : ∀ {B : Type u} [inst : Quiver B] (a : B), (CategoryTheory.FreeBicategory.preinclusion B).obj { as := a } = a
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinder_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)),
  (CategoryTheory.PreOneHypercover.cylinder f g).Y k =
    CategoryTheory.Limits.pullback
      (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd)
        (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯)
          (F.toPullback p.snd))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯)
          (F.toPullback q.snd))
        (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
      (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.TreeMap.unitOfList l cmp).getKey! k = default
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.toOuterMeasure_apply : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α), μ.toOuterMeasure s = μ s
-- Mathlib.CategoryTheory.Bicategory.Extension
/-- Construct a left extension of `g : a ⟶ c` from a left extension of `g ≫ 𝟙 c`.  -/
CategoryTheory.Bicategory.LeftExtension.ofCompId : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          CategoryTheory.Bicategory.LeftExtension f
              (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c)) →
            CategoryTheory.Bicategory.LeftExtension f g
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.isEmpty_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [Std.TransCmp cmp], t.isEmpty = true ↔ t = ∅
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJₗ_apply : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R] (self : QuaternionAlgebra R c₁ c₂ c₃),
  (QuaternionAlgebra.imJₗ c₁ c₂ c₃) self = self.imJ
-- Lean.Meta.Tactic.Apply
/-- Compute the number of expected arguments and whether the result type is of the form
(?m ...) where ?m is an unassigned metavariable.
 -/
Lean.Meta.getExpectedNumArgsAux : Lean.Expr → Lean.MetaM (ℕ × Bool)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColimCompColimIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  [inst_2 : ∀ (c : C), CategoryTheory.Limits.HasColimitsOfShape (↑(F.obj c)) H]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfShape C H]
  (X : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H),
  CategoryTheory.Limits.fiberwiseColimCompColimIso.inv.app X = (CategoryTheory.Limits.colimitFiberwiseColimitIso X).inv
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_ne_neg_one : ∀ (z : Complex.UnitDisc), ↑z ≠ -1
-- Init.Data.Array.Range
_private.Init.Data.Array.Range.0.Array.ofFn.go.match_1.eq_1 : ∀ {n : ℕ} (motive : (x : ℕ) → x ≤ n → Sort u_1) (i : ℕ) (h : i + 1 ≤ n)
  (h_1 : (i : ℕ) → (h : i + 1 ≤ n) → motive i.succ h) (h_2 : (x : 0 ≤ n) → motive 0 x),
  (match i.succ, h with
    | i.succ, h => h_1 i h
    | 0, x => h_2 x) =
    h_1 i h
-- Mathlib.Analysis.Normed.Module.Ball.Action
mulActionSphereBall : {𝕜 : Type u_1} →
  {E : Type u_3} →
    [inst : NormedField 𝕜] →
      [inst_1 : SeminormedAddCommGroup E] →
        [NormedSpace 𝕜 E] → {r : ℝ} → MulAction ↑(Metric.sphere 0 1) ↑(Metric.ball 0 r)
-- Init.Data.SInt.Lemmas
ISize.toUSize_sub : ∀ (a b : ISize), (a - b).toUSize = a.toUSize - b.toUSize
-- Mathlib.Data.Finset.SMulAntidiagonal
Set.IsWF.min.congr_simp : ∀ {α : Type u_2} [inst : Preorder α] {s s_1 : Set α} (e_s : s = s_1) (hs : s.IsWF) (hn : s.Nonempty),
  hs.min hn = ⋯.min ⋯
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsCofilteredOrEmpty.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (X Y : C), ∃ W x x, True) →
    (∀ ⦃X Y : C⦄ (f g : X ⟶ Y),
        ∃ W h, CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp h g) →
      CategoryTheory.IsCofilteredOrEmpty C
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.isInvalidContinuationByte_eq_false_of_assemble₄_eq_some_left : ∀ {w x y z : UInt8} {c : Char},
  ByteArray.utf8DecodeChar?.assemble₄ w x y z = some c → ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = false
-- Init.Data.UInt.Lemmas
UInt16.instIsLinearOrder : Std.IsLinearOrder UInt16
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (toHom : E.Hom F.toPreZeroHypercover)
  (s₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom.s₀ i) (toHom.s₀ j))
  (h₁ : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁ k))
  (w₁₁ :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₁ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom.h₀ i))
      CategoryTheory.PreOneHypercover.Hom.w₁₁._autoParam)
  (w₁₂ :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₂ (s₁ k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom.h₀ j))
      CategoryTheory.PreOneHypercover.Hom.w₁₂._autoParam)
  (toHom_1 : E.Hom F.toPreZeroHypercover) (s₁_1 : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom_1.s₀ i) (toHom_1.s₀ j))
  (h₁_1 : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁_1 k))
  (w₁₁_1 :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁_1 k) (F.p₁ (s₁_1 k)) =
          CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom_1.h₀ i))
      CategoryTheory.PreOneHypercover.Hom.w₁₁._autoParam)
  (w₁₂_1 :
    autoParam
      (∀ {i j : E.I₀} (k : E.I₁ i j),
        CategoryTheory.CategoryStruct.comp (h₁_1 k) (F.p₂ (s₁_1 k)) =
          CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom_1.h₀ j))
      CategoryTheory.PreOneHypercover.Hom.w₁₂._autoParam),
  ({ toHom := toHom, s₁ := s₁, h₁ := h₁, w₁₁ := w₁₁, w₁₂ := w₁₂ } =
      { toHom := toHom_1, s₁ := s₁_1, h₁ := h₁_1, w₁₁ := w₁₁_1, w₁₂ := w₁₂_1 }) =
    (toHom = toHom_1 ∧ s₁ ≍ s₁_1 ∧ h₁ ≍ h₁_1)
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.continuousOn_rpowIntegrand₀₁_Ici : ∀ {p t : ℝ}, p ∈ Set.Ioo 0 1 → 0 < t → ContinuousOn (p.rpowIntegrand₀₁ t) (Set.Ici 0)
-- Mathlib.Data.NNRat.Defs
instCommSemiringNNRat : CommSemiring ℚ≥0
-- Mathlib.CategoryTheory.ObjectProperty.Basic
CategoryTheory.ObjectProperty.prop_of_is : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (P : CategoryTheory.ObjectProperty C) (X : C) [P.Is X],
  P X
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioi_sdiff_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Ioi a \ Set.Ioi b = Set.Ioc a b
-- Lean.MetavarContext
Lean.MetavarContext.getExprAssignmentCore? : Lean.MetavarContext → Lean.MVarId → Option Lean.Expr
-- Mathlib.CategoryTheory.Endofunctor.Algebra
/-- An algebra morphism with an underlying monomorphism hom in `C` is an algebra monomorphism.  -/
CategoryTheory.Endofunctor.Coalgebra.mono_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C}
  {X Y : CategoryTheory.Endofunctor.Coalgebra F} (f : X ⟶ Y) [h : CategoryTheory.Mono f.f], CategoryTheory.Mono f
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.ext_iff' : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] {χ₁ χ₂ : LieModule.Weight R L M}, ⇑χ₁ = ⇑χ₂ ↔ χ₁ = χ₂
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.sum_Ioc_mul_zeta_eq_sum : ∀ {R : Type u_2} [inst : Semiring R] (f : ArithmeticFunction R) (N : ℕ),
  ∑ n ∈ Finset.Ioc 0 N, (f * ↑ArithmeticFunction.zeta) n = ∑ n ∈ Finset.Ioc 0 N, f n * ↑(N / n)
-- Init.Data.Int.Order
Int.le_trans : ∀ {a b c : ℤ}, a ≤ b → b ≤ c → a ≤ c
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.comap_coe_atTop : Filter.comap NNReal.toReal Filter.atTop = Filter.atTop
-- Mathlib.Analysis.Normed.Group.Basic
dist_norm_norm_le : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), dist ‖a‖ ‖b‖ ≤ ‖a - b‖
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.break.sizeOf_spec : ∀ (ref : Lean.Syntax), sizeOf (Lean.Elab.Term.Do.Code.break ref) = 1 + sizeOf ref
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.toStrictlyUnitaryLaxFunctor_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C) (x : B), F.toStrictlyUnitaryLaxFunctor.obj x = F.obj x
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ.eq_1 : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A),
  AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToΓ 𝒜 f =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.ProjectiveSpectrum.Proj.awayToSection 𝒜 f)
      ((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.map (CategoryTheory.homOfLE ⋯).op)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.Location.mk' : ℕ → ℕ → ℕ → ℕ → String → Lean.Lsp.RefInfo.Location
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_card_fiberwise_eq_card_filter : ∀ {ι : Type u_1} {κ : Type u_5} [inst : DecidableEq κ] (s : Finset ι) (t : Finset κ) (g : ι → κ),
  ∑ j ∈ t, {i ∈ s | g i = j}.card = {i ∈ s | g i ∈ t}.card
-- Init.Data.String.Lemmas.Splits
/-- You might want to invoke `Slice.Pos.Splits.exists_eq_singleton_append_of_ne_startPos` to be able to apply this.  -/
String.Slice.Pos.Splits.prev : ∀ {t₁ : String} {c : Char} {t₂ : String} {s : String.Slice} {p : s.Pos} (h : p.Splits (t₁ ++ String.singleton c) t₂),
  (p.prev ⋯).Splits t₁ (String.singleton c ++ t₂)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Manifold
UpperHalfPlane.mdifferentiable_iff : ∀ {f : UpperHalfPlane → ℂ}, MDiff f ↔ DifferentiableOn ℂ (f ∘ ↑UpperHalfPlane.ofComplex) {z | 0 < z.im}
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
_private.Std.Tactic.BVDecide.LRAT.Internal.Assignment.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.eq_3 : ∀ (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg)
  (h_3 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both)
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned),
  (match Std.Tactic.BVDecide.LRAT.Internal.Assignment.both with
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.both => h_3 ()
    | Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned => h_4 ()) =
    h_3 ()
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.unitors_inv_equal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
-- Std.Time.Format
/-- Parses a `String` in the `AscTime` format and returns a `PlainDateTime` object in the GMT time zone.
 -/
Std.Time.PlainDateTime.fromAscTimeString : String → Except String Std.Time.PlainDateTime
-- Mathlib.Algebra.Ring.BooleanRing
toBoolRing_symmDiff : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a b : α), toBoolRing (symmDiff a b) = toBoolRing a + toBoolRing b
-- Mathlib.AlgebraicTopology.SimplicialSet.NerveAdjunction
CategoryTheory.nerve.functorOfNerveMap_obj : ∀ {C D : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  (φ :
    CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of C) ⟶
      CategoryTheory.Nerve.nerveFunctor₂.obj (CategoryTheory.Cat.of D))
  (x : C),
  (CategoryTheory.nerve.functorOfNerveMap φ).obj x =
    CategoryTheory.nerveEquiv
      ((CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op { obj := { len := 0 }, property := _proof_11✝ })))
        (CategoryTheory.nerveEquiv.symm x))
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.mk.inj : ∀ {R : Type u_2} {inst : CommRing R} {n : ℕ} {val val_1 : Fin n → Polynomial R},
  { val := val } = { val := val_1 } → val = val_1
-- Mathlib.Analysis.Normed.Module.MultipliableUniformlyOn
Summable.multipliableLocallyUniformlyOn_one_add : ∀ {α : Type u_1} {ι : Type u_2} {K : Set α} {u : ι → ℝ} {R : Type u_3} [inst : NormedCommRing R] [NormOneClass R]
  [CompleteSpace R] [inst_3 : TopologicalSpace α] {f : ι → α → R} [LocallyCompactSpace α],
  IsOpen K →
    Summable u →
      (∀ᶠ (i : ι) in Filter.cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) →
        (∀ (i : ι), ContinuousOn (f i) K) → MultipliableLocallyUniformlyOn (fun i x => 1 + f i x) K
-- Lean.Server.AsyncList
Lean.AsyncList.cons.inj : ∀ {ε : Type u} {α : Type v} {hd : α} {tl : Lean.AsyncList ε α} {hd_1 : α} {tl_1 : Lean.AsyncList ε α},
  Lean.AsyncList.cons hd tl = Lean.AsyncList.cons hd_1 tl_1 → hd = hd_1 ∧ tl = tl_1
-- Mathlib.Topology.Connected.TotallyDisconnected
isTotallyDisconnected_empty : ∀ {α : Type u} [inst : TopologicalSpace α], IsTotallyDisconnected ∅
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.maxKey!_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).isEmpty = false →
        (Std.DTreeMap.Raw.Const.modify t k f).maxKey! = if cmp t.maxKey! k = Ordering.eq then k else t.maxKey!
-- Mathlib.Algebra.Category.Grp.Kernels
/-- The cokernel cocone induced by the projection onto the quotient.  -/
AddCommGrpCat.cokernelCocone : {G H : AddCommGrpCat} → (f : G ⟶ H) → CategoryTheory.Limits.CokernelCofork f
-- Init.Core
PSigma.mk.injEq : ∀ {α : Sort u} {β : α → Sort v} (fst : α) (snd : β fst) (fst_1 : α) (snd_1 : β fst_1),
  (⟨fst, snd⟩ = ⟨fst_1, snd_1⟩) = (fst = fst_1 ∧ snd ≍ snd_1)