mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
/-- Given `f : T ⟶ X`, `g : T ⟶ Y`, and `i : S ⟶ T`, the diagram
```
X ⨿ₛ Y ⟶ X ⨿ₜ Y
  ↑        ↑
  |        |
  |        |
T ⨿ₛ T  ⟶  T
```
is a pushout square.
 -/
CategoryTheory.Limits.isPushout_map_codiagonal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPushouts C]
  {S T : C} (f : T ⟶ X) (g : T ⟶ Y) (i : S ⟶ T),
  CategoryTheory.IsPushout
    (CategoryTheory.Limits.pushout.map i i (CategoryTheory.CategoryStruct.comp i f)
      (CategoryTheory.CategoryStruct.comp i g) f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
    (CategoryTheory.Limits.pushout.codiagonal i)
    (CategoryTheory.Limits.pushout.map (CategoryTheory.CategoryStruct.comp i f) (CategoryTheory.CategoryStruct.comp i g)
      f g (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) i ⋯ ⋯)
    (CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.pushout.inl f g))
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.inv_mul_eq_inv_mul_iff : ∀ {α : Type u} [inst : DivisionCommMonoid α] {a b c d : α}, IsUnit b → IsUnit d → (b⁻¹ * a = d⁻¹ * c ↔ a * d = c * b)
-- Mathlib.SetTheory.Ordinal.Topology
Ordinal.IsAcc.forall_lt : ∀ {o : Ordinal.{u_1}} {S : Set Ordinal.{u_1}}, o.IsAcc S → ∀ p < o, (S ∩ Set.Ioo p o).Nonempty
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
/-- `limsup (xᵢ + c) = (limsup xᵢ) + c`.  -/
limsup_add_const : ∀ {ι : Type u_1} {R : Type u_4} [inst : ConditionallyCompleteLinearOrder R] [inst_1 : TopologicalSpace R]
  [OrderTopology R] (F : Filter ι) [F.NeBot] [inst_4 : Add R] [ContinuousAdd R] [AddRightMono R] (f : ι → R) (c : R),
  Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) F f →
    Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) F f → Filter.limsup (fun i => f i + c) F = Filter.limsup f F + c
-- Lean.Data.Lsp.Basic
Lean.Lsp.CreateFile.Options.mk : Bool → Bool → Lean.Lsp.CreateFile.Options
-- Mathlib.Order.Interval.Set.OrderIso
OrderIso.image_Ioo : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃o β) (a b : α),
  ⇑e '' Set.Ioo a b = Set.Ioo (e a) (e b)
-- Mathlib.Algebra.CharP.Frobenius
iterate_frobenius : ∀ {R : Type u_1} [inst : CommSemiring R] (p n : ℕ) [inst_1 : ExpChar R p] (x : R), (⇑(frobenius R p))^[n] x = x ^ p ^ n
-- Mathlib.Algebra.Lie.Free
/-- The universal enveloping algebra of the free Lie algebra is just the free unital associative
algebra.  -/
FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra : (R : Type u) →
  (X : Type v) → [inst : CommRing R] → UniversalEnvelopingAlgebra R (FreeLieAlgebra R X) ≃ₐ[R] FreeAlgebra R X
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Multiplying by all the matrices in `listTransvecRow M` does not change the last column.  -/
Matrix.Pivot.mul_listTransvecRow_last_col : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ} (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜) (i : Fin r ⊕ Unit),
  (M * (Matrix.Pivot.listTransvecRow M).prod) i (Sum.inr ()) = M i (Sum.inr ())
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroupRel'.inhabited : (R : Type u) → [inst : Rack R] → Inhabited (Rack.PreEnvelGroupRel' R Rack.PreEnvelGroup.unit Rack.PreEnvelGroup.unit)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instVAddCommClass : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {R₁ : Type u_4} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : VAdd R M] [inst_3 : ContinuousConstVAdd R M] [inst_4 : VAdd R₁ M] [inst_5 : ContinuousConstVAdd R₁ M]
  [VAddCommClass R R₁ M], VAddCommClass R R₁ C(α, M)
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
/-- The "inclusion" `N n ⟶ X _⦋n⦌` for all `n : ℕ`.  -/
CategoryTheory.SimplicialObject.Splitting.ι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X : CategoryTheory.SimplicialObject C} →
      (self : X.Splitting) → (n : ℕ) → self.N n ⟶ X.obj (Opposite.op { len := n })
