mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.mk.sizeOf_spec : ∀ {α : Type u_6} {β : Type u_7} [inst : Max α] [inst_1 : Max β] [inst_2 : Bot α] [inst_3 : Bot β] [inst_4 : SizeOf α]
  [inst_5 : SizeOf β] (toSupHom : SupHom α β) (map_bot' : toSupHom.toFun ⊥ = ⊥),
  sizeOf { toSupHom := toSupHom, map_bot' := map_bot' } = 1 + sizeOf toSupHom + sizeOf map_bot'
-- Mathlib.ModelTheory.Substructures
/-- The equivalence between the domain and the range of an embedding `f`.  -/
FirstOrder.Language.Embedding.equivRange : {L : FirstOrder.Language} →
  {M : Type w} →
    {N : Type u_1} →
      [inst : L.Structure M] → [inst_1 : L.Structure N] → (f : L.Embedding M N) → L.Equiv M ↥f.toHom.range
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.eval_T_real_cos_int_mul_pi_div : ∀ {k n : ℕ}, n ≠ 0 → Polynomial.eval (Real.cos (↑k * Real.pi / ↑n)) (Polynomial.Chebyshev.T ℝ ↑n) = ↑↑(↑k).negOnePow
-- Std.Http.Protocol.H1.Parser
/-- Parses optional whitespace (OWS = *(SP / HTAB), RFC 9110 §5.6.3), bounded by
`limits.maxSpaceSequence`. Fails if more whitespace follows the limit, so oversized
padding is rejected rather than silently truncated.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.ows : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser Unit
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.index_nsmulAddMonoidHom_ker : ∀ (G : Type u_2) [inst : AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ),
  (nsmulAddMonoidHom d).ker.index = Nat.card G / (Nat.card G).gcd d
-- Std.Time.Time.Unit.Hour
/-- Converts an Ordinal into a 1-based hour representation within the range of 1 to 24.
 -/
Std.Time.Hour.Ordinal.shiftTo1BasedHour : Std.Time.Hour.Ordinal → Std.Time.Internal.Bounded.LE 1 24
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableAt.const_smul : ∀ {𝕜 : 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} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [SMulCommClass 𝕜 R F]
  [ContinuousConstSMul R F], DifferentiableAt 𝕜 f x → ∀ (c : R), DifferentiableAt 𝕜 (c • f) x
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A mixin for cancellative multiplication by nonzero elements.  -/
IsCancelMulZero : (M₀ : Type u) → [Mul M₀] → [Zero M₀] → Prop
-- Mathlib.Data.Fin.SuccPred
/-- `castSucc i` is positive when `i` is positive.

The `Fin.castSucc_pos` in `Lean` only applies in `Fin (n+1)`.
This one instead uses a `NeZero n` typeclass hypothesis.  -/
Fin.castSucc_pos' : ∀ {n : ℕ} [inst : NeZero n] {i : Fin n}, 0 < i → 0 < i.castSucc
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int64.intCast_neg : ∀ (i : ℤ), ↑(-i) = -↑i
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {a : α} {b : β}, (t.insert a b).getKey! a = a
-- Mathlib.Topology.Bornology.Absorbs
Absorbs.restrict_scalars : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : Monoid N] [inst_1 : SMul M N] [inst_2 : SMul M α]
  [inst_3 : MulAction N α] [IsScalarTower M N α] [inst_5 : Bornology M] [inst_6 : Bornology N] {s t : Set α},
  Absorbs N s t → Filter.Tendsto (fun x => x • 1) (Bornology.cobounded M) (Bornology.cobounded N) → Absorbs M s t
-- Mathlib.Algebra.Ring.Periodic
/-- The iterates `a`, `f a`, `f^[2] a` etc form a periodic sequence with period `n`
iff `a` is a periodic point for `f`.  -/
Function.periodic_iterate_iff : ∀ {α : Type u_1} {f : α → α} {n : ℕ} {a : α}, Function.Periodic (fun x => f^[x] a) n ↔ Function.IsPeriodicPt f n a
-- Mathlib.Data.Vector.Basic
List.Vector.prod_set : ∀ {α : Type u_1} {n : ℕ} [inst : Monoid α] (v : List.Vector α n) (i : Fin n) (a : α),
  (v.set i a).toList.prod = (List.Vector.take (↑i) v).toList.prod * a * (List.Vector.drop (↑i + 1) v).toList.prod
