mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.SimpleModule.WedderburnArtin
/-- A simple ring is semisimple iff it is Artinian, iff it has a minimal left ideal.  -/
IsSimpleRing.tfae : ∀ {R : Type u} [inst : Ring R] [IsSimpleRing R], [IsSemisimpleRing R, IsArtinianRing R, ∃ I, IsAtom I].TFAE
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.comp_f₃_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁ ⟶ S₂) (g : S₂ ⟶ S₃) {Z : CategoryTheory.ShortComplex C}
  (h : S₃.L₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g).f₃ h =
    CategoryTheory.CategoryStruct.comp f.f₃ (CategoryTheory.CategoryStruct.comp g.f₃ h)
-- Mathlib.Analysis.ODE.Gronwall
/-- If `f` and `g` are two exact solutions of the same ODE, then the distance between them
can't grow faster than exponentially. This is a simple corollary of Grönwall's inequality, and some
people call this Grönwall's inequality too.

This version assumes all inequalities to be true in the whole space.  -/
dist_le_of_trajectories_ODE : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {v : ℝ → E → E} {K : NNReal} {f g : ℝ → E}
  {a b δ : ℝ},
  (∀ (t : ℝ), LipschitzWith K (v t)) →
    ContinuousOn f (Set.Icc a b) →
      (∀ t ∈ Set.Ico a b, HasDerivWithinAt f (v t (f t)) (Set.Ici t) t) →
        ContinuousOn g (Set.Icc a b) →
          (∀ t ∈ Set.Ico a b, HasDerivWithinAt g (v t (g t)) (Set.Ici t) t) →
            dist (f a) (g a) ≤ δ → ∀ t ∈ Set.Icc a b, dist (f t) (g t) ≤ δ * Real.exp (↑K * (t - a))
-- Mathlib.Algebra.Group.Conj
ConjClasses.exists_rep : ∀ {α : Type u} [inst : Monoid α] (a : ConjClasses α), ∃ a0, ConjClasses.mk a0 = a
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
Finset.prod_le_prod_of_subset_of_le_one : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {f : ι → R} {s t : Finset ι}, s ⊆ t → (∀ i ∈ t, 0 ≤ f i) → (∀ i ∈ t, i ∉ s → f i ≤ 1) → ∏ i ∈ t, f i ≤ ∏ i ∈ s, f i
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instSMulCommClass : ∀ {𝕜 : Type u_2} {𝕜' : Type u_3} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] [inst_7 : NormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F]
  [SMulCommClass 𝕜 𝕜' F], SMulCommClass 𝕜 𝕜' (SchwartzMap E F)
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.RingObjCat.forget₂Mon_obj_mon : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (R : CategoryTheory.RingObjCat C),
  ((CategoryTheory.RingObjCat.forget₂Mon C).obj R).mon = R.ringObj.toMonObj
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The first arrow defining the relation.  -/
CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.g₁ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {J : CategoryTheory.GrothendieckTopology C} →
        {S : J.Cover X} → {I₁ I₂ : S.Arrow} → (self : I₁.Relation I₂) → self.Z ⟶ I₁.Y
-- Mathlib.Order.Concept
Concept.intent_ofObjects : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Set α), (Concept.ofObjects r s).intent = upperPolar r s
-- Mathlib.Geometry.Convex.Set
Convexity.IsConvexSet.prod : ∀ {R : Type u_3} {X : Type u_5} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X} {Y : Type u_7} [inst_4 : Convexity.ConvexSpace R Y] {t : Set Y},
  Convexity.IsConvexSet R s → Convexity.IsConvexSet R t → Convexity.IsConvexSet R (s ×ˢ t)
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pushout.inr_codiagonal_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPushout f f] {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.codiagonal f) h) =
    h
