mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
/-- Turn an additive functor into an object of the category `AdditiveFunctor C D`.  -/
CategoryTheory.AdditiveFunctor.of : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] → (F : CategoryTheory.Functor C D) → [F.Additive] → C ⥤+ D
-- Mathlib.Order.Filter.Extr
IsMaxFilter.neg : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] [inst_1 : PartialOrder β] [IsOrderedAddMonoid β] {f : α → β} {a : α}
  {l : Filter α}, IsMaxFilter f l a → IsMinFilter (fun x => -f x) l a
-- Mathlib.Tactic.Ring.Basic
Mathlib.Tactic.Ring.cast_neg : ∀ {n : ℕ} {R : Type u_2} [inst : Ring R] {a : R},
  Mathlib.Meta.NormNum.IsInt a (Int.negOfNat n) → a = (Int.negOfNat n).rawCast + 0
-- Mathlib.RingTheory.LaurentSeries
LaurentSeries.instAlgebraPowerSeries : {R : Type u_1} → [inst : CommSemiring R] → Algebra (PowerSeries R) (LaurentSeries R)
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.cosPoly.eq_3 : ∀ (n : ℕ), cosPoly✝ n.succ.succ = (2 * (2 * ↑n + 3)) • cosPoly✝ (n + 1) + (Polynomial.monomial 2) (-4) * cosPoly✝ n
-- Mathlib.Order.Antichain
IsAntichain.image_embedding_iff : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} [inst : LE α] [inst_1 : LE β] {φ : α ↪o β},
  IsAntichain (fun x1 x2 => x1 ≤ x2) (⇑φ '' s) ↔ IsAntichain (fun x1 x2 => x1 ≤ x2) s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constEntryAtIdx!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {i : ℕ},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.entryAtIdx! t₁ i = Std.DTreeMap.Raw.Const.entryAtIdx! t₂ i
-- Mathlib.ModelTheory.LanguageMap
/-- Pulls a structure back along a language map.  -/
FirstOrder.Language.LHom.reduct : {L : FirstOrder.Language} → {L' : FirstOrder.Language} → (L →ᴸ L') → (M : Type u_1) → [L'.Structure M] → L.Structure M
-- Mathlib.CategoryTheory.Functor.TypeValuedFlat
CategoryTheory.FunctorToTypes.instIsCofilteredElementsOverFromOverFunctor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X : C} (x : F.obj X)
  [CategoryTheory.IsCofiltered F.Elements],
  CategoryTheory.IsCofiltered (CategoryTheory.FunctorToTypes.fromOverFunctor F x).Elements
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trCont.eq_4 : ∀ (c : Turing.ToPartrec.Code) (k : Turing.ToPartrec.Cont),
  Turing.PartrecToTM2.trCont (Turing.ToPartrec.Cont.comp c k) =
    Turing.PartrecToTM2.Cont'.comp c (Turing.PartrecToTM2.trCont k)
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mker_snd : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N],
  MonoidHom.mker (MonoidHom.snd M N) = ⊤.prod ⊥
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_sup : ∀ {μ ν : YoungDiagram} {x : ℕ × ℕ}, x ∈ μ ⊔ ν ↔ x ∈ μ ∨ x ∈ ν
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.sum.eq_1 : ∀ {α : Type u} [inst : AddGroup α], FreeAddGroup.sum = FreeAddGroup.lift id
-- Mathlib.Algebra.Ring.Hom.Defs
AddMonoidHom.coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero : ∀ {α : Type u_2} {β : Type u_3} [inst : CommRing α] [inst_1 : IsDomain α] [inst_2 : CommRing β] (f : β →+ α)
  (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 ≠ 0) (h_one : f 1 = 1),
  ↑(f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = f
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.revAtFun_invol : ∀ {N i : ℕ}, Polynomial.revAtFun N (Polynomial.revAtFun N i) = i
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.reverse_toListRev : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α m β]
  [Std.Iterators.Finite α m] {it : Std.IterM m β}, List.reverse <$> it.toListRev = it.toList
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_symm_toEquiv : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ⇑e.toEquiv.symm = ⇑e.symm
-- Mathlib.Algebra.Category.Ring.Constructions
CommRingCat.coproductCoconeIsColimit_desc : ∀ (A B : CommRingCat) (s : CategoryTheory.Limits.BinaryCofan A B),
  (A.coproductCoconeIsColimit B).desc s =
    CommRingCat.ofHom
      (Algebra.TensorProduct.lift (CommRingCat.Hom.hom s.inl).toIntAlgHom (CommRingCat.Hom.hom s.inr).toIntAlgHom
          ⋯).toRingHom
