mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Y' Z' X' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'}
  [inst_2 : CategoryTheory.ChosenPullbacksAlong g'] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X}
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_snd._auto_3)
  {Z_1 : C} (h : Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd f g) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd f' g')
      (CategoryTheory.CategoryStruct.comp γ₂ h)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- An `AddSubmonoid` is either the trivial `AddSubmonoid` or nontrivial.  -/
AddSubmonoid.bot_or_nontrivial : ∀ {M : Type u_1} [inst : AddZeroClass M] (S : AddSubmonoid M), S = ⊥ ∨ Nontrivial ↥S
-- Mathlib.Data.List.Rotate
List.IsRotated.cyclicPermutations : ∀ {α : Type u} {l l' : List α}, l ~r l' → l.cyclicPermutations ~r l'.cyclicPermutations
-- Mathlib.LinearAlgebra.Matrix.SchurComplement
/-- Alternate statement of the **Weinstein–Aronszajn identity**  -/
Matrix.det_mul_add_one_comm : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_4} [inst : Fintype m] [inst_1 : Fintype n] [inst_2 : DecidableEq m]
  [inst_3 : DecidableEq n] [inst_4 : CommRing α] (A : Matrix m n α) (B : Matrix n m α),
  (A * B + 1).det = (B * A + 1).det
-- Lean.Meta.DiscrTree.Main
_private.Lean.Meta.DiscrTree.Main.0.Lean.Meta.DiscrTree.toNatLit? : Lean.Expr → Option Lean.Literal
-- Aesop.Check
Aesop.Check.all : Lean.Option Bool
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.toArray_eq_if_roc : ∀ {α : Type u} {r : Std.Ric α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxc.IsAlwaysFinite α],
  r.toArray =
    have init := Std.PRange.UpwardEnumerable.least;
    if init ≤ r.upper then #[init] ++ (init<...=r.upper).toArray else #[]
-- Mathlib.Data.Fintype.Card
Fintype.card_congr' : ∀ {α β : Type u_4} [inst : Fintype α] [inst_1 : Fintype β], α = β → Fintype.card α = Fintype.card β
-- Mathlib.Analysis.Normed.Group.Pointwise
div_ball : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (s : Set E) (x : E),
  s / Metric.ball x δ = x⁻¹ • Metric.thickening δ s
-- Mathlib.Topology.UniformSpace.Defs
UniformSpace.mem_ball_self : ∀ {α : Type ua} [inst : UniformSpace α] (x : α) {V : SetRel α α}, V ∈ uniformity α → x ∈ UniformSpace.ball x V
-- Lean.DocString.Types
Lean.Doc.Inline.other.injEq : ∀ {i : Type u} (container : i) (content : Array (Lean.Doc.Inline i)) (container_1 : i)
  (content_1 : Array (Lean.Doc.Inline i)),
  (Lean.Doc.Inline.other container content = Lean.Doc.Inline.other container_1 content_1) =
    (container = container_1 ∧ content = content_1)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.diag.eq_1 : ∀ (A : Type u_2) [inst : Monoid A] [inst_1 : TopologicalSpace A],
  ContinuousMonoidHom.diag A = (ContinuousMonoidHom.id A).prod (ContinuousMonoidHom.id A)
