mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Fin.Lemmas
Fin.castSucc_zero : ∀ {n : ℕ} [inst : NeZero n], Fin.castSucc 0 = 0
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderIdent.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- The product of two open partial homeomorphisms, as an open partial homeomorphism on the product
space.  -/
OpenPartialHomeomorph.prod : {X : Type u_1} →
  {X' : Type u_2} →
    {Y : Type u_3} →
      {Y' : Type u_4} →
        [inst : TopologicalSpace X] →
          [inst_1 : TopologicalSpace X'] →
            [inst_2 : TopologicalSpace Y] →
              [inst_3 : TopologicalSpace Y'] →
                OpenPartialHomeomorph X X' → OpenPartialHomeomorph Y Y' → OpenPartialHomeomorph (X × Y) (X' × Y')
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_ne_zero : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b : G₀}, a ≠ 0 → b ≠ 0 → a / b ≠ 0
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getKeyD_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : Std.DHashMap.Internal.AssocList α β} {a fallback : α},
  Std.DHashMap.Internal.AssocList.getKeyD a fallback l = Std.Internal.List.getKeyD a l.toList fallback
-- Mathlib.Data.Ordmap.Ordset
_private.Mathlib.Data.Ordmap.Ordset.0.Ordnode.size.match_1.splitter : {α : Type u_1} →
  (motive : Ordnode α → Sort u_2) →
    (x : Ordnode α) →
      (Unit → motive Ordnode.nil) →
        ((sz : ℕ) → (l : Ordnode α) → (x : α) → (r : Ordnode α) → motive (Ordnode.node sz l x r)) → motive x
-- Init.Data.SInt.Lemmas
Int64.toBitVec_inj : ∀ {a b : Int64}, a.toBitVec = b.toBitVec ↔ a = b
-- Mathlib.RingTheory.Finiteness.Basic
RingHom.Finite.of_comp_finite : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : CommRing C]
  {f : A →+* B} {g : B →+* C}, (g.comp f).Finite → g.Finite
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `B` is an integral extension of an integrally closed domain `A`, then `IsGaloisGroup` for
their fraction fields implies `IsGaloisGroup` for these rings.  -/
IsGaloisGroup.of_isFractionRing : ∀ (G : Type u_1) (A : Type u_2) (B : Type u_3) (K : Type u_4) (L : Type u_5) [inst : Group G] [inst_1 : CommRing A]
  [inst_2 : CommRing B] [inst_3 : MulSemiringAction G B] [inst_4 : Algebra A B] [inst_5 : Field K] [inst_6 : Field L]
  [inst_7 : Algebra K L] [inst_8 : Algebra A K] [inst_9 : Algebra B L] [inst_10 : Algebra A L] [IsFractionRing A K]
  [IsFractionRing B L] [IsScalarTower A K L] [IsScalarTower A B L] [inst_15 : MulSemiringAction G L]
  [SMulDistribClass G B L] [hGKL : IsGaloisGroup G K L] [IsIntegrallyClosed A] [Algebra.IsIntegral A B],
  IsGaloisGroup G A B
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_add : ∀ {R : Type u} [inst : Semiring R] {f g : Polynomial R},
  Polynomial.derivative (f + g) = Polynomial.derivative f + Polynomial.derivative g
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.toNeg : {α : Type u} → [self : Lean.Grind.Ring α] → Neg α
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuousOn_primitive_Icc : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
  {f : ℝ → E} [MeasureTheory.NullSingletonClass μ],
  MeasureTheory.IntegrableOn f (Set.Icc a b) μ → ContinuousOn (fun x => ∫ (t : ℝ) in Set.Icc a x, f t ∂μ) (Set.Icc a b)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {s : Set (β × γ)},
  MeasurableSet s →
    ∀ (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ] (η : ProbabilityTheory.Kernel (α × β) γ)
      [ProbabilityTheory.IsSFiniteKernel η] (a : α),
      ((κ.compProd η) a) s = ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂κ a
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode.fixed.inj : ∀ {n n_1 : ℕ},
  Std.Http.Protocol.H1.Machine.BodyMode.fixed✝ n = Std.Http.Protocol.H1.Machine.BodyMode.fixed✝ n_1 → n = n_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The braiding isomorphism can be passed through a map by swapping the order.  -/
CategoryTheory.Limits.biprod.braid_natural_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ W) {Z_1 : C}
  (h : W ⊞ Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding Y W).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X Z).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map g f) h)