-- Mathlib.Data.LawfulXor.Basic
instLawfulXorUInt8 : LawfulXor UInt8
-- Init.Data.UInt.Bitwise
USize.toUInt16_shiftLeft : ∀ (a b : USize), b < 16 → (a <<< b).toUInt16 = a.toUInt16 <<< b.toUInt16
-- Mathlib.Data.Sum.Order
Sum.noMinOrder : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] [NoMinOrder α] [NoMinOrder β], NoMinOrder (α ⊕ β)
-- Init.Core
Or.comm : ∀ {a b : Prop}, a ∨ b ↔ b ∨ a
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalence_functor : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C),
  (CategoryTheory.CostructuredArrow.ofCommaFstEquivalence F G c).functor =
    CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceFunctor F G c
-- Mathlib.Data.List.Sort
/-- The list `List.ofFn f` is sorted with respect to `(· ≥ ·)` if and only if `f` is antitone.  -/
List.sortedGE_ofFn_iff : ∀ {α : Type u_1} [inst : Preorder α] {n : ℕ} {f : Fin n → α}, (List.ofFn f).SortedGE ↔ Antitone f
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.instZero : {Γ : Subgroup (GL (Fin 2) ℝ)} → {k : ℤ} → Zero (SlashInvariantForm Γ k)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKeyLT?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKeyLT? k = t₂.getKeyLT? k
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
/-- `Real.sin` and `Real.arcsin` as a (partial) equivalence from `[-(π / 2), (π / 2)]` to
`[-1, 1]`  -/
Real.sinPartialEquiv : PartialEquiv ℝ ℝ
-- Mathlib.Data.List.Basic
List.map_erase : ∀ {α : Type u} {β : Type v} [inst : BEq α] [LawfulBEq α] [inst_2 : BEq β] [LawfulBEq β] {f : α → β},
  Function.Injective f → ∀ {a : α} (l : List α), List.map f (l.erase a) = (List.map f l).erase (f a)
-- Init.Data.List.FinRange
Fin.foldl_eq_finRange_foldl : ∀ {α : Type u_1} {n : ℕ} (f : α → Fin n → α) (x : α), Fin.foldl n f x = List.foldl f x (List.finRange n)
-- Lean.Parser.Command
Lean.Parser.Tactic.set_option.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Lean.Data.Lsp.Basic
/-- A workspace edit represents changes to many resources managed in the workspace.

[reference](https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#workspaceEdit)  -/
Lean.Lsp.WorkspaceEdit : Type
-- Init.Data.List.Control
_private.Init.Data.List.Control.0.List.findSome?.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Init.Core
/-- Auxiliary type used to compile `do` notation. It is used when compiling a do block
nested inside a combinator like `tryCatch`. It encodes the possible ways the
block can exit:
* `pure (a : α) s` means that the block exited normally with return value `a`.
* `return (b : β) s` means that the block exited via a `return b` early-exit command.
* `break s` means that `break` was called, meaning that we should exit
  from the containing loop.
* `continue s` means that `continue` was called, meaning that we should continue
  to the next iteration of the containing loop.

All cases return a value `s : σ` which bundles all the mutable variables of the do-block.
 -/
DoResultPRBC : Type u → Type u → Type u → Type u
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.restrictDegree.eq_1 : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R] (m : ℕ),
  MvPolynomial.restrictDegree σ R m = MvPolynomial.restrictSupport R {n | ∀ (i : σ), n i ≤ m}