-- Mathlib.Algebra.Colimit.Finiteness
/-- Every module is the direct limit of its finitely generated submodules.  -/
Module.fgSystem.equiv : (R : Type u_1) →
  (M : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          [inst_3 : DecidableEq (Submodule R M)] → Module.DirectLimit (fun i => ↥↑i) (Module.fgSystem R M) ≃ₗ[R] M
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Indep.exists_insert_of_encard_lt : ∀ {α : Type u_1} {M : Matroid α} {I J : Set α},
  M.Indep I → M.Indep J → I.encard < J.encard → ∃ e ∈ J \ I, M.Indep (insert e I)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.coe_sup : ∀ {E : Type u_3} [inst : Group E] (p q : GroupSeminorm E), ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.GeneralLinearGroup.val_map_apply : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (u : (Matrix n n R)ˣ), ↑((Matrix.GeneralLinearGroup.map f) u) = (↑u).map ⇑f
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.countable_leftLim_ne : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] [OrderTopology R] (f : StieltjesFunction R),
  {x | Function.leftLim (↑f) x ≠ ↑f x}.Countable
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.addHom_ext'_iff : ∀ {R : Type u} [inst : Semiring R] {M : Type u_1} [inst_1 : AddZeroClass M] {f g : Polynomial R →+ M},
  f = g ↔ ∀ (n : ℕ), f.comp (Polynomial.monomial n).toAddMonoidHom = g.comp (Polynomial.monomial n).toAddMonoidHom
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_filter_eq_length_iff : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {f : (a : α) → β a → Bool}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ((List.filter (fun p => f p.fst p.snd) l).length = l.length ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true), f a (Std.Internal.List.getValueCast a l h) = true)
-- Mathlib.Algebra.Algebra.Subalgebra.Centralizer
/-- Let `R` be a commutative ring and `A, B` be `R`-algebras where `B` is free as `R`-module.
For any subalgebra `S` of `A`, the centralizer of `S ⊗ 1 ⊆ A ⊗ B` is `C_A(S) ⊗ B` where `C_A(S)` is
the centralizer of `S` in `A`.
 -/
Subalgebra.centralizer_coe_map_includeLeft_eq_center_tensorProduct : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] [inst_2 : Algebra R A] (B : Type u_3)
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (S : Subalgebra R A) [Module.Free R B],
  Subalgebra.centralizer R ↑(Subalgebra.map Algebra.TensorProduct.includeLeft S) =
    (Algebra.TensorProduct.map (Subalgebra.centralizer R ↑S).val (AlgHom.id R B)).range
-- Mathlib.MeasureTheory.Measure.NullMeasurable
Set.Finite.nullMeasurableSet_biInter : ∀ {ι : Type u_1} {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : ι → Set α} {s : Set ι},
  s.Finite → (∀ b ∈ s, MeasureTheory.NullMeasurableSet (f b) μ) → MeasureTheory.NullMeasurableSet (⋂ b ∈ s, f b) μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Data.List.Cycle
Cycle.lists_coe : ∀ {α : Type u_1} (l : List α), (↑l).lists = ↑l.cyclicPermutations
-- Mathlib.Data.List.Basic
List.foldr_hom₂ : ∀ {ι : Type u_1} {α : Type u} {β : Type v} {γ : Type w} (l : List ι) (f : α → β → γ) (op₁ : ι → α → α) (op₂ : ι → β → β)
  (op₃ : ι → γ → γ) (a : α) (b : β),
  (∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)) →
    List.foldr op₃ (f a b) l = f (List.foldr op₁ a l) (List.foldr op₂ b l)
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.Hom.mk : {ι : Type t} →
  {X : ι → Type u} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {Y Z : ContinuousGeneratedByCat X} → Topology.ContinuousMapGeneratedBy X ↑Y ↑Z → Y.Hom Z