-- Mathlib.CategoryTheory.Generator.StrongGenerator
CategoryTheory.ObjectProperty.IsStrongGenerator.exists_of_mono_not_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C},
  P.IsStrongGenerator →
    ∀ {X Y : C} (i : X ⟶ Y) [CategoryTheory.Mono i],
      ¬CategoryTheory.IsIso i → ∃ G, ∃ (_ : P G), ∃ g, ∀ (f : G ⟶ X), CategoryTheory.CategoryStruct.comp f i ≠ g
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_succ_eq_push : ∀ {n : ℕ}, (*...=n + 1).toArray = (*...=n).toArray.push (n + 1)
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Prequotient.add.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat} [inst_1 : SizeOf J]
  (a a_1 : CommRingCat.Colimits.Prequotient F), sizeOf (a.add a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.RingTheory.Spectrum.Prime.Polynomial
MvPolynomial.image_comap_C_basicOpen : ∀ {R : Type u_2} [inst : CommRing R] {σ : Type u_1} (f : MvPolynomial σ R),
  PrimeSpectrum.comap MvPolynomial.C '' ↑(PrimeSpectrum.basicOpen f) =
    (PrimeSpectrum.zeroLocus (Set.range fun m => MvPolynomial.coeff m f))ᶜ
-- Lean.Elab.Do.Legacy
/-- Extending code blocks with reassignments: `x : t := v` and `x : t ← v`.
Remark: `stx` is the syntax for the declaration (e.g., `letDecl`), and `xs` are the variables
declared by it. It is an array because we have let-declarations that declare multiple variables.
Example: `(x, y) ← t`
 -/
Lean.Elab.Term.Do.mkReassignCore : Array Lean.Elab.Term.Do.Var →
  Lean.Syntax → Lean.Elab.Term.Do.CodeBlock → Lean.Elab.TermElabM Lean.Elab.Term.Do.CodeBlock
-- Mathlib.Algebra.Ring.CentroidHom
/-- Commutativity of centroid homomorphisms with left multiplication.  -/
CentroidHomClass.map_mul_left : ∀ {F : Type u_6} {α : outParam (Type u_7)} {inst : NonUnitalNonAssocSemiring α} {inst_1 : FunLike F α α}
  [self : CentroidHomClass F α] (f : F) (a b : α), f (a * b) = a * f b
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The pullback of a presieve `R` on `Y` along a morphism `f : X ⟶ Y` is the presieve on `X`
given by all morphisms `g : Z ⟶ X` such that `g ≫ f` is in `R`.  -/
CategoryTheory.Presieve.pullback : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → (X ⟶ Y) → CategoryTheory.Presieve Y → CategoryTheory.Presieve X
-- Mathlib.CategoryTheory.Action.Limits
Action.instReflectsLimitsOfShapeForget : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {J : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_2, u_3} J], CategoryTheory.Limits.ReflectsLimitsOfShape J (Action.forget V G)
-- Mathlib.RingTheory.Coalgebra.Basic
/-- The `R`-module whose elements are functions `Π i, A i` for finite `n` has a coalgebra structure.
The coproduct `Δ` is given by `Δ(fᵢ a) = fᵢ a₁ ⊗ fᵢ a₂` where `Δ(a) = a₁ ⊗ a₂` and
the counit `ε` by `ε(fᵢ a) = ε(a)`, where `fᵢ a` is the function sending `i` to `a` and all
other elements of `ι` to zero.  -/
Pi.instCoalgebra : {R : Type u_1} →
  {n : Type u_2} →
    [inst : CommSemiring R] →
      [Fintype n] →
        [DecidableEq n] →
          {A : n → Type u_3} →
            [inst_3 : (i : n) → AddCommMonoid (A i)] →
              [inst_4 : (i : n) → Module R (A i)] → [(i : n) → Coalgebra R (A i)] → Coalgebra R ((i : n) → A i)
-- Mathlib.RingTheory.Localization.Pi
IsLocalization.surjective_piRingHom_algebraMap_comp_piEvalRingHom : ∀ {ι : Type u_1} {R : ι → Type u_2} (S : ι → Type u_3) [inst : (i : ι) → CommSemiring (R i)]
  [inst_1 : (i : ι) → CommSemiring (S i)] [inst_2 : (i : ι) → Algebra (R i) (S i)] (M : Submonoid ((i : ι) → R i))
  [∀ (i : ι), IsLocalization (Submonoid.map (Pi.evalRingHom R i) M) (S i)] [∀ (i : ι), Ring.KrullDimLE 0 (R i)]
  [∀ (i : ι), IsLocalRing (R i)],
  Function.Surjective ⇑(RingHom.pi fun i => (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i))
-- Mathlib.RingTheory.MvPowerSeries.Equiv
MvPowerSeries.toAdicCompletion_apply_eq_mk_truncTotal : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : Finite σ] {n : ℕ} {p : MvPowerSeries σ R},
  ↑((MvPowerSeries.toAdicCompletion σ R) p) n =
    (Ideal.Quotient.mk (MvPolynomial.idealOfVars σ R ^ n • ⊤)) ((MvPowerSeries.truncTotal n) p)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α],
  (↑m).WF →
    ∀ {l : List (α × β)} {k : α},
      (List.map Prod.fst l).contains k = false →
        (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany m l)).getKey! k = m.getKey! k