-- Mathlib.CategoryTheory.Limits.Connected
/-- When `J` is a connected category, the limit of a
constant functor `J ⥤ C` with value `X : C` identifies to `X`.  -/
CategoryTheory.Limits.isLimitConstCone : (J : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} C] →
        (X : C) → [CategoryTheory.IsConnected J] → CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.constCone J X)
-- Mathlib.NumberTheory.Height.Basic
/-- The multiplicative height of `x + y` is at most `2 ^ totalWeight K`
times the product of the multiplicative heights of `x` and `y`.  -/
Height.mulHeight₁_add_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x y : K),
  Height.mulHeight₁ (x + y) ≤ 2 ^ Height.totalWeight K * Height.mulHeight₁ x * Height.mulHeight₁ y
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_of_isEmpty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a : α},
  m.isEmpty = true → m.get? a = none
-- Mathlib.Analysis.Convex.Jensen
/-- **Maximum principle** for convex functions. If a function `f` is convex on the convex hull of
`s`, then the eventual maximum of `f` on `convexHull 𝕜 s` lies in `s`.  -/
ConvexOn.exists_ge_of_mem_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β} {x : E} {t : Set E},
  ConvexOn 𝕜 s f → t ⊆ s → x ∈ (convexHull 𝕜) t → ∃ y ∈ t, f x ≤ f y
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.Path.fill.match_1.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode.Path α → RBTree.RBNode α → Sort u_2) →
    (x : RBTree.RBNode.Path α) →
      (x_1 : RBTree.RBNode α) →
        ((t : RBTree.RBNode α) → motive RBTree.RBNode.Path.root t) →
          ((c : RBTree.RBColor) →
              (parent : RBTree.RBNode.Path α) →
                (y : α) → (b a : RBTree.RBNode α) → motive (RBTree.RBNode.Path.left c parent y b) a) →
            ((c : RBTree.RBColor) →
                (a : RBTree.RBNode α) →
                  (y : α) →
                    (parent : RBTree.RBNode.Path α) →
                      (b : RBTree.RBNode α) → motive (RBTree.RBNode.Path.right c a y parent) b) →
              motive x x_1
-- Mathlib.CategoryTheory.Distributive.Cartesian
/-- The coproduct coprojections are monic in a Cartesian distributive category.  -/
CategoryTheory.IsCartesianDistributive.monoCoprod : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.IsCartesianDistributive C],
  CategoryTheory.Limits.MonoCoprod C
-- Mathlib.Logic.Small.Defs
Shrink.ext_iff : ∀ {α : Type v} [inst : Small.{w, v} α] {x y : Shrink.{w, v} α}, x = y ↔ (equivShrink α).symm x = (equivShrink α).symm y
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.map_map_apply : ∀ {G : Type u} [inst : Group G] {H : Type v} [inst_1 : Group H] (f : G →* H) {I : Type w} [inst_2 : Group I]
  {g : H →* I} {x : Abelianization G},
  (Abelianization.map g) ((Abelianization.map f) x) = (Abelianization.map (g.comp f)) x
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_inv_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionSemiring α] {q : ℚ≥0}, ↑q.num ≠ 0 → ↑q⁻¹ = (↑q)⁻¹
-- Mathlib.Data.Num.Basic
Num.instMul : Mul Num
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The functor which sends `⦋n⦌` to the simplicial set `Δ[n]` equipped by
the obvious augmentation towards the terminal object of the category of sets.  -/
SSet.Augmented.stdSimplex : CategoryTheory.Functor SimplexCategory SSet.Augmented
-- Mathlib.Computability.TuringMachine.Tape
/-- The map underlying this instance.  -/
Turing.PointedMap.f : {Γ : Type u} → {Γ' : Type v} → [inst : Inhabited Γ] → [inst_1 : Inhabited Γ'] → Turing.PointedMap Γ Γ' → Γ → Γ'
-- Init.Data.Array.Basic
/-- Counts the number of times an element occurs in an array.