-- Mathlib.CategoryTheory.Elementwise
CategoryTheory.IsIso.inv_hom_id_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f]
  {F : C → C → Type uF} {carrier : C → Type w} {instFunLike : (X Y : C) → FunLike (F X Y) (carrier X) (carrier Y)}
  [inst_1 : CategoryTheory.ConcreteCategory C F] (x : carrier Y),
  (CategoryTheory.ConcreteCategory.hom f) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.inv f)) x) = x
-- Mathlib.GroupTheory.Subgroup.Centralizer
AddSubgroup.centralizer_closure : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G),
  AddSubgroup.centralizer ↑(AddSubgroup.closure s) = AddSubgroup.centralizer s
-- Mathlib.CategoryTheory.Action.Basic
Action.resCongr_hom : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] {f f' : G →* H} (h : f = f'),
  (Action.resCongr V h).hom = { app := fun X => (Action.mkIso (CategoryTheory.Iso.refl X.V) ⋯).hom, naturality := ⋯ }
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk : ∀ {M : Type u_3} [inst : AddCommMonoid M] (f : ℕ × ℕ → M) (n : ℕ),
  ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, f ij = ∑ k ∈ Finset.range n.succ, f (k, n - k)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_sq_iff₀ : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : LinearOrder M₀] [PosMulStrictMono M₀] {a : M₀}
  [ZeroLEOneClass M₀], 0 ≤ a → (1 ≤ a ^ 2 ↔ 1 ≤ a)
-- Mathlib.CategoryTheory.Core
CategoryTheory.coreCategory_comp_iso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {x y z : CategoryTheory.Core C} (f : x ⟶ y) (g : y ⟶ z),
  (CategoryTheory.CategoryStruct.comp f g).iso = f.iso ≪≫ g.iso
-- Mathlib.Order.Hom.Basic
/-- Converts an `OrderIso` into a `RelIso (>) (>)`.  -/
OrderIso.toRelIsoGT : {α : Type u_2} →
  {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → α ≃o β → (fun x1 x2 => x2 < x1) ≃r fun x1 x2 => x2 < x1
-- Mathlib.Algebra.Order.Rearrangement
/-- **Rearrangement Inequality**: Pointwise scalar multiplication of `f` and `g` is maximized when
`f` and `g` monovary together. Stated by permuting the entries of `f`.  -/
Monovary.sum_comp_perm_smul_le_sum_smul : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Monovary f g → ∑ i, f (σ i) • g i ≤ ∑ i, f i • g i
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Finset.Ioc a b ↔ a < x ∧ x ≤ b
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Compute the Mellin transform of the modifying term used to kill off the constants at
`0` and `∞`.  -/
WeakFEPair.f_modif_aux2 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) [CompleteSpace E] {s : ℂ},
  P.k < s.re → mellin (fun x => P.f_modif x - P.f x + P.f₀) s = (1 / s) • P.f₀ + (P.ε / (↑P.k - s)) • P.g₀
-- Mathlib.CategoryTheory.Square
/-- Flipping a square by switching the top-right and the bottom-left objects.  -/
CategoryTheory.Square.flip : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Square C → CategoryTheory.Square C
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.structureMapLM_apply : ∀ (𝕜 : 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] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ}
  (f : ContDiffMapSupportedIn E F n K),
  ⇑((ContDiffMapSupportedIn.structureMapLM 𝕜 n i) f) = if ↑i ≤ n then iteratedFDeriv ℝ i ⇑f else 0
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone_lift : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ C) {c : CategoryTheory.Limits.Cone F}
  (hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeRightOpOfCone c))
  (s : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone F hc).lift s =
    (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.yz.eq_1 : ∀ {a : ℕ} (a1 : 1 < a) (n : ℕ), Pell.yz a1 n = ↑(Pell.yn a1 n)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
PresheafOfModules.monoidalCategory : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
      CategoryTheory.MonoidalCategory (PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)))
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_eq_iff : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ},
  n ≠ 0 → (⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ ↑n)