-- Init.Omega.Constraint
Lean.Omega.Constraint.div_sat : ∀ (c : Lean.Omega.Constraint) (t : ℤ) (k : ℕ), k ≠ 0 → ↑k ∣ t → c.sat t = true → (c.div k).sat (t / ↑k) = true
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.isEmptyRingEquiv_symm_apply : ∀ (R : Type u) (σ : Type u_1) [inst : CommSemiring R] [inst_1 : IsEmpty σ] (r : R),
  (MvPolynomial.isEmptyRingEquiv R σ).symm r = MvPolynomial.C r
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.toList.eq_def : ∀ {α : Type u} {β : α → Type v} (x : Std.DHashMap.Internal.AssocList α β),
  x.toList =
    match x with
    | Std.DHashMap.Internal.AssocList.nil => []
    | Std.DHashMap.Internal.AssocList.cons a b es => ⟨a, b⟩ :: es.toList
-- Init.Data.SInt.Lemmas
Int8.toInt8_toInt16 : ∀ (n : Int8), n.toInt16.toInt8 = n
-- Mathlib.Algebra.Order.Archimedean.Class
/-- A closed ball defined by `MulArchimedeanClass.subgroup` of `UpperSet.Ici c`.  -/
MulArchimedeanClass.closedBallSubgroup : {M : Type u_1} →
  [inst : CommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → MulArchimedeanClass M → Subgroup M
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.simplex_fst_castSucc : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d} {l : Fin d},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ → (x.cast hd).simplex.1 l.castSucc = k.castSucc
-- Mathlib.Analysis.SpecialFunctions.Exp
Filter.Tendsto.rexp : ∀ {α : Type u_1} {l : Filter α} {f : α → ℝ} {z : ℝ},
  Filter.Tendsto f l (nhds z) → Filter.Tendsto (fun x => Real.exp (f x)) l (nhds (Real.exp z))
-- Mathlib.Order.BourbakiWitt
instPartialOrderNonemptyChain : {α : Type u_4} → [inst : LE α] → PartialOrder (NonemptyChain α)
-- Mathlib.Topology.Bornology.Basic
/-- `IsBounded` is the predicate that `s` is bounded relative to the ambient bornology on `α`.  -/
Bornology.IsBounded : {α : Type u_2} → [Bornology α] → Set α → Prop
-- Mathlib.Order.Interval.Multiset
Multiset.Ico_inter_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] {a b c d : α},
  Multiset.Ico a b ∩ Multiset.Ico c d = Multiset.Ico (max a c) (min b d)
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.smulTower'_apply : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid A]
  [inst_3 : Module R S] [inst_4 : Module S A] [inst_5 : Module R A] [inst_6 : IsScalarTower R S A] {ι : Type u_5}
  {ι' : Type u_6} (b : Module.Basis ι R S) (c : Module.Basis ι' S A) (ij : ι' × ι),
  (b.smulTower' c) ij = b ij.2 • c ij.1
-- Mathlib.CategoryTheory.Sites.SheafOfTypes
CategoryTheory.Presieve.IsSheaf.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type w)),
  CategoryTheory.Presieve.IsSheaf J P = ∀ ⦃X : C⦄, ∀ S ∈ J X, CategoryTheory.Presieve.IsSheafFor P S.arrows
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Module.FaithfullyFlat.iff_flat_and_rTensor_reflects_triviality : ∀ (R : Type u) (M : Type v) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.FaithfullyFlat R M ↔
    Module.Flat R M ∧
      ∀ (N : Type (max u v)) [inst_3 : AddCommGroup N] [inst_4 : Module R N],
        Subsingleton (TensorProduct R N M) → Subsingleton N
-- Std.Http.Data.Status
Std.Http.Status.gone.sizeOf_spec : sizeOf Std.Http.Status.gone = 1
-- Mathlib.NumberTheory.ModularForms.SlashActions
ModularForm.SL_smul_slash : ∀ {α : Type u_1} [inst : SMul α ℂ] [IsScalarTower α ℂ ℂ] (k : ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ)
  (f : UpperHalfPlane → ℂ) (c : α), SlashAction.map k A (c • f) = c • SlashAction.map k A f
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.algebraMap₀_eq_smul_one : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (r : R),
  TensorPower.algebraMap₀ r = r • GradedMonoid.GOne.one
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_apply' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.SFinite μ] (f : α → ENNReal)
  (s : Set α), (μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instPartialOrder : {E : Type u_3} → [inst : AddGroup E] → PartialOrder (AddGroupSeminorm E)
-- Mathlib.Data.List.Rotate
List.rotate'_length_mul : ∀ {α : Type u} (l : List α) (n : ℕ), l.rotate' (l.length * n) = l
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
FiniteDimensional.finiteDimensional_subalgebra : ∀ {F : Type u_1} {E : Type u_2} [inst : Field F] [inst_1 : Ring E] [inst_2 : Algebra F E] [FiniteDimensional F E]
  (S : Subalgebra F E), FiniteDimensional F ↥S
-- Std.Internal.Do.Order.Heyting
/-- Heyting implication: the upper adjoint of the lattice meet. For `Prop` it is `→`.  -/
Lean.Order.himp : {α : Type u} → [Lean.Order.CompleteLattice α] → α → α → α
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minEntry!.eq_3 : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α)
  (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).minEntry! =
    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minEntry!
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.IsNonloop.eRk_eq : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e → M.eRk {e} = 1
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_isoPushout_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr)
  [inst_2 : CategoryTheory.Limits.HasPushout f g] {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inr)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q hP.isoPushout.hom) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.pushout.inr f g)