Examples:
* `#[1, 1, 2, 3, 5].count 1 = 2`
* `#[1, 1, 2, 3, 5].count 5 = 1`
* `#[1, 1, 2, 3, 5].count 4 = 0`
 -/
Array.count : {α : Type u} → [BEq α] → α → Array α → ℕ
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.instSmallSigma : ∀ {α : Type v} {β : α → Type w} [Std.Internal.Small α] [∀ (a : α), Std.Internal.Small (β a)],
  Std.Internal.Small ((a : α) × β a)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.pairwise_toList_lt : ∀ {α : Type u} {r : Std.Rco α} [LE α] [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], List.Pairwise (fun a b => a < b) r.toList
-- Mathlib.RingTheory.Polynomial.Basic
Ideal.leadingCoeff.eq_1 : ∀ {R : Type u} [inst : Semiring R] (I : Ideal (Polynomial R)), I.leadingCoeff = ⨆ n, I.leadingCoeffNth n
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.getValue : {α : Type u} →
  {β : Type v} → [inst : BEq α] → (a : α) → (l : List ((_ : α) × β)) → Std.Internal.List.containsKey a l = true → β
-- Lean.Util.Path
Lean.getBuildDir : IO System.FilePath
-- Mathlib.Order.Interval.Set.LinearOrder
Set.notMem_Ioi : ∀ {α : Type u_1} [inst : LinearOrder α] {a c : α}, c ∉ Set.Ioi a ↔ c ≤ a
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.foldl_induction.go : ∀ {α : Type u_1} {β : Type u_2} {as : Array α} (motive : ℕ → β → Prop) {f : β → α → β},
  (∀ (i : Fin as.size) (b : β), motive (↑i) b → motive (↑i + 1) (f b as[i])) →
    ∀ {i j : ℕ} {b : β},
      j ≤ as.size → as.size ≤ i + j → motive j b → motive as.size (Array.foldlM.loop f as as.size ⋯ i j b)
-- Mathlib.GroupTheory.Finiteness
/-- Finite product of finitely generated additive groups is finitely generated.  -/
Pi.instAddGroupFG : ∀ {ι : Type u_5} [Finite ι] {G : ι → Type u_6} [inst : (i : ι) → AddGroup (G i)] [∀ (i : ι), AddGroup.FG (G i)],
  AddGroup.FG ((i : ι) → G i)
-- Init.Data.Array.Lemmas
Array.eq_of_mem_singleton : ∀ {α : Type u_1} {b a : α}, a ∈ #[b] → a = b
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- Gives a recurrence to compute the `n + 1`th value of the sequence of integer and fractional
parts of a value in case of non-termination.
 -/