-- Mathlib.Algebra.Group.Action.Defs
Mul.toSMulMulOpposite.eq_1 : ∀ (α : Type u_9) [inst : Mul α], Mul.toSMulMulOpposite α = { smul := fun a b => b * MulOpposite.unop a }
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- If `K` is a field, the function `seminormFromConst` is a `RingNorm` on `K`.  -/
normFromConst : {K : Type u_1} → [inst : Field K] → {k : K} → {g : RingSeminorm K} → g 1 ≤ 1 → g k ≠ 0 → IsPowMul ⇑g → RingNorm K
-- Lean.Data.NameMap.Basic
Lean.NameSet.insert : Lean.NameSet → Lean.Name → Lean.NameSet
-- Mathlib.Topology.FiberBundle.Constructions
/-- The diagonal map from the total space of the fiberwise product of two fiber bundles
`E₁`, `E₂` into `TotalSpace F₁ E₁ × TotalSpace F₂ E₂` is an inducing map.  -/
FiberBundle.Prod.isInducing_diag : ∀ {B : Type u_1} (F₁ : Type u_2) (E₁ : B → Type u_3) (F₂ : Type u_4) (E₂ : B → Type u_5)
  [inst : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] [inst_1 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)],
  Topology.IsInducing fun p => (⟨p.proj, p.snd.1⟩, ⟨p.proj, p.snd.2⟩)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km fallback : α}, t.minKey? = some km → t.getKeyD km fallback = km
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntThms.mk : Option Lean.Expr → Option Lean.Expr → Option Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntThms
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.HasFiniteIntegral.congr'_enorm : ∀ {α : Type u_1} {ε : Type u_4} {ε' : Type u_5} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  [inst_1 : ENorm ε'] {f : α → ε} {g : α → ε'},
  MeasureTheory.HasFiniteIntegral f μ → (∀ᵐ (a : α) ∂μ, ‖f a‖ₑ = ‖g a‖ₑ) → MeasureTheory.HasFiniteIntegral g μ
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitEpi.splitMono.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (se : CategoryTheory.SplitEpi f),
  se.splitMono = { retraction := f, id := ⋯ }
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_pow : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (e : M ≃ₗ[R] M)
  (n : ℕ), ⇑(e ^ n) = (⇑e)^[n]
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
/-- The sum to be bounded (`ℕ` version).  -/
HurwitzKernelBounds.F_nat : ℕ → ℝ → ℝ → ℝ
-- Mathlib.Data.Int.ModEq
/-- `a ≡ b [ZMOD n]` when `a % n = b % n`.  -/
«term_≡_[ZMOD_]» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.Jacobson.Ideal
/-- An ideal `I` equals its Jacobson radical if and only if every element outside `I`
also lies outside of a maximal ideal containing `I`.  -/
Ideal.eq_jacobson_iff_notMem : ∀ {R : Type u} [inst : Ring R] {I : Ideal R}, I.jacobson = I ↔ ∀ x ∉ I, ∃ M, (I ≤ M ∧ M.IsMaximal) ∧ x ∉ M
-- Mathlib.Algebra.Homology.HomotopyFiber
HomologicalComplex.pathObject.mapHomologicalComplexObjIso_inv_map_π₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {α : Type u_2}
  {c : ComplexShape α} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasPathObject]
  {D : Type u_3} [inst_5 : CategoryTheory.Category.{v_2, u_3} D] [inst_6 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_7 : H.Additive]
  [inst_8 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj K).X i)
        (((H.mapHomologicalComplex c).obj K).X i)]
  [inst_9 : ((H.mapHomologicalComplex c).obj K).HasPathObject]
  [inst_10 :
    ∀ (i : α),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)
        (((H.op.mapHomologicalComplex c.symm).obj K.op).X i)]
  [inst_11 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift
        (CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op))
        (-CategoryTheory.CategoryStruct.id ((H.op.mapHomologicalComplex c.symm).obj K.op)))]
  [inst_12 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.op.mapHomologicalComplex c.symm).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K.op)
          (-CategoryTheory.CategoryStruct.id K.op)))]
  [inst_13 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.op.X i) (K.op.X i)]
  (hc : ∀ (i : α), ∃ j, c.Rel i j),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.pathObject.mapHomologicalComplexObjIso K H hc).inv
      ((H.mapHomologicalComplex c).map (HomologicalComplex.pathObject.π₀ K)) =
    HomologicalComplex.pathObject.π₀ ((H.mapHomologicalComplex c).obj K)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.exists_of_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {x y : M}, f x = f y → ∃ c, ↑c * x = ↑c * y
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.apply_mulSingle : ∀ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} [inst : (i : ι) → One (M i)] [inst_1 : (i : ι) → One (N i)]
  [inst_2 : DecidableEq ι] (f' : (i : ι) → M i → N i),
  (∀ (i : ι), f' i 1 = 1) → ∀ (i : ι) (x : M i) (j : ι), f' j (Pi.mulSingle i x j) = Pi.mulSingle i (f' i x) j
-- Mathlib.AlgebraicTopology.ModelCategory.DerivabilityStructureFibrant
HomotopicalAlgebra.FibrantObject.instWeakEquivalenceWWeakEquivalences : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X : C}
  (R : (HomotopicalAlgebra.FibrantObject.localizerMorphism C).RightResolution X), HomotopicalAlgebra.WeakEquivalence R.w
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- If `G` preserves terminal objects, then the terminal comparison map for `G` is an isomorphism.
 -/
CategoryTheory.Limits.PreservesTerminal.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasTerminal D] →
              [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G] → G.obj (⊤_ C) ≅ ⊤_ D
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigOWith.prod_left_fst : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} {G' : Type u_8} [inst : SeminormedAddCommGroup E']
  [inst_1 : SeminormedAddCommGroup F'] [inst_2 : SeminormedAddCommGroup G'] {c : ℝ} {f' : α → E'} {g' : α → F'}
  {k' : α → G'} {l : Filter α}, Asymptotics.IsBigOWith c l (fun x => (f' x, g' x)) k' → Asymptotics.IsBigOWith c l f' k'
