mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.sectL_prodMkLeft : ∀ {β : Type u_2} {mβ : MeasurableSpace β} {γ : Type u_4} {mγ : MeasurableSpace γ} (α : Type u_6)
  [inst : MeasurableSpace α] (κ : ProbabilityTheory.Kernel β γ) (a : α) {b : β},
  ((ProbabilityTheory.Kernel.prodMkLeft α κ).sectL b) a = κ b
-- Lean.Meta.Tactic.Simp.Arith.Int.Basic
Lean.Meta.Simp.Arith.Int.instToExprExpr : Lean.ToExpr Int.Internal.Linear.Expr
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSubtractionMonoid.eq_1 : ∀ {α : Type u_1} [inst : SubtractionMonoid α],
  Colex.instSubtractionMonoid =
    { toSubNegMonoid := Colex.instSubNegAddMonoid, neg_neg := ⋯, neg_add_rev := ⋯, neg_eq_of_add := ⋯ }
-- Mathlib.CategoryTheory.Comma.CardinalArrow
CategoryTheory.hasCardinalLT_arrow_discrete_iff : ∀ {X : Type u} (κ : Cardinal.{w}),
  HasCardinalLT (CategoryTheory.Arrow (CategoryTheory.Discrete X)) κ ↔ HasCardinalLT X κ
-- Mathlib.Data.Int.ModEq
Int.ModEq.of_mul_left : ∀ {n a b : ℤ} (m : ℤ), a ≡ b [ZMOD m * n] → a ≡ b [ZMOD n]
-- Mathlib.Data.Matrix.Mul
Matrix.zero_vecMulVec : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : MulZeroClass α] (v : n → α), Matrix.vecMulVec 0 v = 0
-- Mathlib.Geometry.Manifold.Instances.Sphere
/-- The unit circle in `ℂ` is a charted space modelled on `EuclideanSpace ℝ (Fin 1)`.  This
follows by definition from the corresponding result for `Metric.Sphere`.  -/
instChartedSpaceEuclideanSpaceRealFinOfNatNatCircle : ChartedSpace (EuclideanSpace ℝ (Fin 1)) Circle
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
/-- If `C` has strict initial objects and there is a commutative square `Xᵢ ← Z → Xⱼ`
over `∐ X`, then `Z` is initial.  -/
CategoryTheory.Limits.IsInitial.ofCoproductDisjointOfCommSq : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : ι → C} →
        [CategoryTheory.Limits.CoproductDisjoint X] →
          {i j : ι} →
            i ≠ j →
              [CategoryTheory.Limits.HasStrictInitialObjects C] →
                {c : CategoryTheory.Limits.Cofan X} →
                  CategoryTheory.Limits.IsColimit c →
                    {Z : C} →
                      (fst : Z ⟶ X i) →
                        (snd : Z ⟶ X j) →
                          CategoryTheory.CategoryStruct.comp fst (c.inj i) =
                              CategoryTheory.CategoryStruct.comp snd (c.inj j) →
                            [CategoryTheory.Limits.HasPullback (c.inj i) (c.inj j)] → CategoryTheory.Limits.IsInitial Z