GenContFract.IntFractPair.succ_nth_stream_eq_some_iff : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] {v : K} {n : ℕ}
  {ifp_succ_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v (n + 1) = some ifp_succ_n ↔
    ∃ ifp_n,
      GenContFract.IntFractPair.stream v n = some ifp_n ∧
        ifp_n.fr ≠ 0 ∧ GenContFract.IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_map : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [EquivBEq α] {f : (a : α) → β a → γ a}
  {l : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getEntry? k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) =
      Option.map (fun p => ⟨p.fst, f p.fst p.snd⟩) (Std.Internal.List.getEntry? k l)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.State.mk.sizeOf_spec : ∀ (exp : ℕ) (rings : Array Lean.Meta.Sym.Arith.CommRing) (semirings : Array Lean.Meta.Sym.Arith.CommSemiring)
  (ncRings : Array Lean.Meta.Sym.Arith.Ring) (ncSemirings : Array Lean.Meta.Sym.Arith.Semiring)
  (typeClassify : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Sym.Arith.ClassifyResult),
  sizeOf
      { exp := exp, rings := rings, semirings := semirings, ncRings := ncRings, ncSemirings := ncSemirings,
        typeClassify := typeClassify } =
    1 + sizeOf exp + sizeOf rings + sizeOf semirings + sizeOf ncRings + sizeOf ncSemirings + sizeOf typeClassify
-- Batteries.Data.Vector.Lemmas
Vector.getD_mk : ∀ {α : Type u_1} {n : ℕ} (a : Array α) (h : a.size = n) (i : ℕ) (x : α), (Vector.mk a h).getD i x = a.getD i x
-- Mathlib.Algebra.Group.End
Equiv.Perm.inv_eq_iff_eq : ∀ {α : Type u_4} {f : Equiv.Perm α} {x y : α}, f⁻¹ x = y ↔ x = f y
-- Mathlib.Order.Antichain
IsAntichain.image_relEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {r' : β → β → Prop} {s : Set α},
  IsAntichain r s → ∀ (φ : r ↪r r'), IsAntichain r' (⇑φ '' s)
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.coeff_toMvPowerSeries : ∀ {R : Type u_2} [inst : Semiring R] {σ : Type u_3} [inst_1 : Finite σ] {f : HahnSeries (σ →₀ ℕ) R} {n : σ →₀ ℕ},
  (MvPowerSeries.coeff n) (HahnSeries.toMvPowerSeries f) = f.coeff n
-- Mathlib.Condensed.Discrete.Colimit
/-- A finite set is the coproduct of its points in `LightProfinite`.  -/
LightCondensed.fintypeCatAsCofanIsColimit : (X : LightProfinite) → [Finite ↑X.toTop] → CategoryTheory.Limits.IsColimit (LightCondensed.fintypeCatAsCofan X)
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.entails_wp_of_pre_post : ∀ {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {x : Prog}
  {pre pre' : Pred} {post post' : Value → Pred} {epost : EPred},
  ⦃ pre' ⦄ x ⦃ post'; epost ⦄ →
    Lean.Order.PartialOrder.rel pre pre' →
      Lean.Order.PartialOrder.rel post' post → Lean.Order.PartialOrder.rel pre (Std.Internal.Do.wp x post epost)
-- Mathlib.Algebra.Category.Grp.Images
AddCommGrpCat.image.fac : ∀ {G H : AddCommGrpCat} (f : G ⟶ H),
  CategoryTheory.CategoryStruct.comp (AddCommGrpCat.factorThruImage f) (AddCommGrpCat.image.ι f) = f
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.isUnsatLe.eq_1 : ∀ (k : ℤ), (Int.Internal.Linear.Poly.num k).isUnsatLe = decide (k > 0)
-- Mathlib.Order.Atoms
Pi.isAtom_single : ∀ {ι : Type u_4} {π : ι → Type u} {i : ι} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (π i)]
  [inst_2 : (i : ι) → OrderBot (π i)] {a : π i}, IsAtom a → IsAtom (Function.update ⊥ i a)
-- Mathlib.Combinatorics.Young.SemistandardTableau
SemistandardYoungTableau.mk.injEq : ∀ {μ : YoungDiagram} (entry : ℕ → ℕ → ℕ) (row_weak' : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry i j1 ≤ entry i j2)
  (col_strict' : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry i1 j < entry i2 j)
  (zeros' : ∀ {i j : ℕ}, (i, j) ∉ μ → entry i j = 0) (entry_1 : ℕ → ℕ → ℕ)
  (row_weak'_1 : ∀ {i j1 j2 : ℕ}, j1 < j2 → (i, j2) ∈ μ → entry_1 i j1 ≤ entry_1 i j2)
  (col_strict'_1 : ∀ {i1 i2 j : ℕ}, i1 < i2 → (i2, j) ∈ μ → entry_1 i1 j < entry_1 i2 j)
  (zeros'_1 : ∀ {i j : ℕ}, (i, j) ∉ μ → entry_1 i j = 0),
  ({ entry := entry, row_weak' := row_weak', col_strict' := col_strict', zeros' := zeros' } =
      { entry := entry_1, row_weak' := row_weak'_1, col_strict' := col_strict'_1, zeros' := zeros'_1 }) =
    (entry = entry_1)
-- Batteries.Data.List.Basic
List.replaceF.eq_def : ∀ {α : Type u_1} (f : α → Option α) (x : List α),
  List.replaceF f x =
    match x with
    | [] => []
    | x :: xs =>
      match f x with
      | none => x :: List.replaceF f xs
      | some a => a :: xs
-- Mathlib.Algebra.GCDMonoid.Basic
normUnit_eq_one : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : Subsingleton αˣ] (x : α), normUnit x = 1
-- Mathlib.Algebra.Group.Submonoid.MulAction
Submonoid.smul_def : ∀ {M' : Type u_1} {α : Type u_2} [inst : MulOneClass M'] [inst_1 : SMul M' α] {S : Submonoid M'} (g : ↥S) (a : α),
  g • a = ↑g • a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
/-- The map (as a cocone) of a pushout cocone is colimit iff
the map (as a pushout cocone) is limit.  -/
CategoryTheory.Limits.PushoutCocone.isColimitMapCoconeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {W X Y : C} →
          {f : W ⟶ X} →
            {g : W ⟶ Y} →
              (c : CategoryTheory.Limits.PushoutCocone f g) →
                (G : CategoryTheory.Functor C D) →
                  CategoryTheory.Limits.IsColimit (G.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (c.map G)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.anyM_eq_match_step : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  Std.Iter.anyM p it =
    match ↑it.step with
    | Std.IterStep.yield it' x => do
      let __do_lift ← p x
      if __do_lift = true then pure true else Std.Iter.anyM p it'
    | Std.IterStep.skip it' => Std.Iter.anyM p it'
    | Std.IterStep.done => pure false
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.count_normalizedFactors_eq : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {p x : Ideal R} [hp : p.IsPrime] {n : ℕ},
  x ≤ p ^ n → ¬x ≤ p ^ (n + 1) → Multiset.count p (UniqueFactorizationMonoid.normalizedFactors x) = n
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- **Alias** of `neg_apply`. -/
ContinuousMultilinearMap.neg_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Neg β}
  {inst_2 : Neg F} [self : IsNegApply F α β] (f : F) (x : α), (-f) x = -f x
-- Mathlib.Data.Finset.Max
Finset.max_le_iff : ∀ {α : Type u_2} [inst : LinearOrder α] {m : WithBot α} {s : Finset α}, s.max ≤ m ↔ ∀ a ∈ s, ↑a ≤ m
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
denseRange_zsmul_iff_nsmul : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] {x : G},
  (DenseRange fun x_1 => x_1 • x) ↔ DenseRange fun x_1 => x_1 • x
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_smul : ∀ {M : Type u_2} {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Monoid M] [inst_2 : DistribMulAction M α]
  [inst_3 : SMulCommClass M α α] [inst_4 : IsScalarTower M α α] (m : M) (x : CentroidHom α), (m • x).toEnd = m • x.toEnd
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.add_def : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Add (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] (i : ι) (x y : G i),
  ⟦⟨i, x⟩⟧ + ⟦⟨i, y⟩⟧ = ⟦⟨i, x + y⟩⟧
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.toHoCat_map_eq_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.FibrantObject C} [HomotopicalAlgebra.IsCofibrant X.obj] (f g : X ⟶ Y),
  HomotopicalAlgebra.FibrantObject.toHoCat.map f = HomotopicalAlgebra.FibrantObject.toHoCat.map g ↔
    HomotopicalAlgebra.FibrantObject.homRel C f g
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Let `#click_suggestions` show the candidate lemmas that failed to apply.  -/
Mathlib.Tactic.ClickSuggestions.click_suggestions.debug : Lean.Option Bool
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The obvious triangle `X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂ ⟶ X₁⟦1⟧`.  -/
CategoryTheory.Pretriangulated.binaryBiproductTriangle : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (X₁ X₂ : C) →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂] → CategoryTheory.Pretriangulated.Triangle C
-- Mathlib.Analysis.RCLike.Sqrt
/-- The square root on `RCLike`.  -/
RCLike.sqrt : {𝕜 : Type u_1} → [RCLike 𝕜] → 𝕜 → 𝕜