mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Abelian.RightDerived
/-- We can compute a right derived functor using a chosen injective resolution.  -/
CategoryTheory.InjectiveResolution.isoRightDerivedObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
        [inst_2 : CategoryTheory.Abelian C] →
          [inst_3 : CategoryTheory.HasInjectiveResolutions C] →
            [inst_4 : CategoryTheory.Abelian D] →
              {X : C} →
                (I : CategoryTheory.InjectiveResolution X) →
                  (F : CategoryTheory.Functor C D) →
                    [inst_5 : F.Additive] →
                      (n : ℕ) →
                        (F.rightDerived n).obj X ≅
                          (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj
                            ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)
-- Mathlib.Order.SupClosed
SupClosed.insert_upperBounds : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α} {a : α}, SupClosed s → a ∈ upperBounds s → SupClosed (insert a s)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.self_val : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (a : S),
  (Algebra.Generators.self R S).val a = id a
-- Mathlib.Control.Fold
Traversable.foldl_toList : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] [LawfulTraversable t] (f : α → β → α) (xs : t β) (x : α),
  Traversable.foldl f x xs = List.foldl f x (Traversable.toList xs)
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
/-- **Alias** of the reverse direction of `Nat.pow_nthRoot_le_iff`.

---

`nthRoot n a ^ n ≤ a` unless both `n` and `a` are zeros.  -/
Nat.pow_nthRoot_le : ∀ {n a : ℕ}, n ≠ 0 ∨ a ≠ 0 → n.nthRoot a ^ n ≤ a
-- Mathlib.AlgebraicTopology.ModelCategory.BrownLemma
HomotopicalAlgebra.FibrantBrownFactorization.instWeakEquivalenceR : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) (h : HomotopicalAlgebra.FibrantBrownFactorization f), HomotopicalAlgebra.WeakEquivalence h.r
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.univ_add_univ : ∀ {α : Type u_2} [inst : AddMonoid α], Set.univ + Set.univ = Set.univ
-- Init.Data.SInt.Lemmas
Int8.ofIntClamp.eq_1 : ∀ (i : ℤ),
  Int8.ofIntClamp i =
    if hl : Int8.minValue.toInt ≤ i then if hr : i ≤ Int8.maxValue.toInt then Int8.ofIntLE i hl hr else Int8.maxValue
    else Int8.minValue
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval₂Hom_C : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (r : R), (MvPolynomial.eval₂Hom f g) (MvPolynomial.C r) = f r
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
/-- Destructor for constant functor  -/
MvQPF.Const.get : {n : ℕ} → {A : Type u} → {α : TypeVec.{u} n} → MvQPF.Const n A α → A
-- Mathlib.GroupTheory.GroupAction.Defs
AddAction.orbitRel.quotient_eq_of_quotient_addSubgroup_eq : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {H : AddSubgroup G} {a b : α},
  ⟦a⟧ = ⟦b⟧ → ⟦a⟧ = ⟦b⟧
-- Mathlib.Data.Countable.Defs
uncountable_iff_forall_not_surjective : ∀ {α : Sort u} [Nonempty α], Uncountable α ↔ ∀ (f : ℕ → α), ¬Function.Surjective f
-- Std.Tactic.BVDecide.LRAT.Internal.PosFin
Std.Tactic.BVDecide.LRAT.Internal.instToStringPosFin : {n : ℕ} → ToString (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)
-- Mathlib.Algebra.BigOperators.Ring.Multiset
Multiset.sum_map_mul_right : ∀ {ι : Type u_1} {R : Type u_4} [inst : NonUnitalNonAssocSemiring R] {a : R} {s : Multiset ι} {f : ι → R},
  (Multiset.map (fun i => f i * a) s).sum = (Multiset.map f s).sum * a
-- Mathlib.LinearAlgebra.QuadraticForm.Signature
exists_finrank_eq_sigNeg_and_negDef : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommGroup M] [inst_1 : CommRing R] [inst_2 : LinearOrder R]
  [inst_3 : Module R M] (Q : QuadraticForm R M) [Module.Finite R M] [StrongRankCondition R],
  ∃ V, Module.finrank R ↥V = sigNeg Q ∧ (QuadraticMap.restrict (-Q) V).PosDef
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instZPow : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : Group G] → [IsTopologicalGroup G] → Pow (SeparationQuotient G) ℤ
-- Mathlib.Analysis.Calculus.FDeriv.Defs
HasFDerivWithinAt.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (f : E → F) (f' : E →L[𝕜] F) (s : Set E) (x : E),
  HasFDerivWithinAt f f' s x = HasFDerivAtFilter f f' (nhdsWithin x s ×ˢ pure x)
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.instLargeCategory : CategoryTheory.LargeCategory UniformSpaceCat
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_center_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] {a : A},
  a ∈ NonUnitalSubalgebra.center R A ↔ ∀ (b : A), b * a = a * b