-- Init.MetaTypes
Lean.Meta.instBEqEtaStructMode.beq : Lean.Meta.EtaStructMode → Lean.Meta.EtaStructMode → Bool
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey?_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t₁ \ t₂).getKey? k = if k ∈ t₂ then none else t₁.getKey? k
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.of_equiv : ∀ {R : Type u_4} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallySmooth R A] (e : A ≃ₐ[R] B), Algebra.FormallySmooth R B
-- Mathlib.RingTheory.PowerSeries.PiTopology
PowerSeries.WithPiTopology.multipliable_one_sub_X_pow : ∀ (R : Type u_2) [inst : CommRing R] [inst_1 : TopologicalSpace R], Multipliable fun n => 1 - PowerSeries.X ^ (n + 1)
-- Mathlib.Algebra.BigOperators.Finprod
add_finsum_cond_ne : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} (a : α),
  Function.HasFiniteSupport f → f a + ∑ᶠ (i : α) (_ : i ≠ a), f i = ∑ᶠ (i : α), f i
-- Mathlib.Data.Finset.Dedup
List.toFinset_coe : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), (↑l).toFinset = l.toFinset
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.deg_one : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜], HomogeneousLocalization.NumDenSameDeg.deg 1 = 0
-- Mathlib.Logic.Nonempty
/-- Given `f : α → β`, if `α` is nonempty then `β` is also nonempty.
`Nonempty` cannot be a `functor`, because `Functor` is restricted to `Type`.  -/
Nonempty.map : ∀ {α : Sort u_3} {β : Sort u_4} (f : α → β), Nonempty α → Nonempty β
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.associator_hom_comp_tensorHom_tensorHom_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {W X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f : X₁ ⟶ X₂) (g : Y₁ ⟶ Y₂) (h : Z₁ ⟶ Z₂)
  (gh : CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂ ⟶ W),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g h) gh)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X₂) gh))
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_erase_le_maxKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : (t.erase k).isEmpty = false}, (cmp ((t.erase k).maxKey he) (t.maxKey ⋯)).isLE = true
-- Init.Data.Int.Gcd
Int.gcd_add_mul_right_left : ∀ (m n k : ℤ), (n + k * m).gcd m = n.gcd m
-- Init.Data.Bool
/-- This should not be turned on globally as an instance because it degrades performance in Mathlib,
but may be used locally.
 -/
boolRelToRel : {α : Sort u_1} → Coe (α → α → Bool) (α → α → Prop)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A pointed convex cone defines a preorder.  -/
ConvexCone.toPreorder : {R : Type u_2} →
  {G : Type u_3} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : AddCommGroup G] → [inst_3 : SMul R G] → (C : ConvexCone R G) → C.Pointed → Preorder G
-- Std.Time.Internal.Bounded
/-- Expand the range of a bounded value.
 -/
Std.Time.Internal.Bounded.LE.expand : {lo hi nhi nlo : ℤ} → Std.Time.Internal.Bounded.LE lo hi → hi ≤ nhi → nlo ≤ lo → Std.Time.Internal.Bounded.LE nlo nhi
-- Mathlib.Data.Complex.Basic
Complex.natCast_im : ∀ (n : ℕ), (↑n).im = 0
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.ofIsRightAdjoint.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (left : CategoryTheory.Functor C D) [inst_2 : left.IsRightAdjoint],
  CategoryTheory.Adjunction.ofIsRightAdjoint left = ⋯.some
-- Mathlib.NumberTheory.FunctionField
FunctionField.ringOfIntegers.instIsDomainSubtypeMemSubalgebraPolynomial : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra (Polynomial F) K],
  IsDomain ↥(FunctionField.ringOfIntegers F K)
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- When lowered to a prop, `Matrix.invertibleOfSubmatrixEquivInvertible` forms an `iff`.  -/
Matrix.isUnit_submatrix_equiv : ∀ {m : Type u} {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α]
  [inst_3 : Fintype m] [inst_4 : DecidableEq m] {A : Matrix m m α} (e₁ e₂ : n ≃ m),
  IsUnit (A.submatrix ⇑e₁ ⇑e₂) ↔ IsUnit A