-- Mathlib.RingTheory.Localization.Cardinality
IsFractionRing.lift_cardinalMk : ∀ (R : Type u) [inst : CommRing R] (L : Type v) [inst_1 : CommRing L] [inst_2 : Algebra R L] [IsFractionRing R L],
  Cardinal.lift.{u, v} (Cardinal.mk L) = Cardinal.lift.{v, u} (Cardinal.mk R)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : BoundedLatticeHom α β),
  BooleanSubalgebra.map f ⊥ = ⊥
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_rhs_suffix : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ head lhs₂ rhs₂ rhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_suffix_cert lhs₁ rhs₁ head rhs₂ rhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂'
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instLEOffset : LE Std.Time.Minute.Offset
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- Hölder inequality  -/
lp.tsum_mul_le_mul_norm : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p q : ENNReal},
  p.toReal.HolderConjugate q.toReal →
    ∀ (f : ↥(lp E p)) (g : ↥(lp E q)), (Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- The natural equivalence between linear endomorphisms of finite free modules and square matrices
is compatible with the algebra structures.  -/
algEquivMatrix' : {R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type u_3} → [inst_1 : DecidableEq n] → [inst_2 : Fintype n] → Module.End R (n → R) ≃ₐ[R] Matrix n n R
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.posFittingCompOf.congr_simp : ∀ (R : Type u_2) {L : Type u_3} (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] (x x_1 : L),
  x = x_1 → LieModule.posFittingCompOf R M x = LieModule.posFittingCompOf R M x_1
-- Mathlib.Tactic.FBinop
/-- `true` if there are two types `α` and `β` where we don't have coercions in any direction.  -/
_private.Mathlib.Tactic.FBinop.0.FBinopElab.AnalyzeResult.hasUncomparable : FBinopElab.AnalyzeResult✝ → Bool
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.instInhabitedOffset : Inhabited Std.Time.TimeZone.Offset
-- Lean.Language.Lean.Types
/-- State after successful parsing.  -/
Lean.Language.Lean.HeaderParsedSnapshot.result? : Lean.Language.Lean.HeaderParsedSnapshot → Option Lean.Language.Lean.HeaderParsedState
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.Cover.oneHypercover_toPreOneHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (S : J.Cover X), S.oneHypercover.toPreOneHypercover = S.preOneHypercover
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If an alternating map `f` satisfies a boundedness property around `0`,
one can deduce a bound on `f m₁ - f m₂` using the multilinearity.
Here, we give a usable but not very precise version.
See `AlternatingMap.norm_image_sub_le_of_bound'` for a more precise but less usable version.
The bound is `‖f m - f m'‖ ≤ C * card ι * ‖m - m'‖ * (max ‖m‖ ‖m'‖) ^ (card ι - 1)`.  -/
AlternatingMap.norm_image_sub_le_of_bound : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F) {C : ℝ},
  0 ≤ C →
    (∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
      ∀ (m₁ m₂ : ι → E), ‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E}, DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (-f) x
