mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).inv (F.map h))
      (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv)
        (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv
          (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv)))
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_intCast : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (z : ℤ), ↑↑z = ↑z
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc).ι = CategoryTheory.Limits.Fork.ι c
-- Mathlib.NumberTheory.Padics.Complex
/-- The coercion of the valuation of `x : PadicAlgCl p` to `ℝ` agrees with its norm.  -/
PadicAlgCl.valuation_coe : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : PadicAlgCl p), ↑(Valued.v x) = ‖x‖
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanImportMetaKind.toJson : Lean.Lsp.LeanImportMetaKind → Lean.Json
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.alternatingCofaceMapComplex_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.CosimplicialObject C} (f : X ⟶ Y),
  (AlgebraicTopology.alternatingCofaceMapComplex C).map f = AlgebraicTopology.AlternatingCofaceMapComplex.map f
-- Mathlib.Data.Set.Function
Set.SurjOn.comp_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ} {s : Set β} {t : Set γ},
  Function.Surjective f → Set.SurjOn g s t → Set.SurjOn (g ∘ f) (f ⁻¹' s) t
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated differential within a set `s` at a point `x` is not modified if one intersects
`s` with an open set containing `x`.  -/
iteratedFDerivWithin_inter_open : ∀ {𝕜 : 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 u : Set E}
  {f : E → F} {x : E} {n : ℕ}, IsOpen u → x ∈ u → iteratedFDerivWithin 𝕜 n f (s ∩ u) x = iteratedFDerivWithin 𝕜 n f s x
-- Mathlib.RingTheory.Binomial
Ring.multichoose_one_right : ∀ {R : Type u_1} [inst : AddCommMonoid R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [inst_3 : MulOneClass R]
  [NatPowAssoc R] (r : R), Ring.multichoose r 1 = r
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_addNatEmb_Icc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), Finset.map (Fin.addNatEmb m) (Finset.Icc i j) = Finset.Icc (i.addNat m) (j.addNat m)
-- Mathlib.GroupTheory.Perm.DomMulAct
DomMulAct.stabilizerEquiv_invFun_eq : ∀ {α : Type u_1} {ι : Type u_2} {f : α → ι} (g : (i : ι) → Equiv.Perm { a // f a = i }) {a : α} {i : ι} (h : f a = i),
  DomMulAct.stabilizerEquiv_invFun g a = ↑((g i) ⟨a, h⟩)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.lt_norm0 : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] [inst_1 : LT α] (lhs rhs : α), (lhs < rhs) = (lhs < rhs + ↑0)
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresentationData.mk.injEq : ∀ (name : Lean.Name) (userName : String) (html : ProofWidgets.Html) (name_1 : Lean.Name) (userName_1 : String)
  (html_1 : ProofWidgets.Html),
  ({ name := name, userName := userName, html := html } = { name := name_1, userName := userName_1, html := html_1 }) =
    (name = name_1 ∧ userName = userName_1 ∧ html = html_1)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.min!.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] (t t_1 : Std.ExtTreeSet α cmp),
  t = t_1 → t.min! = t_1.min!
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
riemannZetaSummandHom.eq_1 : ∀ {s : ℂ} (hs : s ≠ 0),
  riemannZetaSummandHom hs = { toFun := fun n => ↑n ^ (-s), map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.MeasureTheory.Integral.CircleAverage
/-- Circle averages respect the `≤` relation.
 -/
Real.circleAverage_mono : ∀ {c : ℂ} {R : ℝ} {f₁ f₂ : ℂ → ℝ},
  CircleIntegrable f₁ c R →
    CircleIntegrable f₂ c R →
      (∀ x ∈ Metric.sphere c |R|, f₁ x ≤ f₂ x) → Real.circleAverage f₁ c R ≤ Real.circleAverage f₂ c R
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.instModule : {α : Type u_1} →
  {𝕜 : Type u_2} →
    {E : Type u_4} →
      {m : MeasurableSpace α} →
        {p : ENNReal} →
          {μ : MeasureTheory.Measure α} →
            [inst : NormedAddCommGroup E] →
              [inst_1 : NormedRing 𝕜] → [inst_2 : Module 𝕜 E] → [IsBoundedSMul 𝕜 E] → Module 𝕜 ↥(MeasureTheory.Lp E p μ)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany_one : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] {a : α}, Std.PRange.succMany 1 a = Std.PRange.succ a
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHom.id_comp : ∀ {A : Type u_1} {B : Type u_2} [inst : NonUnitalNonAssocSemiring A] [inst_1 : Star A]
  [inst_2 : NonUnitalNonAssocSemiring B] [inst_3 : Star B] (f : A →⋆ₙ+* B), (NonUnitalStarRingHom.id B).comp f = f
-- Mathlib.Data.Fin.Tuple.Basic
Fin.cons_le : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} [inst : (i : Fin (n + 1)) → Preorder (α i)] {x : α 0}
  {q : (i : Fin (n + 1)) → α i} {p : (i : Fin n) → α i.succ}, Fin.cons x p ≤ q ↔ x ≤ q 0 ∧ p ≤ Fin.tail q