-- Mathlib.Algebra.Homology.Embedding.TruncLEHomology
HomologicalComplex.Acyclic.truncLE : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : HomologicalComplex C c'} [inst_2 : ∀ (i' : ι'), K.HasHomology i']
  [inst_3 : CategoryTheory.Limits.HasZeroObject C],
  K.Acyclic → ∀ (e : c.Embedding c') [inst_4 : e.IsTruncLE], (K.truncLE e).Acyclic
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.succ : Turing.PartrecToTM2.Λ' → Turing.PartrecToTM2.Λ'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.inr_inl_pushoutLeftPushoutInrIso_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g' : Z ⟶ W)
  [inst_1 : CategoryTheory.Limits.HasPushout f g]
  [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushout.inr f g) g')
        (CategoryTheory.Limits.pushoutLeftPushoutInrIso f g g').hom) =
    CategoryTheory.CategoryStruct.comp g'
      (CategoryTheory.Limits.pushout.inr f (CategoryTheory.CategoryStruct.comp g g'))
-- Mathlib.SetTheory.Descriptive.Tree
Descriptive.Tree.pullSub_mono : ∀ {A : Type u_1} {S : ↥(Descriptive.tree A)} (T : ↥(Descriptive.tree A)),
  S ≤ T → ∀ (x : List A), Descriptive.Tree.pullSub S x ≤ Descriptive.Tree.pullSub T x
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toSquare : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] → J.MayerVietorisSquare → CategoryTheory.Square C
-- Mathlib.Data.Int.Bitwise
/-- `div2 n = n/2`  -/
Int.div2 : ℤ → ℤ
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
/-- The (exact) sequence
`H_i(S.X₁) ⟶ H_i(S.X₂) ⟶ H_i(S.X₃) ⟶ H_j(S.X₁) ⟶ H_j(S.X₂) ⟶ H_j(S.X₃)` when `c.Rel i j`
and `S` is a short exact short complex of homological complexes in an abelian category.  -/
HomologicalComplex.HomologySequence.composableArrows₅ : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        {c : ComplexShape ι} →
          {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)} →
            S₁.ShortExact → (i j : ι) → c.Rel i j → CategoryTheory.ComposableArrows C 5
-- Batteries.Data.List.Basic
/-- Auxiliary for `zipWithLeft'TR`: `zipWithLeft'TR.go l acc = acc.toList ++ zipWithLeft' l`.  -/
List.zipWithLeft'TR.go : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (α → Option β → γ) → List α → List β → Array γ → List γ × List β
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
WithSeminorms.isVonNBounded_iff_seminorm_bounded : ∀ {𝕜 : Type u_2} {E : Type u_6} {ι : Type u_9} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] {p : SeminormFamily 𝕜 E ι} [inst_3 : TopologicalSpace E] {s : Set E},
  WithSeminorms p → (Bornology.IsVonNBounded 𝕜 s ↔ ∀ (i : ι), ∃ r > 0, ∀ x ∈ s, (p i) x < r)
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinOnBall.mk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal},
  r ≤ p.radius →
    0 < r →
      (∀ {y : E}, x + y ∈ insert x s → y ∈ Metric.eball 0 r → HasSum (fun n => (p n) fun x => y) (f (x + y))) →
        HasFPowerSeriesWithinOnBall f p s x r
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
_private.Mathlib.AlgebraicTopology.FundamentalGroupoid.Product.0.FundamentalGroupoidFunctor.prodToProdTop.match_1.eq_1 : ∀ (A : TopCat) (B : TopCat)
  (motive :
    (x y :
        ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A) ×
          ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) →
      (x ⟶ y) → Sort u_3)
  (fst : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A))
  (snd : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B))
  (fst_1 : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A))
  (snd_1 : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) (p₀ : (fst, snd).1 ⟶ (fst_1, snd_1).1)
  (p₁ : (fst, snd).2 ⟶ (fst_1, snd_1).2)
  (h_1 :
    (fst : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)) →
      (snd : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) →
        (fst_2 : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj A)) →
          (snd_2 : ↑(FundamentalGroupoid.fundamentalGroupoidFunctor.obj B)) →
            (p₀ : (fst, snd).1 ⟶ (fst_2, snd_2).1) →
              (p₁ : (fst, snd).2 ⟶ (fst_2, snd_2).2) → motive (fst, snd) (fst_2, snd_2) (p₀, p₁)),
  (match (fst, snd), (fst_1, snd_1), (p₀, p₁) with
    | (fst, snd), (fst_2, snd_2), (p₀, p₁) => h_1 fst snd fst_2 snd_2 p₀ p₁) =
    h_1 fst snd fst_1 snd_1 p₀ p₁
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.free_congr_left : ∀ {α : Type u_4} {β : Type u_5} {γ : Type u_6} {A : SimpleGraph α} {B : SimpleGraph β} {C : SimpleGraph γ}
  (e₁ : A ≃g B), A.Free C ↔ B.Free C