-- Std.Internal.Do.WP.Basic
/-- Weakest precondition of `x` for normal postcondition `post` and exception postcondition `epost`.
The `WP` interpretation can be supplied explicitly via dot notation (`inst.wp x post epost`).  -/
Std.Internal.Do.WP.wp : {Prog : Type u} →
  {Value : Type v} →
    {Pred : Type w} →
      {EPred : Type w'} →
        [inst : Std.Internal.Do.Assertion Pred] →
          [inst_1 : Std.Internal.Do.Assertion EPred] →
            [self : Std.Internal.Do.WP Prog Value Pred EPred] → Prog → (Value → Pred) → EPred → Pred
-- Mathlib.CategoryTheory.Functor.Basic
/-- The action of a functor on morphisms.  -/
CategoryTheory.Functor.map : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (self : CategoryTheory.Functor C D) → {X Y : C} → (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
-- Mathlib.SetTheory.Cardinal.Divisibility
/-- Alias of `isUnit_iff_eq_one` for discoverability.  -/
Cardinal.isUnit_iff : ∀ {a : Cardinal.{u}}, IsUnit a ↔ a = 1
-- Mathlib.CategoryTheory.Limits.Types.Pullbacks
/-- The explicit pullback in the category of types, bundled up as a `LimitCone`
for given `f` and `g`.
 -/
CategoryTheory.Limits.Types.pullbackLimitCone : {X Y Z : Type u} → (f : X ⟶ Z) → (g : Y ⟶ Z) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.cospan f g)
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.congr : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {X Y : CategoryTheory.Grothendieck F} {f g : X ⟶ Y} (h : f = g),
  f.fiber = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g.fiber
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.isBasis'_iff_isBasis : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α},
  autoParam (X ⊆ M.E) Matroid.isBasis'_iff_isBasis._auto_1 → (M.IsBasis' I X ↔ M.IsBasis I X)
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.destructTuple.destruct : List Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.Algebra.Group.Subgroup.Ker
Subgroup.comap_sup_eq_of_le_range : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N) {H K : Subgroup N},
  H ≤ f.range → K ≤ f.range → Subgroup.comap f H ⊔ Subgroup.comap f K = Subgroup.comap f (H ⊔ K)
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.HasShift C ℤ}
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} {hom₁ : T₁.obj₁ ⟶ T₂.obj₁} {hom₂ : T₁.obj₂ ⟶ T₂.obj₂}
  {hom₃ : T₁.obj₃ ⟶ T₂.obj₃}
  {comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ T₂.mor₁)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₁._autoParam}
  {comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ T₂.mor₂)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₂._autoParam}
  {comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
        CategoryTheory.CategoryStruct.comp hom₃ T₂.mor₃)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₃._autoParam}
  {hom₁_1 : T₁.obj₁ ⟶ T₂.obj₁} {hom₂_1 : T₁.obj₂ ⟶ T₂.obj₂} {hom₃_1 : T₁.obj₃ ⟶ T₂.obj₃}
  {comm₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₁ hom₂_1 = CategoryTheory.CategoryStruct.comp hom₁_1 T₂.mor₁)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₁._autoParam}
  {comm₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₂ hom₃_1 = CategoryTheory.CategoryStruct.comp hom₂_1 T₂.mor₂)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₂._autoParam}
  {comm₃_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁_1) =
        CategoryTheory.CategoryStruct.comp hom₃_1 T₂.mor₃)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₃._autoParam},
  { hom₁ := hom₁, hom₂ := hom₂, hom₃ := hom₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃ } =
      { hom₁ := hom₁_1, hom₂ := hom₂_1, hom₃ := hom₃_1, comm₁ := comm₁_1, comm₂ := comm₂_1, comm₃ := comm₃_1 } →
    hom₁ = hom₁_1 ∧ hom₂ = hom₂_1 ∧ hom₃ = hom₃_1
-- Mathlib.RingTheory.PowerSeries.Exp
PowerSeries.order_exp : ∀ (A : Type u_4) [inst : Ring A] [inst_1 : Algebra ℚ A] [Nontrivial A], (PowerSeries.exp A).order = 0
-- Mathlib.RingTheory.Localization.Integral
RingHom.isIntegralElem_localization_at_leadingCoeff : ∀ {R : Type u_5} {S : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (x : S)
  (p : Polynomial R),
  Polynomial.eval₂ f x p = 0 →
    ∀ (M : Submonoid R),
      p.leadingCoeff ∈ M →
        ∀ {Rₘ : Type u_7} {Sₘ : Type u_8} [inst_2 : CommRing Rₘ] [inst_3 : CommRing Sₘ] [inst_4 : Algebra R Rₘ]
          [inst_5 : IsLocalization M Rₘ] [inst_6 : Algebra S Sₘ] [inst_7 : IsLocalization (Submonoid.map f M) Sₘ],
          (IsLocalization.map Sₘ f ⋯).IsIntegralElem ((algebraMap S Sₘ) x)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc : ∀ {n : Type u} {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.toSpecMvPoly n T) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.toSpecMvPoly n S) h
-- Mathlib.Analysis.SpecificLimits.Normed
geom_series_mul_neg : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (x : R), ‖x‖ < 1 → (∑' (i : ℕ), x ^ i) * (1 - x) = 1
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftId_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]
  (L : CategoryTheory.Functor A 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] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftId L R).inv.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Lean.Data.JsonRpc