-- Mathlib.Data.Subtype
Subtype.map_comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {p : α → Prop} {q : β → Prop} {r : γ → Prop} {x : Subtype p} (f : α → β)
  (h : ∀ (a : α), p a → q (f a)) (g : β → γ) (l : ∀ (a : β), q a → r (g a)),
  Subtype.map g l (Subtype.map f h x) = Subtype.map (g ∘ f) ⋯ x
-- Lean.Level
Lean.Level.PP.Context : Type
-- Mathlib.GroupTheory.Exponent
MulOpposite.exponent : ∀ {G : Type u} [inst : Monoid G], Monoid.exponent Gᵐᵒᵖ = Monoid.exponent G
-- Mathlib.Data.PFun
PFun.ext : ∀ {α : Type u_1} {β : Type u_2} {f g : α →. β}, (∀ (a : α) (b : β), b ∈ f a ↔ b ∈ g a) → f = g
-- Mathlib.Util.Notation3
/-- Create a `Term` that represents a matcher for `foldr` notation.
Reminder: `( lit ","* => foldr (x y => scopedTerm) init)`  -/
Mathlib.Notation3.mkFoldrMatcher : Lean.Name →
  Lean.Name →
    Lean.Name →
      Lean.Term →
        Lean.Term → Array Lean.Name → OptionT Lean.Elab.TermElabM (List Mathlib.Notation3.DelabKey × Lean.Term)
-- Mathlib.LinearAlgebra.Multilinear.Pi
MultilinearMap.piFamily_single_left : ∀ {ι : Type uι} {κ : ι → Type uκ} {R : Type uR} {M : (i : ι) → κ i → Type uM} {N : ((i : ι) → κ i) → Type uN}
  [inst : Semiring R] [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (M i k)]
  [inst_2 : (p : (i : ι) → κ i) → AddCommMonoid (N p)] [inst_3 : (i : ι) → (k : κ i) → Module R (M i k)]
  [inst_4 : (p : (i : ι) → κ i) → Module R (N p)] [inst_5 : Fintype ι] [inst_6 : (i : ι) → DecidableEq (κ i)]
  (p : (i : ι) → κ i) (f : MultilinearMap R (fun i => M i (p i)) (N p)),
  MultilinearMap.piFamily (Pi.single p f) =
    (LinearMap.single R N p).compMultilinearMap (f.compLinearMap fun i => LinearMap.proj (p i))
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex_of_subsingleton : ∀ (𝕜 : Type u_2) (ι : Type u_1) [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : Fintype ι] [Subsingleton 𝕜],
  stdSimplex 𝕜 ι = Set.univ
-- Mathlib.NumberTheory.ClassNumber.Finite
ClassGroup.distinctElems.congr_simp : ∀ {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) (adm : abv.IsAdmissible) [inst_6 : Infinite R],
  ClassGroup.distinctElems bS adm = ClassGroup.distinctElems bS adm