-- Mathlib.Combinatorics.Matroid.Closure
/-- **Alias** of `Matroid.Indep.closure_sdiff_ssubset`. -/
Matroid.Indep.closure_diff_ssubset : ∀ {α : Type u_2} {M : Matroid α} {X I : Set α}, M.Indep I → (I ∩ X).Nonempty → M.closure (I \ X) ⊂ M.closure I
-- Init.Data.SInt.Basic
/-- Constructs an `Int8` from an `Int`, clamping if the value is too small or too large.  -/
Int8.ofIntClamp : ℤ → Int8
-- Mathlib.AlgebraicGeometry.Morphisms.AffineAnd
AlgebraicGeometry.targetAffineLocally_affineAnd_iff_affineLocally : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] => Q) →
    ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
      AlgebraicGeometry.targetAffineLocally (AlgebraicGeometry.affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f ↔
        AlgebraicGeometry.IsAffineHom f ∧ AlgebraicGeometry.affineLocally (fun {R S} [CommRing R] [CommRing S] => Q) f
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncLE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C), t.IsLE ((t.truncLE n).obj X) n
-- Mathlib.Algebra.Module.Torsion.Free
instIsTorsionFree : ∀ {R : Type u_1} [inst : Semiring R], Module.IsTorsionFree R R
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂.brecOn.eq : ∀ {motive : Mathlib.Tactic.BicategoryLike.Mor₂ → Sort u} (t : Mathlib.Tactic.BicategoryLike.Mor₂)
  (F_1 : (t : Mathlib.Tactic.BicategoryLike.Mor₂) → Mathlib.Tactic.BicategoryLike.Mor₂.below t → motive t),
  Mathlib.Tactic.BicategoryLike.Mor₂.brecOn t F_1 = F_1 t (Mathlib.Tactic.BicategoryLike.Mor₂.brecOn.go t F_1).2