-- Init.Data.SInt.Lemmas
Int64.toInt8_mul : ∀ (a b : Int64), (a * b).toInt8 = a.toInt8 * b.toInt8
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_w_assoc : ∀ {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},
  CategoryTheory.IsPushout f g inl inr →
    ∀ {Q Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q P ⟶ Z_1),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q f)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inl) h) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q g)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inr) h)
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instFibrationPCofibrationsTrivialFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  {X Y : C} (f : X ⟶ Y)
  (h : (HomotopicalAlgebra.cofibrations C).MapFactorizationData (HomotopicalAlgebra.trivialFibrations C) f),
  HomotopicalAlgebra.Fibration h.p
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.toFun_spec' : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (g : L ≃+* L) {n : ℕ} [inst_2 : NeZero n] {t : Lˣ},
  t ∈ rootsOfUnity n L → g ↑t = ↑t ^ (modularCyclotomicCharacter.toFun n g).val
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_add_natCast : ∀ (o : Ordinal.{u_1}), ⨆ n, o + ↑n = o + Ordinal.omega0
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.pullback_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X Y : C}
  (f : Y ⟶ X) (x : CategoryTheory.Subobject X),
  (CategoryTheory.Subobject.pullback f).obj x =
    CategoryTheory.Subobject.mk (CategoryTheory.Limits.pullback.snd x.arrow f)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.inl_normalizationCoprodIso_hom_fromNormalization_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {U V : AlgebraicGeometry.Scheme} {iU : U ⟶ X} {iV : V ⟶ X}
  (e : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk iU iV))
  [inst_2 : AlgebraicGeometry.QuasiCompact iU] [inst_3 : AlgebraicGeometry.QuasiSeparated iU]
  [inst_4 : AlgebraicGeometry.QuasiCompact iV] [inst_5 : AlgebraicGeometry.QuasiSeparated iV]
  {Z : AlgebraicGeometry.Scheme} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationCoprodIso f e).hom
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.fromNormalization f) h)) =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.Hom.fromNormalization (CategoryTheory.CategoryStruct.comp iU f)) h
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.AEEqFun.compMeasurePreserving.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace γ] [inst_2 : MeasurableSpace β] {ν : MeasureTheory.Measure β} (g g_1 : β →ₘ[ν] γ),
  g = g_1 →
    ∀ (f f_1 : α → β) (e_f : f = f_1) (hf : MeasureTheory.MeasurePreserving f μ ν),
      g.compMeasurePreserving f hf = g_1.compMeasurePreserving f_1 ⋯
-- Mathlib.Data.Finset.Lattice.Fold
Finset.ofDual_inf' : ∀ {α : Type u_2} {ι : Type u_5} [inst : SemilatticeSup α] {s : Finset ι} (hs : s.Nonempty) (f : ι → αᵒᵈ),
  OrderDual.ofDual (s.inf' hs f) = s.sup' hs (⇑OrderDual.ofDual ∘ f)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
covariant_le_iff_contravariant_lt : ∀ (M : Type u_1) (N : Type u_2) (μ : M → N → N) [inst : LinearOrder N],
  (Covariant M N μ fun x1 x2 => x1 ≤ x2) ↔ Contravariant M N μ fun x1 x2 => x1 < x2
-- Init.Data.UInt.Bitwise
UInt64.neg_one_and : ∀ {a : UInt64}, -1 &&& a = a
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.mem_inf : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S T : Subalgebra R A}
  {x : A}, x ∈ S ⊓ T ↔ x ∈ S ∧ x ∈ T
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal_map_const_sub : ∀ {μ : ℝ} {v : NNReal} (y : ℝ),
  MeasureTheory.Measure.map (fun x => y - x) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (y - μ) v
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
/-- The set of Liouville numbers has Lebesgue measure zero.  -/
volume_setOfPred_liouville : MeasureTheory.volume {x | Liouville x} = 0
-- Init.Data.Range.Polymorphic.BitVec
BitVec.instRxiIsAlwaysFinite : ∀ {n : ℕ}, Std.Rxi.IsAlwaysFinite (BitVec n)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
/-- The canonical isomorphism
`Triangle.shiftFunctor C n ≅ Triangle.shiftFunctor C a ⋙ Triangle.shiftFunctor C b`
when `a + b = n`.  -/
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
          (a b n : ℤ) →
            a + b = n →
              (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n ≅
                (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C a).comp
                  (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C b))