-- Mathlib.NumberTheory.PellMatiyasevic
/-- Every solution to **Pell's equation** is recursively obtained from the initial solution
`(1,0)` using the recursion `pell`.  -/
Pell.eq_pell : ∀ {a : ℕ} (a1 : 1 < a) {x y : ℕ}, x * x - Pell.d✝ a1 * y * y = 1 → ∃ n, x = Pell.xn a1 n ∧ y = Pell.yn a1 n
-- Mathlib.FieldTheory.IntermediateField.ExtendRight
IntermediateField.coe_extendRightEquiv : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (M : Type u_3) [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [inst_6 : IsScalarTower K L M]
  (a : ↥F), ↑((F.extendRightEquiv M) a) = (algebraMap (↥F) M) a
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- If two sets `s` and `t` are included in a set `u`, and `μ s + μ t > μ u`,
then `s` intersects `t`. Version assuming that `s` is measurable.  -/
MeasureTheory.nonempty_inter_of_measure_lt_add' : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s t u : Set α},
  MeasurableSet s → s ⊆ u → t ⊆ u → μ u < μ s + μ t → (s ∩ t).Nonempty
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [inst_2 : IsCyclotomicExtension {p ^ k} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  hζ.subOneIntegralPowerBasisOfPrimePow.gen = ⟨ζ - 1, ⋯⟩
-- Init.Data.Rat.Basic
Rat.instInv : Inv ℚ
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT_hom_ι_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (X : C) {Z : C} (h_1 : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncLEIsoTruncLT a b h).hom.app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncLTι b).app X) h_1) =
    CategoryTheory.CategoryStruct.comp ((t.truncLEι a).app X) h_1
-- Mathlib.Order.Interval.Set.Basic
Set.Ioo_subset_Icc_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioo a b ⊆ Set.Icc a b
-- Mathlib.Order.Filter.Finite
/-- **Alias** of `Set.Finite.eventuallyEq_iInter`. -/
Filter.EventuallyEq.biInter : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
  s.Finite → ∀ {f g : ι → Set α}, (∀ i ∈ s, f i =ᶠ[l] g i) → ⋂ i ∈ s, f i =ᶠ[l] ⋂ i ∈ s, g i
-- Mathlib.Analysis.Normed.Module.Span
ContinuousLinearEquiv.toSpanNonzeroSingleton_apply_coe : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (x : E) (h : x ≠ 0) (x_1 : 𝕜), ↑((ContinuousLinearEquiv.toSpanNonzeroSingleton 𝕜 x h) x_1) = x_1 • x
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.entryAtIdxD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → ℕ → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (n : ℕ) (fallback : (a : α) × β a)
  (h_1 : (x : ℕ) → (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf x fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (n : ℕ) → (fallback : (a : α) × β a) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r) n fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback with
    | Std.DTreeMap.Internal.Impl.leaf, x, fallback => h_1 x fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l r, n, fallback => h_2 size k v l r n fallback) =
    h_2 size k v l r n fallback
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
Continuous.integrableOn_Ioc : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} [OpensMeasurableSpace X] {f : X → E} {a b : X}
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_5 : Preorder X] [CompactIccSpace X] [T2Space X],
  Continuous f → MeasureTheory.IntegrableOn f (Set.Ioc a b) μ
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- `C ⥤ᵣ D` denotes right exact functors `C ⥤ D`  -/
CategoryTheory.«term_⥤ᵣ_» : Lean.TrailingParserDescr
-- Batteries.Data.List.Lemmas
List.idxOf_eq_getD_idxOf? : ∀ {α : Type u_1} [inst : BEq α] (a : α) (l : List α), List.idxOf a l = (List.idxOf? a l).getD l.length
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_op_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), S.op.Exact ↔ S.Exact
-- Mathlib.Order.InitialSeg
InitialSeg.mem_range_of_le : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} {b : β} [inst_1 : LT α] (f : α ≤i β),
  b ≤ f a → b ∈ Set.range ⇑f