-- Init.Data.SInt.Lemmas
ISize.toInt_minValue_le : ISize.minValue.toInt ≤ -2 ^ 31
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdx?.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → ℕ → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (x_1 : ℕ) (h_1 : (x : ℕ) → motive Std.DTreeMap.Internal.Impl.leaf x)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (n : ℕ) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n)
  (x_2 : ℕ),
  x = Std.DTreeMap.Internal.Impl.leaf →
    x_1 = x_2 →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, x => h_1 x
        | Std.DTreeMap.Internal.Impl.inner size k v l r, n => h_2 size k v l r n) ≍
        h_1 x_2
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.mul_vlt_mul_iff_left : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ z → (x * z <ᵥ y * z ↔ x <ᵥ y)
-- Mathlib.Order.Filter.Pointwise
Filter.smul_filter_le_smul_filter : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {f₁ f₂ : Filter β} {a : α}, f₁ ≤ f₂ → a • f₁ ≤ a • f₂
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.star_zero : star 0 = 0
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.Semiring.mk.sizeOf_spec : ∀ (id : ℕ) (type : Lean.Expr) (u : Lean.Level) (semiringInst : Lean.Expr)
  (addFn? mulFn? powFn? natCastFn? : Option Lean.Expr)
  (denote : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.Arith.CommRing.SemiringExpr)
  (vars : Lean.PArray Lean.Expr) (varMap : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.CommRing.Var),
  sizeOf
      { id := id, type := type, u := u, semiringInst := semiringInst, addFn? := addFn?, mulFn? := mulFn?,
        powFn? := powFn?, natCastFn? := natCastFn?, denote := denote, vars := vars, varMap := varMap } =
    1 + sizeOf id + sizeOf type + sizeOf u + sizeOf semiringInst + sizeOf addFn? + sizeOf mulFn? + sizeOf powFn? +
            sizeOf natCastFn? +
          sizeOf denote +
        sizeOf vars +
      sizeOf varMap
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} {comon : CategoryTheory.ComonObj X}
  {comm : CategoryTheory.IsCommComonObj X} {X_1 : C} {comon_1 : CategoryTheory.ComonObj X_1}
  {comm_1 : CategoryTheory.IsCommComonObj X_1},
  { X := X, comon := comon, comm := comm } = { X := X_1, comon := comon_1, comm := comm_1 } → X = X_1 ∧ comon ≍ comon_1