-- Mathlib.RingTheory.Algebraic.Basic
/-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K  -/
Algebra.IsAlgebraic.tower_top : ∀ {K : Type u_1} (L : Type u_2) {A : Type u_5} [inst : Field K] [inst_1 : Field L] [inst_2 : Ring A]
  [inst_3 : Algebra K L] [inst_4 : Algebra L A] [inst_5 : Algebra K A] [IsScalarTower K L A] [Algebra.IsAlgebraic K A],
  Algebra.IsAlgebraic L A
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trStmts₁.match_1.eq_7 : ∀ (motive : Turing.PartrecToTM2.Λ' → Sort u_1) (q₁ q₂ : Turing.PartrecToTM2.Λ')
  (h_1 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k₁ k₂ : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.move p k₁ k₂ q → motive (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q))
  (h_2 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.K') →
        (s : Option Turing.PartrecToTM2.Γ' → Option Turing.PartrecToTM2.Γ') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.push k s q → motive (Turing.PartrecToTM2.Λ'.push k s q))
  (h_3 :
    (Q : Turing.PartrecToTM2.Λ') →
      (q : Option Turing.PartrecToTM2.Γ' → Turing.PartrecToTM2.Λ') →
        Q = Turing.PartrecToTM2.Λ'.read q → motive (Turing.PartrecToTM2.Λ'.read q))
  (h_4 :
    (Q : Turing.PartrecToTM2.Λ') →
      (p : Turing.PartrecToTM2.Γ' → Bool) →
        (k : Turing.PartrecToTM2.K') →
          (q : Turing.PartrecToTM2.Λ') →
            Q = Turing.PartrecToTM2.Λ'.clear p k q → motive (Turing.PartrecToTM2.Λ'.clear p k q))
  (h_5 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.copy → motive q.copy)
  (h_6 : (Q q : Turing.PartrecToTM2.Λ') → Q = q.succ → motive q.succ)
  (h_7 : (Q q₁ q₂ : Turing.PartrecToTM2.Λ') → Q = q₁.pred q₂ → motive (q₁.pred q₂))
  (h_8 :
    (Q : Turing.PartrecToTM2.Λ') →
      (k : Turing.PartrecToTM2.Cont') → Q = Turing.PartrecToTM2.Λ'.ret k → motive (Turing.PartrecToTM2.Λ'.ret k)),
  (match q₁.pred q₂ with
    | Q@h:(Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) => h_1 Q p k₁ k₂ q h
    | Q@h:(Turing.PartrecToTM2.Λ'.push k s q) => h_2 Q k s q h
    | Q@h:(Turing.PartrecToTM2.Λ'.read q) => h_3 Q q h
    | Q@h:(Turing.PartrecToTM2.Λ'.clear p k q) => h_4 Q p k q h
    | Q@h:q.copy => h_5 Q q h
    | Q@h:q.succ => h_6 Q q h
    | Q@h:(q₁.pred q₂) => h_7 Q q₁ q₂ h
    | Q@h:(Turing.PartrecToTM2.Λ'.ret k) => h_8 Q k h) =
    h_7 (q₁.pred q₂) q₁ q₂ ⋯
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.evalLazyEntry : {α : Type} →
  Array α ×
      Lean.Meta.LazyDiscrTree.TrieIndex × Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex →
    Lean.Meta.LazyDiscrTree.LazyEntry α →
      Lean.Meta.LazyDiscrTree.MatchM α
        (Array α ×
          Lean.Meta.LazyDiscrTree.TrieIndex × Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex)
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.comap_id : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (C : PointedCone R E), PointedCone.comap LinearMap.id C = C
-- Mathlib.Topology.Order.OrderClosed
nhdsWithin_Icc_eq_nhdsLE : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → nhdsWithin b (Set.Icc a b) = nhdsWithin b (Set.Iic b)
-- Mathlib.Tactic.Linter.TextBased
/-- Lint a collection of input strings for disallowed unicode characters.

This is implemented using an allowlist, see
`Mathlib.Linter.TextBased.UnicodeLinter.isAllowedCharacter`.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.unicodeLinter : Mathlib.Linter.TextBased.TextbasedLinter✝
-- Mathlib.CategoryTheory.Limits.Final
/-- Given a colimit cocone over `G : D ⥤ E` we can construct a colimit cocone over `F ⋙ G`.  -/
CategoryTheory.Functor.Final.colimitCoconeComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [F.Final] →
            {E : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} E] →
                {G : CategoryTheory.Functor D E} →
                  CategoryTheory.Limits.ColimitCocone G → CategoryTheory.Limits.ColimitCocone (F.comp G)
-- Mathlib.Data.Quot
/-- A version of `Quotient.ind₂` taking `{s₁ : Setoid α} {s₂ : Setoid β}` as implicit arguments
instead of instance arguments.  -/
Quotient.ind₂' : ∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁ → Quotient s₂ → Prop},
  (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → ∀ (q₁ : Quotient s₁) (q₂ : Quotient s₂), p q₁ q₂
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.mono : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {s t : Set X},
  IsCoveringMapOn f s → t ⊆ s → IsCoveringMapOn f t
-- Mathlib.Data.Sum.Order
WithBot.orderIsoPUnitSumLex_toLex : ∀ {α : Type u_1} [inst : LE α] (a : α), WithBot.orderIsoPUnitSumLex ↑a = toLex (Sum.inr a)
-- Lean.Setup
Lean.instReprModuleSetup : Repr Lean.ModuleSetup
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.adjoint_toLinearMap_eq_symm : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  {K : Type u_6} [inst_3 : NormedAddCommGroup K] [inst_4 : InnerProductSpace 𝕜 K] [inst_5 : FiniteDimensional 𝕜 H]
  [inst_6 : FiniteDimensional 𝕜 K] (e : H ≃ₗᵢ[𝕜] K), LinearMap.adjoint ↑e.toLinearEquiv = ↑e.symm.toLinearEquiv
-- Mathlib.Algebra.Group.Defs
mul_div_assoc : ∀ {G : Type u_1} [inst : DivInvMonoid G] (a b c : G), a * b / c = a * (b / c)
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_rpow : ∀ {x : ENNReal} {y : ℝ}, (x ^ y).log = ↑y * x.log
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_mul : ∀ {a b : ℕ} (ha : a < 2 ^ 16) (hb : b < 2 ^ 16) (hab : a * b < 2 ^ 16),
  UInt16.ofNatLT (a * b) hab = UInt16.ofNatLT a ha * UInt16.ofNatLT b hb
-- Mathlib.Data.List.Sort
List.mergeSort_eq_self : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] [Std.Total r] [IsTrans α r] [Std.Antisymm r] {l : List α},
  List.Pairwise r l → (l.mergeSort fun x1 x2 => decide (r x1 x2)) = l
-- Init.Data.String.Lemmas.Search
String.Slice.Pos.le_find : ∀ {ρ : Type} {σ : String.Slice → Type}
  [inst : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [inst_1 : (s : String.Slice) → Std.IteratorLoop (σ s) Id Id] {s : String.Slice} (pos : s.Pos) (pattern : ρ)
  [inst_2 : String.Slice.Pattern.ToForwardSearcher pattern σ], pos ≤ pos.find pattern
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
MeasureTheory.Measure.IicSnd.eq_1 : ∀ {α : Type u_1} {mα : MeasurableSpace α} (ρ : MeasureTheory.Measure (α × ℝ)) (r : ℝ),
  ρ.IicSnd r = (ρ.restrict (Set.univ ×ˢ Set.Iic r)).fst
-- Mathlib.Data.Matrix.Basic
Matrix.map_pow : ∀ {m : Type u_2} [inst : Fintype m] [inst_1 : DecidableEq m] {α : Type u_14} {β : Type u_15} [inst_2 : Semiring α]
  [inst_3 : Semiring β] (M : Matrix m m α) (f : α →+* β) (a : ℕ), (M ^ a).map ⇑f = M.map ⇑f ^ a
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- `Iotop a b` is the interval `Ioo a b` if `b` is not top, and `Ioc a b` if `b` is top.
This makes sure that any element which is not bot belongs to an interval `Iotop a b`, and also
that these intervals are all open. These two properties together are important in the proof of
`StieltjesFunction.outer_Ioc`.  -/
Iotop : {R : Type u_1} → [LinearOrder R] → R → R → Set R
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.T_natAbs : ∀ (R : Type u_1) [inst : CommRing R] (n : ℤ), Polynomial.Chebyshev.T R ↑n.natAbs = Polynomial.Chebyshev.T R n
-- Mathlib.Logic.Equiv.Basic
/-- If `α` is equivalent to `β`, then `Unique α` is equivalent to `Unique β`.  -/
Equiv.uniqueCongr : {α : Sort u_1} → {β : Sort u_4} → α ≃ β → Unique α ≃ Unique β
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_C_succ : ∀ {R : Type u} [inst : Semiring R] {r : R} {n : ℕ}, (Polynomial.C r).coeff (n + 1) = 0
-- Mathlib.Topology.Algebra.Star.Unitary
instContinuousInvSubtypeMemSubmonoidUnitaryOfContinuousStar : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : TopologicalSpace R] [ContinuousStar R],
  ContinuousInv ↥(unitary R)
-- Mathlib.Data.Fin.SuccPred
Fin.le_of_castSucc_lt_of_succ_lt : ∀ {n : ℕ} {a b : Fin (n + 1)} {i : Fin n}, i.castSucc < a → b < i.succ → b < a
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Finset.aestronglyMeasurable_fun_prod : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : CommMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousMul M] {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.AEStronglyMeasurable (fun a => ∏ i ∈ s, f i a) μ
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_nil : ∀ {α : Type u_1}, FreeMonoid.toList [] = []
-- Lean.Parser.Term
Lean.Parser.Term.letOptNondep.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.eq_zero_of_coe_mem_of_disjoint : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M}, Disjoint p q → ∀ {a : ↥p}, ↑a ∈ q → a = 0
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The center of a semiring acts commutatively on that semiring.  -/
Subring.center.smulCommClass_right : ∀ {R : Type u_3} [inst : Ring R], SMulCommClass R (↥(Subring.center R)) R
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.instInhabitedHom : (X : AlgebraicGeometry.LocallyRingedSpace) → Inhabited (X.Hom X)
-- Init.Sym.Lemmas
Lean.Sym.Char.lt_eq_false : ∀ (a b : Char), decide (a < b) = false → (a < b) = False
-- Mathlib.Analysis.Seminorm
/-- The supremum over a finite set of continuous seminorms is continuous.  -/
Seminorm.continuous_finsetSup : ∀ {𝕝 : Type u_6} {E : Type u_7} {ι : Type u_11} [inst : SeminormedRing 𝕝] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕝 E] [inst_3 : TopologicalSpace E] [IsTopologicalAddGroup E] {p : ι → Seminorm 𝕝 E} {s : Finset ι},
  (∀ i ∈ s, Continuous ⇑(p i)) → Continuous ⇑(s.sup p)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_insertMany_of_mem : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type v} [inst_2 : ForIn Id ρ α]
  [EquivBEq α] [LawfulHashable α], m.WF → ∀ {l : ρ} {k : α}, k ∈ m → k ∈ m.insertMany l
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.open_source' : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι), IsOpen (Z.localTrivAsPartialEquiv i).source
-- Mathlib.Algebra.Group.End
MulAut.conj.eq_1 : ∀ {G : Type u_3} [inst : Group G],
  MulAut.conj =
    {
      toFun := fun g =>
        { toFun := fun h => g * h * g⁻¹, invFun := fun h => g⁻¹ * h * g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ },
      map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Field.Periodic
Function.Antiperiodic.const_mul : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : DivisionSemiring α] [inst_1 : Neg β],
  Function.Antiperiodic f c → ∀ {a : α}, a ≠ 0 → Function.Antiperiodic (fun x => f (a * x)) (a⁻¹ * c)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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 : ℤ) {Z : CategoryTheory.Functor C C}
  (h : (CategoryTheory.Functor.id C).comp (CategoryTheory.shiftFunctor C 1) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.truncGEδLT n)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight (t.truncLTι n) (CategoryTheory.shiftFunctor C 1)) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_lt_ofReal : ∀ {K : Type u_1} [inst : RCLike K] {x y : ℝ}, ↑x < ↑y ↔ x < y
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- A version of `RCLike.inner_apply` that swaps the order of multiplication.  -/
RCLike.inner_apply' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (x y : 𝕜), inner 𝕜 x y = (starRingEnd 𝕜) x * y
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_eq_top : ∀ {R : Type u_2} [inst : NonAssocRing R] {S : Subring R}, S.op = ⊤ ↔ S = ⊤
-- Init.Data.Nat.Bitwise.Lemmas
Nat.decide_shiftRight_mod_two_eq_one : ∀ {x i : ℕ}, decide (x >>> i % 2 = 1) = x.testBit i
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroupClass.coe_sub : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G]
  (x y : ↥H), ↑(x - y) = ↑x - ↑y
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then
it is differentiable at `x`.  -/
HasFTaylorSeriesUpToOn.differentiableAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → n ≠ 0 → s ∈ nhds x → DifferentiableAt 𝕜 f x
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
/-- If `α` has at least `n` elements, then any `n`-pretransitive action on `α`
is `n`-pretransitive for any `m ≤ n`.

This version allows `α` to be infinite and uses `ENat.card`.
For `Finite α`, use `AddAction.isMultiplyPretransitive_of_le`.  -/
AddAction.isMultiplyPretransitive_of_le' : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {m n : ℕ}
  [AddAction.IsMultiplyPretransitive G α n], m ≤ n → ↑n ≤ ENat.card α → AddAction.IsMultiplyPretransitive G α m
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.coe_id : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁], ↑(ContinuousLinearMap.id R₁ M₁) = LinearMap.id
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β} {h : k' ∈ Std.DHashMap.Const.alter m k f},
  Std.DHashMap.Const.get (Std.DHashMap.Const.alter m k f) k' h =
    if heq : (k == k') = true then (f (Std.DHashMap.Const.get? m k)).get ⋯ else Std.DHashMap.Const.get m k' ⋯
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapWithPostcondition : ∀ {α β γ : Type w} {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] {f : β → Std.Iterators.PostconditionT m γ} (it : Std.IterM Id β),
  (Std.IterM.mapWithPostcondition f it).toList = List.mapM (fun x => (f x).run) it.toList.run
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_iff_utf8ByteSize_eq_zero : ∀ {s : String}, s.isEmpty = true ↔ s.utf8ByteSize = 0
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.neg_eq : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c → f (-c) = -f 0
-- Init.Core
/-- Decidable equality for PEmpty  -/
instDecidableEqPEmpty : DecidableEq PEmpty.{u_1}
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- Transfer a `DifferentialAlgebra` instance across a `AlgEquiv`.
 -/
DifferentialAlgebra.equiv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] {R : Type u_2} {R₂ : Type u_3} [inst_2 : CommRing R]
  [inst_3 : CommRing R₂] [inst_4 : Differential R₂] [inst_5 : Algebra A R] [inst_6 : Algebra A R₂]
  [DifferentialAlgebra A R₂] (h : R ≃ₐ[A] R₂), DifferentialAlgebra A R
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.Context.currNamespace : Lean.PrettyPrinter.Delaborator.Context → Lean.Name
-- Std.Sat.AIG.CNF
/-- Mix:
1. An assignment for AIG atoms
2. An assignment for auxiliary Tseitin variables
into an assignment that can be used by a CNF produced by our Tseitin transformation.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.mixAssigns : {aig : Std.Sat.AIG ℕ} → (ℕ → Bool) → (Fin aig.decls.size → Bool) → ℕ → Bool
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousAt_biInf : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {ι : Sort u_4} {δ : Type u_5} [inst_1 : CompleteLinearOrder δ]
  {p : ι → Prop} {f : (i : ι) → p i → α → δ},
  (∀ (i : ι) (hi : p i), UpperSemicontinuousAt (f i hi) x) →
    UpperSemicontinuousAt (fun x' => ⨅ i, ⨅ (hi : p i), f i hi x') x
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.coe_copy : ∀ {G : Type u_1} [inst : Group G] (K : Subgroup G) (s : Set G) (hs : s = ↑K), ↑(K.copy s hs) = s
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cochainsMap_zero : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H), groupCohomology.cochainsMap f 0 = 0
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.mem_filter : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I) {p : BoxIntegral.Box ι → Prop},
  J ∈ π.filter p ↔ J ∈ π ∧ p J
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- If the `R`-integral element `a : S` has coordinates `≤ y` with respect to some basis `b`,
its norm is less than `normBound abv b * y ^ dim S`.  -/
ClassGroup.norm_le : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) (a : S) {y : ℤ},
  (∀ (k : ι), abv ((bS.repr a) k) ≤ y) → abv ((Algebra.norm R) a) ≤ ClassGroup.normBound abv bS * y ^ Fintype.card ι
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.hasColimit_ι_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  (X : C), CategoryTheory.Limits.HasColimit ((CategoryTheory.Grothendieck.ι F X).comp G)
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.allTR_loop_congr : ∀ {n m : ℕ} (w : n = m) (f : (i : ℕ) → i < n → Bool) (j : ℕ) (h : j ≤ n),
  Nat.allTR.loop✝ n f j h = Nat.allTR.loop✝ m (fun i h => f i ⋯) j ⋯