-- Mathlib.Topology.LocallyClosed
/-- **Alias** of the forward direction of `isLocallyClosed_iff_isOpen_coborder`. -/
IsLocallyClosed.isOpen_coborder : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsLocallyClosed s → IsOpen (coborder s)
-- Init.Data.SInt.Lemmas
Int8.toInt_add : ∀ (a b : Int8), (a + b).toInt = (a.toInt + b.toInt).bmod (2 ^ 8)
-- Mathlib.Order.UpperLower.Principal
/-- Strict principal upper set. `Set.Ioi` as an upper set.  -/
UpperSet.Ioi : {α : Type u_1} → [inst : Preorder α] → α → UpperSet α
-- Mathlib.RingTheory.Depth.Rees
/-- The implication `(4) → (1)` of `exists_isRegular_tfae`: for `M N` finitely generated
module over Noetherian ring `R` and ideal `I` satisfying `IM < M` and `Supp N ⊆ V(I)`,
if there is an `M`-regular sequence `rs` contained in `I`,
then `Ext N M i = 0` for all `i < rs.length`.  -/
ModuleCat.subsingleton_ext_of_exists_isRegular : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (N : ModuleCat R)
  [Nfin : Module.Finite R ↑N],
  Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I →
    ∀ (M : ModuleCat R) [Module.Finite R ↑M],
      I • ⊤ < ⊤ →
        ∀ (rs : List R),
          (∀ r ∈ rs, r ∈ I) →
            RingTheory.Sequence.IsRegular (↑M) rs → ∀ i < rs.length, Subsingleton (CategoryTheory.Abelian.Ext N M i)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_equiv_top : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (f : M ≃+ N), AddSubmonoid.map f ⊤ = ⊤
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.instInhabitedState.default : Std.Http.Protocol.H1.Writer.State
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_neg : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (n : ℤ),
  Mathlib.Tactic.FieldSimp.zpow' a (-n) = (Mathlib.Tactic.FieldSimp.zpow' a n)⁻¹
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.State.mk.sizeOf_spec : ∀ (cur : Array Bool) (added : Array ℕ) (numCalls : ℕ) (found : Bool),
  sizeOf { cur := cur, added := added, numCalls := numCalls, found := found } =
    1 + sizeOf cur + sizeOf added + sizeOf numCalls + sizeOf found
-- Mathlib.Algebra.GroupWithZero.Idempotent
IsIdempotentElem.zero : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀], IsIdempotentElem 0
-- Mathlib.Order.BoundedOrder.Basic
Subtype.mk_eq_top_iff : ∀ {α : Type u} {p : α → Prop} [inst : PartialOrder α] [inst_1 : OrderTop α] [inst_2 : OrderTop (Subtype p)],
  p ⊤ → ∀ {x : α} (hx : p x), ⟨x, hx⟩ = ⊤ ↔ x = ⊤
-- Mathlib.Topology.Algebra.Monoid
ContinuousOn.nsmul : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : AddMonoid M]
  [ContinuousAdd M] {f : X → M} {s : Set X}, ContinuousOn f s → ∀ (n : ℕ), ContinuousOn (n • f) s
-- Init.Data.Array.Count
Array.size_filterMap_eq_countP : ∀ {α : Type u_2} {β : Type u_1} {f : α → Option β} {xs : Array α},
  (Array.filterMap f xs).size = Array.countP (fun a => (f a).isSome) xs