-- Mathlib.Topology.UnitInterval
unitInterval.coe_symm_eq : ∀ (x : ↑unitInterval), ↑(unitInterval.symm x) = 1 - ↑x
-- Init.Data.List.Lemmas
List.getElem_eq_getD : ∀ {α : Type u_1} {l : List α} {i : ℕ} {h : i < l.length} (fallback : α), l[i] = l.getD i fallback
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Rank
/-- The weak rank function attached to a rank function.  -/
SSet.Subcomplex.Pairing.RankFunction.toWeakRankFunction : {X : SSet} →
  {A : X.Subcomplex} →
    (P : A.Pairing) → (α : Type v) → [inst : PartialOrder α] → P.RankFunction α → P.WeakRankFunction α
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset.eq_1 : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (α : Type w)
  [inst_1 : CategoryTheory.Limits.HasFiniteProducts C],
  CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinset C α =
    { obj := CategoryTheory.Limits.ProductsFromFiniteCofiltered.liftToFinsetObj,
      map := fun {X Y} β => { app := fun x => CategoryTheory.Limits.Pi.map fun x_1 => β.app ↑x_1, naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_insertListIfNewUnitₘ : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {l : List α},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.Const.insertListIfNewUnitₘ m l)).buckets).Perm
      (Std.Internal.List.insertListIfNewUnit (Std.DHashMap.Internal.toListModel (↑m).buckets) l)
-- Mathlib.Data.Finset.Insert
Finset.ssubset_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∉ s → s ⊂ insert a s
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDefinitionParams.toJson : Lean.Lsp.DefinitionParams → Lean.Json
-- Mathlib.Analysis.Complex.Trigonometric
Real.cos_pos_of_le_one : ∀ {x : ℝ}, |x| ≤ 1 → 0 < Real.cos x
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.constantCoeff.eq_def : ∀ {R : Type u_1} [inst : Semiring R], PowerSeries.constantCoeff = MvPowerSeries.constantCoeff
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.corecF_eq : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : β → F (α ::: β))
  (x : β),
  MvPFunctor.M.dest (MvQPF.P F) (MvQPF.corecF g x) = MvFunctor.map (TypeVec.id ::: MvQPF.corecF g) (MvQPF.repr (g x))
-- Init.Util
dbgTraceVal : {α : Type u} → [ToString α] → α → α
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel_eq : ∀ {Ω : Type u_1} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω)
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] [h : Nonempty Ω] (m : MeasurableSpace Ω),
  ProbabilityTheory.condExpKernel μ m = (ProbabilityTheory.condDistrib id id μ).comap id ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- A coproduct over coproducts is a coproduct indexed by a product.  -/