-- Init.Data.UInt.Bitwise
UInt8.ofFin_or : ∀ (a b : Fin UInt8.size), UInt8.ofFin (a ||| b) = UInt8.ofFin a ||| UInt8.ofFin b
-- Mathlib.Analysis.RCLike.Basic
RCLike.toNormedAlgebra : {K : semiOutParam (Type u_1)} → [self : RCLike K] → NormedAlgebra ℝ K
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidChangeTextDocumentParams.mk.inj : ∀ {textDocument : Lean.Lsp.VersionedTextDocumentIdentifier}
  {contentChanges : Array Lean.Lsp.TextDocumentContentChangeEvent}
  {textDocument_1 : Lean.Lsp.VersionedTextDocumentIdentifier}
  {contentChanges_1 : Array Lean.Lsp.TextDocumentContentChangeEvent},
  { textDocument := textDocument, contentChanges := contentChanges } =
      { textDocument := textDocument_1, contentChanges := contentChanges_1 } →
    textDocument = textDocument_1 ∧ contentChanges = contentChanges_1
-- Init.Data.String.Lemmas.Order
String.Pos.lt_sliceTo_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {q : s.Pos} {h : q ≤ p₀},
  p < p₀.sliceTo q h ↔ String.Pos.ofSliceTo p < q
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.centerToMulOpposite_apply_coe : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (r : ↥(Subsemigroup.center R)),
  ↑(NonUnitalSubsemiring.centerToMulOpposite r) = MulOpposite.op ↑r
-- Mathlib.Data.ZMod.Basic
ZMod.mul_inv_of_unit : ∀ {n : ℕ} (a : ZMod n), IsUnit a → a * a⁻¹ = 1
-- Mathlib.NumberTheory.SmoothNumbers
Nat.mem_smoothNumbersUpTo : ∀ {N k n : ℕ}, n ∈ N.smoothNumbersUpTo k ↔ n ≤ N ∧ n ∈ k.smoothNumbers
-- Mathlib.LinearAlgebra.CliffordAlgebra.Prod
CliffordAlgebra.prodEquiv_symm_apply : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] (Q₁ : QuadraticForm R M₁)
  (Q₂ : QuadraticForm R M₂) (a : GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂)),
  (CliffordAlgebra.prodEquiv Q₁ Q₂).symm a = (CliffordAlgebra.toProd Q₁ Q₂) a
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Subgroup.index_mul_measure : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul G] (H : Subgroup G) [H.FiniteIndex],
  MeasurableSet ↑H → ∀ (μ : MeasureTheory.Measure G) [μ.IsMulLeftInvariant], ↑H.index * μ ↑H = μ Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse_obj_map_fst : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
  {x y : X} (f : x ⟶ y),
  (((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).inverse.obj S).map f).fst = S.fst.map f
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.isoTriangleOfIso₁₂_hom_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).hom.hom₁ = e₁.hom
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.homMk.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : CategoryTheory.Grp C} (f : A.X ⟶ B.X) [inst_2 : CategoryTheory.IsMonHom f],
  CategoryTheory.Grp.homMk f = CategoryTheory.Grp.homMk' { hom := f, isMonHom_hom := inst_2 }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- A variant of `of_is_coproduct` that is more useful with `apply`.  -/
CategoryTheory.IsPushout.of_is_coproduct' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Z X Y P : C} {inl : X ⟶ P} {inr : Y ⟶ P}
  (h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr))
  (t : CategoryTheory.Limits.IsInitial Z), CategoryTheory.IsPushout (t.to X) (t.to Y) inl inr
-- Std.Time.Format.DateFormat
Std.Time.instReprDayPeriodSymbols.repr : Std.Time.DayPeriodSymbols → ℕ → Std.Format
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.rightUnitor_inv_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R : CategoryTheory.Functor Cᵒᵖ CommRingCat}
  (M₁ : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor M₁).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M₁.obj X)).inv
-- Mathlib.Order.Grade
/-- `grade` preserves `CovBy`.  -/
GradeOrder.covBy_grade : ∀ {𝕆 : Type u_5} {α : Type u_6} {inst : Preorder 𝕆} {inst_1 : Preorder α} [self : GradeOrder 𝕆 α] ⦃a b : α⦄,
  a ⋖ b → GradeOrder.grade a ⋖ GradeOrder.grade b