-- Mathlib.Tactic.Linarith.Parsing
/-- The unit monomial `one` is represented by the empty TreeMap.  -/
Mathlib.Tactic.Linarith.one : Mathlib.Tactic.Linarith.Monom
-- Mathlib.Data.Int.Init
Int.pred_self_lt : ∀ (a : ℤ), a.pred < a
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Clopens.coe_sup : ∀ {α : Type u_2} [inst : TopologicalSpace α] (s t : TopologicalSpace.Clopens α), ↑(s ⊔ t) = ↑s ∪ ↑t
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionHom : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] {c c' : C} {d d_1 : D} (f : d ⟶ d_1)
  (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g =
    (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f.op g.op).unop
-- Mathlib.Algebra.Group.Action.Defs
smul_inv_smul : ∀ {G : Type u_3} {α : Type u_5} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α), g • g⁻¹ • a = a
-- Mathlib.Order.Partition.Basic
/-- The collection of parts  -/
Partition.parts : {α : Type u_1} → [inst : CompleteLattice α] → {s : α} → Partition s → Set α
-- Init.Data.Nat.Lemmas
Nat.sub_le_iff_le_add' : ∀ {a b c : ℕ}, a - b ≤ c ↔ a ≤ b + c
-- Lean.Meta.Basic
/-- Annotate any constant and sort in `e` that satisfies `p` with `pp.universes true`  -/
_private.Lean.Meta.Basic.0.Lean.Meta.exposeRelevantUniverses : Lean.Expr → (Lean.Level → Bool) → Lean.Expr
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExpKernel_def : ∀ {Ω : Type u_3} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω] (μ : MeasureTheory.Measure Ω)
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] (m : MeasurableSpace Ω),
  ProbabilityTheory.condExpKernel μ m =
    if _h : Nonempty Ω then (ProbabilityTheory.condDistrib id id μ).comap id ⋯ else 0
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
HasStrictFDerivAt.ccosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {f' : StrongDual ℂ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Complex.cosh (f x)) (Complex.sinh (f x) • f') x
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.smul_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s : Set α} {t u : Set β}, s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u
-- Mathlib.Topology.ApproximateUnit
/-- Multiplication on the left by `m` tends to `𝓝 m` along the filter.  -/
Filter.IsApproximateUnit.tendsto_mul_left : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Mul α] {l : Filter α},
  l.IsApproximateUnit → ∀ (m : α), Filter.Tendsto (fun x => m * x) l (nhds m)
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The structure of the induction in the proof of Chevalley's theorem:
Consider a property on a vector `e` of polynomials. Suppose that it holds for the following cases:
1. The vector contains zeroes only.
2. The vector contains a single monic polynomial (and zero otherwise).
3. Suppose `eᵢ` has the lowest degree among all monic polynomials and `eⱼ` is some other polynomial.
  If the property holds when `eⱼ` is replaced by `eⱼ % eᵢ`, then it holds for `e`.
4. Suppose the property holds for both the localization at some leading coefficient of `eᵢ` and
  the localization at the leading coefficient of `eᵢ`, then the property holds for `e`.

Then it holds for all vectors `e` over all rings.
 -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.induction_structure : ∀ (n : ℕ) (P : (R : Type u) → [inst : CommRing R] → ChevalleyThm.PolynomialC.InductionObj✝ R n → Prop),
  (∀ (R : Type u) [inst : CommRing R], P R { val := 0 }) →
    (∀ (R : Type u) [inst : CommRing R] (e : ChevalleyThm.PolynomialC.InductionObj✝ R n) (i : Fin n),
        (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).Monic →
          (∀ (j : Fin n), j ≠ i → ChevalleyThm.PolynomialC.InductionObj.val✝ e j = 0) → P R e) →
      (∀ (R : Type u) [inst : CommRing R] (e : ChevalleyThm.PolynomialC.InductionObj✝ R n) (i j : Fin n),
          (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).Monic →
            (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).degree ≤
                (ChevalleyThm.PolynomialC.InductionObj.val✝ e j).degree →
              i ≠ j →
                P R
                    {
                      val :=
                        Function.update (ChevalleyThm.PolynomialC.InductionObj.val✝ e) j
                          (ChevalleyThm.PolynomialC.InductionObj.val✝ e j %ₘ
                            ChevalleyThm.PolynomialC.InductionObj.val✝ e i) } →
                  P R e) →
        (∀ (R : Type u) [inst : CommRing R] (c : R) (i : Fin n) (e : ChevalleyThm.PolynomialC.InductionObj✝ R n),
            c = (ChevalleyThm.PolynomialC.InductionObj.val✝ e i).leadingCoeff →
              c ≠ 0 →
                P (Localization.Away c)
                    {
                      val :=
                        Polynomial.C (IsLocalization.Away.invSelf c) •
                          ⇑(Polynomial.mapRingHom (algebraMap R (Localization.Away c))) ∘
                            ChevalleyThm.PolynomialC.InductionObj.val✝ e } →
                  P (R ⧸ Ideal.span {c})
                      {
                        val :=
                          ⇑(Polynomial.mapRingHom (algebraMap R (R ⧸ Ideal.span {c}))) ∘
                            ChevalleyThm.PolynomialC.InductionObj.val✝ e } →
                    P R e) →
          ∀ {R : Type u} [inst : CommRing R] (e : ChevalleyThm.PolynomialC.InductionObj✝ R n), P R e