CategoryTheory.Limits.Cofan.IsColimit.prod : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {ι' : Type u_2} →
        {X : ι → ι' → C} →
          (c : (i : ι) → CategoryTheory.Limits.Cofan fun j => X i j) →
            ((i : ι) → CategoryTheory.Limits.IsColimit (c i)) →
              (c' : CategoryTheory.Limits.Cofan fun i => (c i).pt) →
                CategoryTheory.Limits.IsColimit c' →
                  CategoryTheory.Limits.IsColimit
                    (CategoryTheory.Limits.Cofan.mk c'.pt fun p =>
                      CategoryTheory.CategoryStruct.comp ((c p.1).inj p.2) (c'.inj p.1))
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {fallback : α}, t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.ConstructibleSetData.toSet_map : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S)
  (s : PrimeSpectrum.ConstructibleSetData R),
  (PrimeSpectrum.ConstructibleSetData.map f s).toSet = PrimeSpectrum.comap f ⁻¹' s.toSet
-- Mathlib.Topology.Order
instIndiscreteTopology : ∀ {α : Type u_1}, IndiscreteTopology α
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftEq_inv_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (l l' : L₁ ⟶ L₂) (h : l = l')
  (hl :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
      P (CategoryTheory.CategoryStruct.comp (l.app X.left) X.hom))
  (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftEq R l l' h hl).inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.equiv_functor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (V : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {X Y : CategoryTheory.MonoidalCategory.DayFunctor C V} (α : X ⟶ Y),
  (CategoryTheory.MonoidalCategory.DayFunctor.equiv C V).functor.map α = α.natTrans
-- Mathlib.FieldTheory.Galois.Profinite
InfiniteGalois.instCompactSpaceAlgEquivOfIsGalois : ∀ (k : Type u_3) (K : Type u_4) [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K] [IsGalois k K],
  CompactSpace Gal(K/k)
-- Std.Time.Date.ValidDate
_private.Std.Time.Date.ValidDate.0.Std.Time.ValidDate.ofOrdinal.go.eq_def : ∀ {leap : Bool} (ordinal : Std.Time.Day.Ordinal.OfYear leap) (idx : Std.Time.Month.Ordinal) (acc : ℤ)
  (h : ↑ordinal > acc) (p : acc = (Std.Time.Month.Ordinal.cumulativeDays leap idx).val),
  Std.Time.ValidDate.ofOrdinal.go✝ ordinal idx acc h p =
    let monthDays := Std.Time.Month.Ordinal.days leap idx;
    if h₁ : ↑ordinal ≤ acc + ↑monthDays then
      let bounded := (Std.Time.Internal.Bounded.LE.mk ↑ordinal ⋯).sub acc;
      let bounded := Std.Time.Internal.Bounded.cast ⋯ ⋯ bounded;
      let days₁ := ⟨↑bounded, ⋯⟩;
      ⟨(idx, days₁), ⋯⟩
    else
      have h₂ := ⋯;
      have h₃ := ⋯;
      let idx₂ := (Std.Time.Internal.Bounded.LE.truncateTop idx ⋯).addTop 1 Std.Time.ValidDate.ofOrdinal.go._proof_11✝;
      Std.Time.ValidDate.ofOrdinal.go✝ ordinal idx₂ (acc + ↑monthDays) h₂ ⋯
-- Mathlib.Topology.Sets.Compacts
/-- The compacts neighbourhoods of a compact  -/
TopologicalSpace.Compacts.compactNhds : {α : Type u_1} → [inst : TopologicalSpace α] → TopologicalSpace.Compacts α → Set (TopologicalSpace.Compacts α)
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.idem_f_assoc : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C]
  (P : CategoryTheory.Idempotents.Karoubi (CategoryTheory.Idempotents.Karoubi C)) {Z : C} (h : P.X.X ⟶ Z),
  CategoryTheory.CategoryStruct.comp P.p.f (CategoryTheory.CategoryStruct.comp P.p.f h) =
    CategoryTheory.CategoryStruct.comp P.p.f h
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.rightAdjointUniq_trans_assoc : ∀ {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] {F : CategoryTheory.Functor C D}
  {G G' G'' : CategoryTheory.Functor D C} (adj1 : F ⊣ G) (adj2 : F ⊣ G') (adj3 : F ⊣ G'')
  {Z : CategoryTheory.Functor D C} (h : G'' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (adj1.rightAdjointUniq adj2).hom
      (CategoryTheory.CategoryStruct.comp (adj2.rightAdjointUniq adj3).hom h) =
    CategoryTheory.CategoryStruct.comp (adj1.rightAdjointUniq adj3).hom h
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKeyD_eq_getD_keysArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.minKeyD fallback = t.keysArray.getD 0 fallback
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instInhabited : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Inhabited (Std.ExtDHashMap α β)
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.toLin_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : GL n R) (v : n → R),
  ↑(Matrix.GeneralLinearGroup.toLin A) v = (↑A).mulVecLin v
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_X : ∀ {R : Type u_1} [inst : CommSemiring R] {n : ℕ},
  n ≠ 0 → Polynomial.X.homogenize n = MvPolynomial.X 0 * MvPolynomial.X 1 ^ (n - 1)
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.insert.match_1.splitter : (motive : RBTree.RBColor → Sort u_1) →
  (x : RBTree.RBColor) → (Unit → motive RBTree.RBColor.red) → (Unit → motive RBTree.RBColor.black) → motive x
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
Lex.instMulActionWithZero : {G₀ : Type u_1} →
  {M₀ : Type u_2} →
    [inst : MonoidWithZero G₀] → [inst_1 : AddMonoid M₀] → [MulActionWithZero G₀ M₀] → MulActionWithZero (Lex G₀) M₀
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.DiagnosticRelatedInformation.mk : Lean.Lsp.Location → String → Lean.Lsp.DiagnosticRelatedInformation
-- Mathlib.Order.OrderDual
OrderDual.toDual_trans_ofDual : ∀ {α : Type u_1}, OrderDual.toDual.trans OrderDual.ofDual = Equiv.refl α
-- Mathlib.Algebra.Group.Basic
zero_sub_zero : ∀ {G : Type u_3} [inst : SubNegZeroMonoid G], 0 - 0 = 0
-- Mathlib.Topology.Order.LocalExtr
/-- If `f` is monotone to the left and antitone to the right, then it has a local maximum.  -/
isLocalMax_of_mono_anti' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {β : Type u_2} [inst_2 : Preorder β] {b : α}
  {f : α → β} {a : Set α},
  a ∈ nhdsWithin b (Set.Iic b) →
    ∀ {c : Set α}, c ∈ nhdsWithin b (Set.Ici b) → MonotoneOn f a → AntitoneOn f c → IsLocalMax f b
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.self_le_max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (cmp k (t.insert k).max!).isLE = true
-- Mathlib.Algebra.Group.Invertible.Defs
Invertible.subsingleton : ∀ {α : Type u} [inst : Monoid α] (a : α), Subsingleton (Invertible a)