-- Mathlib.Data.Set.Lattice
Set.iInter_eq_const : ∀ {α : Type u_1} {ι : Sort u_5} [Nonempty ι] {f : ι → Set α} {s : Set α}, (∀ (i : ι), f i = s) → ⋂ i, f i = s
-- Mathlib.CategoryTheory.Limits.Preorder
/-- The colimit cocone for a functor `F : J ⥤ C` to a preorder when `pt : C`
is the least upper bound of `Set.range F.obj`  -/
Preorder.colimitCoconeOfIsLUB : {C : Type u} →
  [inst : Preorder C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v, u'} J] →
        (F : CategoryTheory.Functor J C) → {pt : C} → IsLUB (Set.range F.obj) pt → CategoryTheory.Limits.ColimitCocone F
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
/-- Given a subset `F`, an entourage `U` and an integer `n`, a subset `s` is a `(U, n)`-
dynamical cover of `F` if any orbit of length `n` in `F` is `U`-shadowed by an orbit of length `n`
of a point in `s`.  -/
Dynamics.IsDynCoverOf : {X : Type u_1} → (X → X) → Set X → SetRel X X → ℕ → Set X → Prop
-- Init.Data.Ord.UInt
UInt32.instLawfulOrderOrd : Std.LawfulOrderOrd UInt32
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBase.isBasis_ground : ∀ {α : Type u_1} {M : Matroid α} {B : Set α}, M.IsBase B → M.IsBasis B M.E
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.isEmpty : {α : Type u_1} → {β : Type u_2} → Lean.PersistentHashMap.Node α β → Bool
-- Init.Data.BitVec.Bitblast
BitVec.toInt_sdiv_of_ne_or_ne : ∀ {w : ℕ} (a b : BitVec w), a ≠ BitVec.intMin w ∨ b ≠ -1#w → (a.sdiv b).toInt = a.toInt.tdiv b.toInt
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.toSetoid : {S : Type u_2} → {M : Type u_3} → [inst : VAdd S M] → VAddCon S M → Setoid M
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₂_yonedaEquivFst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X Y : C}
  (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y),
  (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).yonedaEquivFst =
    (CategoryTheory.ConcreteCategory.hom (A.map f.op)) p.yonedaEquivFst
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.tail_eval : Turing.ToPartrec.Code.tail.eval = fun v => pure v.tail
-- Mathlib.Algebra.Polynomial.Basic
/-- `Polynomial R` is the type of univariate polynomials over `R`,
denoted as `R[X]` within the `Polynomial` namespace.

Polynomials should be seen as (semi-)rings with the additional constructor `X`.
The embedding from `R` is called `C`.  -/
Polynomial : (R : Type u_1) → [Semiring R] → Type u_1
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.encard_eq_encard : ∀ {α : Type u_1} {M : Matroid α} {I X J : Set α}, M.IsBasis I X → M.IsBasis J X → I.encard = J.encard
-- Mathlib.Topology.ContinuousMap.Interval
ContinuousMap.concat_right : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {a b c : α}
  [inst_3 : Fact (a ≤ b)] [inst_4 : Fact (b ≤ c)] {E : Type u_2} [inst_5 : TopologicalSpace E]
  {f : C(↑(Set.Icc a b), E)} {g : C(↑(Set.Icc b c), E)},
  f ⊤ = g ⊥ → ∀ {t : ↑(Set.Icc a c)} (ht : b ≤ ↑t), (f.concat g) t = g ⟨↑t, ⋯⟩
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.smul : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
  [inst_1 : TopologicalSpace 𝕜] [inst_2 : SMul 𝕜 β] [ContinuousSMul 𝕜 β] {f : α → 𝕜} {g : α → β},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f • g)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α}
  {k fallback : α}, l.contains k = false → (Std.TreeMap.unitOfList l cmp).getKeyD k fallback = fallback
-- Aesop.RuleSet
Aesop.LocalRuleSet.add : Aesop.LocalRuleSet → Aesop.LocalRuleSetMember → Aesop.LocalRuleSet
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.powers.congr_simp : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : CommRing R] (x x_1 : HahnSeries Γ R),
  x = x_1 → HahnSeries.SummableFamily.powers x = HahnSeries.SummableFamily.powers x_1
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.coe_lt_coe : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Preorder β] {f g : MeasureTheory.SimpleFunc α β},
  ⇑f < ⇑g ↔ f < g
-- Mathlib.RepresentationTheory.Coinvariants
Representation.ofQuotient.congr_simp : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ ρ_1 : Representation k G V) (e_ρ : ρ = ρ_1) (S : Subgroup G) [inst_4 : S.Normal]
  [inst_5 : Representation.IsTrivial (MonoidHom.comp ρ S.subtype)], ρ.ofQuotient S = ρ_1.ofQuotient S