-- Mathlib.Data.Finmap
Finmap.keysLookupEquiv_apply_coe_fst : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (s : Finmap β), (↑(Finmap.keysLookupEquiv s)).1 = s.keys
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_ne_top_of_nonempty_of_bounded`.

---

If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff
edistance.  -/
Metric.hausdorffEdist_ne_top_of_nonempty_of_bounded : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α},
  s.Nonempty → t.Nonempty → Bornology.IsBounded s → Bornology.IsBounded t → Metric.hausdorffEDist s t ≠ ⊤
-- Mathlib.FieldTheory.KummerExtension
/-- An arbitrary choice of `ⁿ√a` in the splitting field of `Xⁿ - a`.  -/
rootOfSplitsXPowSubC : {K : Type u} →
  [inst : Field K] →
    {n : ℕ} →
      0 < n →
        (a : K) →
          (L : Type u_2) →
            [inst_1 : Field L] →
              [inst_2 : Algebra K L] → [Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] → L
-- Mathlib.Order.Closure
LowerAdjoint.closure_union_closure_right : ∀ {α : Type u_1} {β : Type u_4} [inst : SetLike α β] [inst_1 : Preorder α] (l : LowerAdjoint SetLike.coe) (x y : α),
  l.toFun (↑x ∪ ↑(l.toFun ↑y)) = l.toFun (↑x ∪ ↑y)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.zero_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {σ₂₁ : R₂ →+* R} [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] [inst_8 : Subsingleton M]
  [inst_9 : Subsingleton M₂], LinearEquiv.symm 0 = 0
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Reinterpret a `ContinuousAddMonoidHom` as a `ContinuousMap`.  -/
ContinuousAddMonoidHom.toContinuousMap : {A : Type u_7} →
  {B : Type u_8} →
    [inst : AddMonoid A] →
      [inst_1 : AddMonoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → (A →ₜ+ B) → C(A, B)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_iff_toArray_perm : ∀ {α : Type u} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β},
  t₁.Equiv t₂ ↔ (Std.DTreeMap.Internal.Impl.Const.toArray t₁).Perm (Std.DTreeMap.Internal.Impl.Const.toArray t₂)
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.instHasTensorXTensorUnit_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C] {I : Type u_2}
  [inst_4 : AddMonoid I] {c : ComplexShape I} (K : HomologicalComplex C c) [inst_5 : DecidableEq I]
  [∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)],
  CategoryTheory.GradedObject.HasTensor K.X (HomologicalComplex.tensorUnit C c).X
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.basis.eq_1 : ∀ (R : Type u_7) (k : Type u_8) [inst : Semiring k],
  MonoidAlgebra.basis R k = { repr := MonoidAlgebra.coeffLinearEquiv k }
-- Mathlib.Analysis.Normed.Module.Bases
/-- The norm of any projection is bounded by the basis constant.  -/
UnconditionalSchauderBasis.norm_proj_le_nnnormProjBound : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] {β : Type u_3} (b : UnconditionalSchauderBasis β 𝕜 X) [CompleteSpace X] (A : Finset β),
  ‖GeneralSchauderBasis.proj b A‖ ≤ ↑b.nnnormProjBound
-- Mathlib.Order.Defs.Unbundled
trans_trichotomous_right : ∀ {α : Sort u_1} {r : α → α → Prop} [IsTrans α r] [Std.Trichotomous r] {a b c : α}, r a b → ¬r c b → r a c
-- Mathlib.Algebra.Group.Shrink
/-- Shrink `α` to a smaller universe preserves multiplication.  -/
Shrink.mulEquiv : {α : Type u_2} → [inst : Small.{v, u_2} α] → [inst_1 : Mul α] → Shrink.{v, u_2} α ≃* α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_maxKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α}, t.maxKey? = some km → t.getKey? km = some km
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_C_lt : ∀ {R : Type u} {a : R} [inst : Semiring R], (Polynomial.C a).degree < 1
-- Mathlib.Order.DirSupClosed
DirSupInaccOn.of_isEmpty : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] [IsEmpty α] {s : Set α}, DirSupInaccOn D s
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Pi.isoMk_inv : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {X Y : (i : I) → C i}
  (iso : (i : I) → X i ≅ Y i) (i : I), (CategoryTheory.Pi.isoMk iso).inv i = (iso i).inv
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.jmp.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (args : Array (Lean.Compiler.LCNF.Arg pu))
  (fvarId_1 : Lean.FVarId) (args_1 : Array (Lean.Compiler.LCNF.Arg pu)),
  (Lean.Compiler.LCNF.Code.jmp fvarId args = Lean.Compiler.LCNF.Code.jmp fvarId_1 args_1) =
    (fvarId = fvarId_1 ∧ args = args_1)
-- Mathlib.RingTheory.Ideal.Prime
Ideal.primeCompl_bot : ∀ {α : Type u} [inst : Semiring α] [inst_1 : Nontrivial α] [inst_2 : NoZeroDivisors α], ⊥.primeCompl = nonZeroDivisors α
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.inr_φ_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.kernelCokernelCompSequence.φ f g)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h)) =
    CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.id Y) h
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.instZeroHomObjTopCommRingCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier : (X : TopCat) → (R : TopCommRingCat) → Zero (X ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.hasLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.HasLimitsOfShape J (Type u)
-- Mathlib.Analysis.Real.Sqrt
Real.sq_le : ∀ {x y : ℝ}, 0 ≤ y → (x ^ 2 ≤ y ↔ -√y ≤ x ∧ x ≤ √y)
-- Mathlib.Algebra.Order.Hom.Basic
map_pos_of_ne_zero : ∀ {F : Type u_2} {α : Type u_3} {β : Type u_4} [inst : FunLike F α β] [inst_1 : AddGroup α] [inst_2 : AddCommMonoid β]
  [inst_3 : LinearOrder β] [IsOrderedAddMonoid β] [AddGroupNormClass F α β] (f : F) {x : α}, x ≠ 0 → 0 < f x
-- Init.Prelude
/-- Converts a natural number to a 64-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than `2^64`.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.ofNatLT : (n : ℕ) → n < UInt64.size → UInt64
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.mulRight.eq_1 : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul Gᵐᵒᵖ G] (c : G),
  IsometryEquiv.mulRight c = { toEquiv := Equiv.mulRight c, isometry_toFun := ⋯ }
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : β → β}, (m.modify k f).size = m.size
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.uniqueHomFromTrivial.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C),
  A.uniqueHomFromTrivial =
    (have this := CategoryTheory.InducedCategory.homEquiv;
      this).unique
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.liftTruncLT_ι_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) {X Y : C} (f : X ⟶ Y) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
  [inst_6 : t.IsLE X n₀] {Z : C} (h_1 : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (t.liftTruncLT f n₀ n₁ h)
      (CategoryTheory.CategoryStruct.comp ((t.truncLTι n₁).app Y) h_1) =
    CategoryTheory.CategoryStruct.comp f h_1
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Algebra.Hom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C C} →
      {A₀ A₁ : CategoryTheory.Endofunctor.Algebra F} →
        (f : A₀.a ⟶ A₁.a) →
          autoParam (CategoryTheory.CategoryStruct.comp (F.map f) A₁.str = CategoryTheory.CategoryStruct.comp A₀.str f)
              CategoryTheory.Endofunctor.Algebra.Hom.h._autoParam →
            A₀.Hom A₁
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isOpenEmbedding_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsOpenEmbedding ⇑DomMulAct.mk
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
/-- A Lie-Rinehart subalgebra of a Lie-Rinehart algebra forms a Lie algebra.  -/
LieRinehartSubalgebra.lieAlgebra : {A : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : LieRing L] →
        [inst_2 : Module A L] →
          (L' : LieRinehartSubalgebra A L) →
            [inst_3 : LieRingModule L A] →
              [inst_4 : LieRinehartRing A L] →
                (R : Type u_3) →
                  [inst_5 : CommRing R] →
                    [inst_6 : Algebra R A] → [inst_7 : LieAlgebra R L] → [LieRinehartAlgebra R A L] → LieAlgebra R ↥L'
-- Mathlib.MeasureTheory.Group.AEStabilizer
MulAction.mem_aestabilizer : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.SMulInvariantMeasure G α μ] {g : G} {s : Set α},
  g ∈ MulAction.aestabilizer G μ s ↔ g • s =ᵐ[μ] s
-- Mathlib.Data.Int.Cast.Lemmas
Commute.intCast_mul_intCast_mul : ∀ {α : Type u_3} [inst : Ring α] {a b : α}, Commute a b → ∀ (m n : ℤ), Commute (↑m * a) (↑n * b)
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
instFaithfulFGAlgCatUliftFunctor : ∀ (R : Type u) [inst : CommRing R], (FGAlgCat.uliftFunctor R).Faithful
-- Mathlib.Data.Quot
nonempty_quotient_iff : ∀ {α : Sort u_1} (s : Setoid α), Nonempty (Quotient s) ↔ Nonempty α
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a},
  (↑m).WF → (↑(Std.DHashMap.Internal.Raw₀.map f m)).isEmpty = (↑m).isEmpty
-- Mathlib.NumberTheory.ModularForms.Basic
/-- `ModularFormClass F Γ k` says that `F` is a type of bundled functions that extend
`SlashInvariantFormClass` by requiring that the functions be holomorphic and bounded
at all cusps.  -/
ModularFormClass : (F : Type u_2) → outParam (Subgroup (GL (Fin 2) ℝ)) → outParam ℤ → [FunLike F UpperHalfPlane ℂ] → Prop
-- Mathlib.GroupTheory.Perm.Sign
/-- `SignType.sign` of a permutation returns the signature or parity of a permutation, `1` for even
permutations, `-1` for odd permutations. It is the unique surjective group homomorphism from
`Perm α` to the group with two elements.  -/
Equiv.Perm.sign : {α : Type u} → [DecidableEq α] → [Fintype α] → Equiv.Perm α →* ℤˣ
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- The mapping cone of a morphism of cochain complexes indexed by `ℤ`.  -/
CochainComplex.mappingCone : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {F G : CochainComplex C ℤ} → (φ : F ⟶ G) → [HomologicalComplex.HasHomotopyCofiber φ] → CochainComplex C ℤ
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_ssubset_compl : ∀ {α : Type u_1} {s t : Finset α} [inst : Fintype α] [inst_1 : DecidableEq α], sᶜ ⊂ tᶜ ↔ t ⊂ s
-- Mathlib.Computability.Primrec.Basic
Primrec₂.nat_iff' : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ},
  Primrec₂ f ↔ Primrec₂ fun m n => (Encodable.decode m).bind fun a => Option.map (f a) (Encodable.decode n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.cos_arctan_pos : ∀ (x : ℝ), 0 < Real.cos (Real.arctan x)
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
Multipliable.of_subsingleton_cod : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {L : SummationFilter β}
  [Subsingleton α], Multipliable f L
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- If a `VectorBundleCore` has the `IsContMDiff` mixin, then the vector bundle constructed from it
is a `C^n` vector bundle.  -/
VectorBundleCore.instContMDiffVectorBundle : ∀ {n : WithTop ℕ∞} {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
  [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] {ι : Type u_11} (Z : VectorBundleCore 𝕜 B F ι)
  [Z.IsContMDiff IB n], ContMDiffVectorBundle n F Z.Fiber IB
-- Mathlib.CategoryTheory.Filtered.Basic
/-- If `C` is cofiltered, and we have a functor `L : C ⥤ D` with a right adjoint,
then `D` is cofiltered.
 -/
CategoryTheory.IsCofiltered.of_left_adjoint : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (h : L ⊣ R), CategoryTheory.IsCofiltered D
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.lift_apply_of : ∀ {α : Type u} {β : Type v} [inst : AddCommGroup β] (f : α → β) (x : α),
  (FreeAbelianGroup.lift f) (FreeAbelianGroup.of x) = f x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.π_ofπ : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {P : C} (π : Y ⟶ P)
  (w : CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π),
  (CategoryTheory.Limits.Cofork.ofπ π w).π = π
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.toAdditive : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (G : Type u_4)
  [inst_2 : Group G] [inst_3 : MulAction G E], IsQuotientCoveringMap f G → IsAddQuotientCoveringMap f (Additive G)
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instInhabited : (A : Type u_3) → (E : Type u_4) → [Inhabited E] → Inhabited (WithCStarModule A E)
-- Mathlib.Analysis.Calculus.UniformLimitsDeriv
uniformCauchySeqOnFilter_of_deriv : ∀ {ι : Type u_1} {l : Filter ι} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {G : Type u_3}
  [inst_1 : NormedAddCommGroup G] [inst_2 : NormedSpace 𝕜 G] {f f' : ι → 𝕜 → G} {x : 𝕜} [IsRCLikeNormedField 𝕜],
  UniformCauchySeqOnFilter f' l (nhds x) →
    (∀ᶠ (n : ι × 𝕜) in l ×ˢ nhds x, HasDerivAt (f n.1) (f' n.1 n.2) n.2) →
      Cauchy (Filter.map (fun n => f n x) l) → UniformCauchySeqOnFilter f l (nhds x)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.IsSpanning.card_verts : ∀ {V : Type u} {G : SimpleGraph V} [inst : Fintype V] {G' : G.Subgraph} [inst_1 : Fintype ↑G'.verts],
  G'.IsSpanning → G'.verts.toFinset.card = Fintype.card V