-- Mathlib.Algebra.Group.Action.Pi
/-- If `α i` has a faithful scalar action for a given `i`, then so does `Π i, α i`. This is
not an instance as `i` cannot be inferred.  -/
Pi.faithfulSMul_at : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → SMul M (α i)] [∀ (i : ι), Nonempty (α i)] (i : ι)
  [FaithfulSMul M (α i)], FaithfulSMul M ((i : ι) → α i)
-- Mathlib.Analysis.Complex.Conformal
/-- Construct a continuous complex-linear map from a continuous real-linear map `ℓ` that maps `I` to
`I • ℓ 1`.
 -/
ContinuousLinearMap.complexOfReal : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℂ E] → (ℓ : ℂ →L[ℝ] E) → ℓ Complex.I = Complex.I • ℓ 1 → ℂ →L[ℂ] E
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.iso_map_bijective : ∀ {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [inst : (i : I) → Decidable (J i)],
  Function.Bijective ⇑(Profinite.NobelingProof.iso_map C J)
-- Mathlib.Analysis.SumIntegralExpDecay
sum_Ico_pow_mul_exp_neg_le : ∀ {k M : ℕ} {c : ℝ},
  0 < c → ∑ i ∈ Finset.Ico 0 M, ↑i ^ k * Real.exp (-(c * ↑i)) ≤ Real.exp c * ↑k.factorial / c ^ (k + 1)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesIsoRightHomology_inv_hom_id_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] (hg : S.g = 0) {Z : C} (h : S.rightHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.rightHomologyι
      (CategoryTheory.CategoryStruct.comp (S.opcyclesIsoRightHomology hg).hom h) =
    h
-- Init.Data.Nat.Div.Basic
Nat.mod_one : ∀ (x : ℕ), x % 1 = 0
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.IterM.step_intermediateZip.match_1.splitter : {α₁ β₁ : Type u_1} →
  {m : Type u_1 → Type u_2} →
    [inst : Std.Iterator α₁ m β₁] →
      {it₁ : Std.IterM m β₁} →
        (motive : it₁.Step → Sort u_3) →
          (x : it₁.Step) →
            ((it₁' : Std.IterM m β₁) →
                (out : β₁) →
                  (hp : it₁.IsPlausibleStep (Std.IterStep.yield it₁' out)) → motive ⟨Std.IterStep.yield it₁' out, hp⟩) →
              ((it₁' : Std.IterM m β₁) →
                  (hp : it₁.IsPlausibleStep (Std.IterStep.skip it₁')) → motive ⟨Std.IterStep.skip it₁', hp⟩) →
                ((hp : it₁.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, hp⟩) → motive x
-- Std.Time.Format.Modifier
/-- Only the hour is output (e.g., "+01")
 -/
Std.Time.OffsetX.hour : Std.Time.OffsetX
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The homology functor `DerivedCategory.Plus C ⥤ C` in degree `n : ℤ`.  -/
DerivedCategory.Plus.homologyFunctor : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → ℤ → CategoryTheory.Functor (DerivedCategory.Plus C) C
-- Init.Data.Vector.Algebra
Vector.add_comm : ∀ {α : Type u_1} {n : ℕ} [inst : Add α], (∀ (x y : α), x + y = y + x) → ∀ (xs ys : Vector α n), xs + ys = ys + xs
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_disjiUnion : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : CommMonoid M] {f : ι → M} (s : Finset κ) (t : κ → Finset ι)
  (h : (↑s).PairwiseDisjoint t), ∏ x ∈ s.disjiUnion t h, f x = ∏ i ∈ s, ∏ x ∈ t i, f x
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.associator_map_inl_inr : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {X Y : D} (f : X ⟶ Y),
  (CategoryTheory.sum.associator C D E).map
      ((CategoryTheory.Sum.inl_ (C ⊕ D) E).map ((CategoryTheory.Sum.inr_ C D).map f)) =
    (CategoryTheory.Sum.inr_ C (D ⊕ E)).map ((CategoryTheory.Sum.inl_ D E).map f)