-- Mathlib.Geometry.Manifold.HasGroupoid
hasGroupoid_of_pregroupoid : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (PG : Pregroupoid H),
  (∀ {e e' : OpenPartialHomeomorph M H},
      e ∈ atlas H M → e' ∈ atlas H M → PG.property (↑(e.symm.trans e')) (e.symm.trans e').source) →
    HasGroupoid M PG.groupoid
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.count_edges_takeUntil_le_one : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support) (x : V),
  List.count s(u, x) (p.takeUntil u h).edges ≤ 1
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.mk.inj : ∀ {toBoolAlg : BoolAlg} {isFintype : Fintype ↑toBoolAlg} {toBoolAlg_1 : BoolAlg} {isFintype_1 : Fintype ↑toBoolAlg_1},
  { toBoolAlg := toBoolAlg, isFintype := isFintype } = { toBoolAlg := toBoolAlg_1, isFintype := isFintype_1 } →
    toBoolAlg = toBoolAlg_1 ∧ isFintype ≍ isFintype_1
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.colimit_sound' : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} {j'' : J} (f : j ⟶ j'')
  (f' : j' ⟶ j''),
  (CategoryTheory.ConcreteCategory.hom (F.map f)) x = (CategoryTheory.ConcreteCategory.hom (F.map f')) x' →
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j')) x'
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Given a functor `G : J × K ⥤ C` such that `(curry.obj G ⋙ colim)` makes sense and has a colimit,
we can construct a cocone under `G` with `colimit (curry.obj G ⋙ colim)` as a cocone point  -/
CategoryTheory.Limits.coconeOfHasColimitCurryCompColim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C] →
                [CategoryTheory.Limits.HasColimit
                      ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)] →
                  CategoryTheory.Limits.Cocone G
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.get!ₘ_eq_getValue! : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [PartialEquivBEq α] [LawfulHashable α]
  [inst_4 : Inhabited β] {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α},
      Std.DHashMap.Internal.Raw₀.Const.get!ₘ m a =
        Std.Internal.List.getValue! a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.yoneda'_map_hom : ∀ {X Y : Type u} (f : X ⟶ Y), (CategoryTheory.yoneda'.map f).hom = CategoryTheory.yoneda.map f
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.mk : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} → [inst : LinearOrder ι] → {f : P.RankFunction ι} → {i : ι} → (s : ↑P.II) → f.rank s = i → f.Cell i
-- Aesop.RuleTac.Basic
/-- Input for a rule tactic.  -/
Aesop.RuleTacInput : Type
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] (R : Type u_3) [inst_1 : NonUnitalSeminormedRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R] (x y : R),
  ‖((ContinuousLinearMap.mulLeftRight 𝕜 R) x) y‖ ≤ ‖x‖ * ‖y‖
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) =
    (Std.DTreeMap.Internal.Impl.contains k m₁ || Std.DTreeMap.Internal.Impl.contains k m₂)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_map : ∀ (R : Type u) (S : Type v) {T : Type w} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing T]
  (p : Polynomial T) [inst_3 : CommRing S] [inst_4 : Algebra T S] [inst_5 : Algebra S R] [inst_6 : Algebra T R]
  [IsScalarTower T S R], (Polynomial.map (algebraMap T S) p).aroots R = p.aroots R
-- 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₃ ((CategoryTheory.shiftFunctor C 1).map e₁.hom) =
      CategoryTheory.CategoryStruct.comp e₃.hom T₂.mor₃),
  (CategoryTheory.Pretriangulated.isoTriangleOfIso₁₃ T₁ T₂ hT₁ hT₂ e₁ e₃ comm).inv.hom₁ = e₁.inv
-- Init.Data.Iterators.Lemmas.Combinators.Take
_private.Init.Data.Iterators.Lemmas.Combinators.Take.0.Std.Iter.atIdxSlow?_eq_match.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- Given
```
X₁ - f₁ -> X₂ - f₂ -> X₃
|          |          |
i₁         i₂         i₃
∨          ∨          ∨
Y₁ - g₁ -> Y₂ - g₂ -> Y₃
```
Then the big square is a pushout if both the small squares are.
 -/
CategoryTheory.Limits.pasteHorizIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Y₁ : C} →
      {f₁ : X₁ ⟶ X₂} →
        {f₂ : X₂ ⟶ X₃} →
          {i₁ : X₁ ⟶ Y₁} →
            {t₁ : CategoryTheory.Limits.PushoutCocone i₁ f₁} →
              {i₂ : X₂ ⟶ t₁.pt} →
                {t₂ : CategoryTheory.Limits.PushoutCocone i₂ f₂} →
                  (hi₂ : i₂ = t₁.inr) →
                    CategoryTheory.Limits.IsColimit t₁ →
                      CategoryTheory.Limits.IsColimit t₂ → CategoryTheory.Limits.IsColimit (t₁.pasteHoriz t₂ hi₂)