Lean.JsonRpc.instCoeJsonNumberRequestID : Coe Lean.JsonNumber Lean.JsonRpc.RequestID
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.map_obj_left : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R),
  ((CategoryTheory.Comma.map α β).obj X).left = F₁.obj X.left
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.liftKaehlerDifferential_D : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S],
  (KaehlerDifferential.D R S).liftKaehlerDifferential = LinearMap.id
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.trivial_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C)
  (x x_1 : (CategoryTheory.PreZeroHypercover.singleton (CategoryTheory.CategoryStruct.id S)).I₀) (x_2 : PUnit.{w + 1}),
  (CategoryTheory.PreOneHypercover.trivial S).Y x_2 = S
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.equivOp.eq_1 : ∀ {M : Type u_2} [inst : AddZeroClass M] (H : AddSubmonoid M), H.equivOp = AddOpposite.opEquiv.subtypeEquiv ⋯
-- Mathlib.RingTheory.Ideal.Height
/-- If `x` is a non-zero-divisor, then `span {x}` has height at least 1.  -/
Ideal.one_le_height_span_singleton_of_mem_nonZeroDivisors : ∀ {R : Type u_1} [inst : CommRing R] {x : R}, x ∈ nonZeroDivisors R → 1 ≤ (Ideal.span {x}).height
-- Mathlib.Algebra.Group.Prod
Prod.instAddCommGroup : {G : Type u_1} → {H : Type u_2} → [AddCommGroup G] → [AddCommGroup H] → AddCommGroup (G × H)
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
CategoryTheory.IsGrothendieckAbelian.hasLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C], CategoryTheory.Limits.HasLimitsOfSize.{w, w, v, u} C
-- Mathlib.Algebra.Symmetrized
SymAlg.nonAssocSemiring : {α : Type u_1} → [inst : Semiring α] → [Invertible 2] → NonAssocSemiring αˢʸᵐ
-- Mathlib.Algebra.BigOperators.Ring.Finset
Int.cast_list_sum : ∀ {R : Type u_4} [inst : AddGroupWithOne R] (s : List ℤ), ↑s.sum = (List.map Int.cast s).sum
-- Aesop.Search.Queue
Aesop.FIFOQueue.instQueue : Aesop.Queue Aesop.FIFOQueue
-- Mathlib.Algebra.Module.Presentation.Tensor
Module.Relations.tensor_G : ∀ {A : Type u} [inst : CommRing A] (relations₁ : Module.Relations A) (relations₂ : Module.Relations A),
  (relations₁.tensor relations₂).G = (relations₁.G × relations₂.G)
-- Mathlib.Data.Finset.Range
Finset.mem_range_le : ∀ {n x : ℕ}, x ∈ Finset.range n → x ≤ n
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.mk.injEq : ∀ (toPartOrd : PartOrd) [isFintype : Fintype ↑toPartOrd] (toPartOrd_1 : PartOrd) (isFintype_1 : Fintype ↑toPartOrd_1),
  ({ toPartOrd := toPartOrd, isFintype := isFintype } = { toPartOrd := toPartOrd_1, isFintype := isFintype_1 }) =
    (toPartOrd = toPartOrd_1 ∧ isFintype ≍ isFintype_1)
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivAt_iff_isLittleO_nhds_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜},
  HasDerivAt f f' x ↔ (fun h => f (x + h) - f x - h • f') =o[nhds 0] fun h => h
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_mul_of_ediv_dvd : ∀ {a b c : ℤ}, b ∣ a → a / b ∣ c → a ∣ b * c
-- Mathlib.Order.Hom.Lattice
SupHom.comp.eq_1 : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Max α] [inst_1 : Max β] [inst_2 : Max γ] (f : SupHom β γ)
  (g : SupHom α β), f.comp g = { toFun := ⇑f ∘ ⇑g, map_sup' := ⋯ }
-- Mathlib.Data.Ineq
Mathlib.instInhabitedIneq.default : Mathlib.Ineq
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.whiskerLeft_inv_hom_whiskerRight_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) (k : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp h k) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η.inv k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η.hom k)) h_1) =
    h_1
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- The `Subsemigroup` generated by a set.  -/
Subsemigroup.closure : {M : Type u_1} → [inst : Mul M] → Set M → Subsemigroup M