-- Mathlib.CategoryTheory.Limits.VanKampen
CategoryTheory.IsUniversalColimit.of_iso : ∀ {J : Type v'} [inst : CategoryTheory.Category.{u', v'} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F},
  CategoryTheory.IsUniversalColimit c → ∀ (e : c ≅ c'), CategoryTheory.IsUniversalColimit c'
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.gcd_mono_fun : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f g : β → α}, (∀ b ∈ s, f b ∣ g b) → s.gcd f ∣ s.gcd g
-- Lean.Util.FoldConsts
Lean.Expr.FoldConstsImpl.State.visitedConsts : Lean.Expr.FoldConstsImpl.State → Lean.NameHashSet
-- Mathlib.Order.Directed
directed_comp : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {ι : Sort u_5} {f : ι → β} {g : β → α},
  Directed r (g ∘ f) ↔ Directed (g ⁻¹'o r) f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_sub_pi : ∀ (θ : Real.Angle), (θ - ↑Real.pi).cos = -θ.cos
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_top_left_eq_bot_iff_le_center : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ⁅⊤, H⁆ = ⊥ ↔ H ≤ AddSubgroup.center G
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_union_of_contains_eq_false_left : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k m₁ = false →
    Std.DTreeMap.Internal.Impl.Const.get! (m₁.union m₂ ⋯ ⋯) k = Std.DTreeMap.Internal.Impl.Const.get! m₂ k
-- Mathlib.Data.FinEnum
_private.Mathlib.Data.FinEnum.0.FinEnum.Finset.enum.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((x : α) → (xs : List α) → motive (x :: xs)) → motive x
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.whiskerRight_comp_unit_app : ∀ {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]
  (F G : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolution F G] {x x' : C} (y : C)
  (f : x ⟶ x'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (G.obj y))
      ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x', y)) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (x, y))
      ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f y))
-- Mathlib.Data.Multiset.ZeroCons
Multiset.rel_cons_left : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {a : α} {as : Multiset α} {bs : Multiset β},
  Multiset.Rel r (a ::ₘ as) bs ↔ ∃ b bs', r a b ∧ Multiset.Rel r as bs' ∧ bs = b ::ₘ bs'
-- Init.Data.List.MinMaxIdx
List.maxIdxOn?_nil : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β}, List.maxIdxOn? f [] = none
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {n : ℕ} (m k : ℕ)
  (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n) {T : Type u_4} [inst_3 : CommRing T] [inst_4 : Algebra R T]
  (f : Polynomial.UniversalCoprimeFactorizationRing m k hn p →ₐ[R] S) (g : S →ₐ[R] T),
  (↑((Polynomial.UniversalCoprimeFactorizationRing.homEquiv T m k hn p) (g.comp f))).2 =
    (↑((Polynomial.UniversalCoprimeFactorizationRing.homEquiv S m k hn p) f)).2.map ↑g
-- Mathlib.Algebra.Order.Nonneg.Floor
Nonneg.nat_floor_coe : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedRing α] [inst_3 : FloorSemiring α]
  (a : { r // 0 ≤ r }), ⌊↑a⌋₊ = ⌊a⌋₊
-- Aesop.Search.Queue
Aesop.LIFOQueue.addGoals : Aesop.LIFOQueue → Array Aesop.GoalRef → Aesop.LIFOQueue
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.setCurr : ∀ {l : List Char} {c : Char} {r : List Char} {it : String.Legacy.Iterator},
  String.Legacy.Iterator.ValidFor l (c :: r) it → String.Legacy.Iterator.ValidFor l (c :: r) (it.setCurr c)
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- `secondInter` is unchanged by negating the vector.  -/
EuclideanGeometry.Sphere.secondInter_neg : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P) (v : V),
  s.secondInter p (-v) = s.secondInter p v
-- Mathlib.Algebra.Group.Action.Defs
SemigroupAction.ext : ∀ {α : Type u_9} {β : Type u_10} {inst : Semigroup α} {x y : SemigroupAction α β}, SMul.smul = SMul.smul → x = y
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_inv_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C) (hT₁ : T₁ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles)
  (hT₂ : T₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles) (e₁ : T₁.obj₁ ≅ T₂.obj₁) (e₂ : T₁.obj₂ ≅ T₂.obj₂)
  (comm : CategoryTheory.CategoryStruct.comp T₁.mor₁ e₂.hom = CategoryTheory.CategoryStruct.comp e₁.hom T₂.mor₁),
  (CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂ T₁ T₂ hT₁ hT₂ e₁ e₂ comm).inv.hom₁ = e₁.inv
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.WalkingParallelFamily.instDecidableEqHom.decEq : {J : Type u_1} →
  {a a_1 : CategoryTheory.Limits.WalkingParallelFamily J} →
    [DecidableEq J] → (x x_1 : CategoryTheory.Limits.WalkingParallelFamily.Hom J a a_1) → Decidable (x = x_1)
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.IsComplex.cokerToKer'.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.IsComplex) (k : ℕ) (hk : k ≤ n)
  (cc : CategoryTheory.Limits.CokernelCofork (S.map' k (k + 1) ⋯ ⋯))
  (kf : CategoryTheory.Limits.KernelFork (S.map' (k + 2) (k + 3) ⋯ ⋯)) (hcc : CategoryTheory.Limits.IsColimit cc)
  (hkf : CategoryTheory.Limits.IsLimit kf),
  hS.cokerToKer' k hk cc kf hcc hkf =
    hcc.desc
      (CategoryTheory.Limits.CokernelCofork.ofπ
        (hkf.lift (CategoryTheory.Limits.KernelFork.ofι (S.map' (k + 1) (k + 1 + 1) ⋯ ⋯) ⋯)) ⋯)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
IsBoundedBilinearMap.toContinuousLinearMap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E × F → G}
  (hf : IsBoundedBilinearMap 𝕜 f) (x : E) (y : F), (hf.toContinuousLinearMap x) y = f (x, y)
-- Init.Data.Fin.Basic
Fin.instShiftLeft : {n : ℕ} → ShiftLeft (Fin n)
-- Init.Data.Int.DivMod.Lemmas
Int.sub_emod_right : ∀ (a b : ℤ), (a - b) % b = a % b