-- Init.Meta.Defs
/-- Returns syntax for the given value.
 -/
Lean.Quote.quote : {α : Type} → {k : optParam Lean.SyntaxNodeKind `term} → [self : Lean.Quote α k] → α → Lean.TSyntax k
-- Mathlib.CategoryTheory.Monad.Basic
/-- The multiplication for the monad.  -/
CategoryTheory.Monad.μ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (self : CategoryTheory.Monad C) → self.comp self.toFunctor ⟶ self.toFunctor
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.CoeAdjoinAux.mk : ∀ {α : Type u_1} {x : α} {s : Set α}, x ∈ s → Algebra.CoeAdjoinAux x s
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.coe_mk_subtype : ∀ {z : ℂ} (hz : 0 < z.im), ↑{ coe := z, coe_im_pos := hz } = z
-- Mathlib.Data.Setoid.Basic
Setoid.top_def : ∀ {α : Type u_1}, ⇑⊤ = ⊤
-- Mathlib.Data.Finset.Card
/-- **Alias** of the reverse direction of `Finset.card_pair_eq_two_iff`.

---

A two-element finset `{a, b}` has cardinality `2` iff `a ≠ b`. The reverse direction is
`Finset.card_pair`.  -/
Finset.card_pair : ∀ {α : Type u_1} {a b : α} [inst : DecidableEq α], a ≠ b → {a, b}.card = 2
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_union_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Aesop.Search.Expansion.Norm
Aesop.modifyForwardState : Aesop.ForwardState → Array Aesop.ForwardRuleMatch → Std.HashSet Lean.FVarId → Aesop.NormM Unit
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.ofEq_rfl : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {R' : Type u_12} [inst_1 : Ring R'] [inst_2 : Module R' E]
  {p : Submodule R' E}, LinearIsometryEquiv.ofEq p p ⋯ = LinearIsometryEquiv.refl R' ↥p
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Notation for the `whiskerRight` operator of monoidal categories  -/
CategoryTheory.MonoidalCategory.«term_▷_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.d_pos : ∀ {a : ℕ} (a1 : 1 < a), 0 < Pell.d✝ a1
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- `s₁` is not a subset of `s₂`  -/
Lean.Grind.AC.SubsetResult.false : Lean.Grind.AC.SubsetResult
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_coe : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (f : A →A[R] B), ⇑↑f = ⇑f
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instTransOrdOrdinal : Std.TransOrd Std.Time.Minute.Ordinal
-- Init.Data.FloatArray.Basic
FloatArray.usize : FloatArray → USize
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.map.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone G} (P : CategoryTheory.Limits.IsColimit t)
  (s : CategoryTheory.Limits.Cocone F) (α : G ⟶ F),
  P.map s α = P.desc ((CategoryTheory.Limits.Cocone.precompose α).obj s)
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.IsVeryGood.fibration_π : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {A : C}
  {inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C} {P : HomotopicalAlgebra.Cylinder A}
  {inst_2 : CategoryTheory.Limits.HasBinaryCoproduct A A} {inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C}
  {inst_4 : HomotopicalAlgebra.CategoryWithFibrations C} [self : P.IsVeryGood], HomotopicalAlgebra.Fibration P.π
-- Mathlib.Data.Set.Sigma
Set.mk_mem_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s : Set ι} {t : (i : ι) → Set (α i)} {i : ι} {a : α i},
  i ∈ s → a ∈ t i → ⟨i, a⟩ ∈ s.sigma t
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Morphisms of group objects preserve negations.  -/
CategoryTheory.AddGrpObj.neg_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj A] [inst_3 : CategoryTheory.AddGrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsAddMonHom f] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg h)
-- Mathlib.Data.Matrix.Basic
Matrix.diag_multiset_sum : ∀ {n : Type u_3} {α : Type u_11} [inst : AddCommMonoid α] (s : Multiset (Matrix n n α)),
  s.sum.diag = (Multiset.map Matrix.diag s).sum
-- Mathlib.Analysis.Polynomial.Basic
/-- If `deg Q < deg P`, there are only finitely many integers `x` where `|P(x)| ≤ |Q(x)|`.  -/
Polynomial.finite_abs_eval_le_of_degree_lt : ∀ {P Q : Polynomial ℤ}, Q.degree < P.degree → {x | |Polynomial.eval x P| ≤ |Polynomial.eval x Q|}.Finite
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → Std.Sat.AIG α → ℕ → Type