mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.Cusps
/-- For a subgroup `𝒢` of `GL(2, R)`, this is the additive group of `x : R` such that
`±[1, x; 0, 1] ∈ 𝒢`.  -/
Subgroup.periods : {R : Type u_1} → [inst : Ring R] → Subgroup (GL (Fin 2) R) → AddSubgroup R
-- Lean.Server.InfoUtils
/-- `foldInfoTree.go` is like `foldInfoTree` but with an additional outer context parameter `ctx?`.  -/
_private.Lean.Server.InfoUtils.0.Lean.Elab.InfoTree.foldInfoTree.go : {α : Type u_1} →
  (Lean.Elab.ContextInfo → Lean.Elab.InfoTree → α → α) → Option Lean.Elab.ContextInfo → α → Lean.Elab.InfoTree → α
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.ext_iff : ∀ {M : Type u_1} [inst : AddZeroClass M] {S T : AddSubmonoid M}, S = T ↔ ∀ (x : M), x ∈ S ↔ x ∈ T
-- Mathlib.MeasureTheory.Measure.GiryMonad
MeasureTheory.Measure.bind_zero_right' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (m : MeasureTheory.Measure α),
  (m.bind fun x => 0) = 0
-- Std.Data.String.ToInt
String.toInt?_eq_some_of_toNat?_eq_some : ∀ {s : String} {a : ℕ}, s.toNat? = some a → s.toInt? = some ↑a
-- Mathlib.Algebra.Homology.QuasiIso
QuasiIso.congr_simp : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c}
  (f f_1 : K ⟶ L),
  f = f_1 → ∀ [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i], QuasiIso f = QuasiIso f_1
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y : C} [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {J : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver Y)),
  CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation F =
    CategoryTheory.MonoOver.coconeOfHasStrongEpiMonoFactorisation F
-- Mathlib.Topology.Compactness.Compact
/-- To show that `∀ y ∈ K, P x y` holds for `x` close enough to `x₀` when `K` is compact,
it is sufficient to show that for all `y₀ ∈ K` there `P x y` holds for `(x, y)` close enough
to `(x₀, y₀)`.

Provided for backwards compatibility,
see `IsCompact.mem_prod_nhdsSet_of_forall` for a stronger statement.
 -/
IsCompact.eventually_forall_of_forall_eventually : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x₀ : X} {K : Set Y},
  IsCompact K →
    ∀ {P : X → Y → Prop}, (∀ y ∈ K, ∀ᶠ (z : X × Y) in nhds (x₀, y), P z.1 z.2) → ∀ᶠ (x : X) in nhds x₀, ∀ y ∈ K, P x y
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.instModuleSubtypeMem : {R : Type u} →
  {A : Type v} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → Module R ↥S
-- Mathlib.Algebra.Group.Conj
isConj_one_left : ∀ {α : Type u} [inst : Monoid α] {a : α}, IsConj a 1 ↔ a = 1
-- Mathlib.Data.EReal.Inv
EReal.abs_mul : ∀ (x y : EReal), (x * y).abs = x.abs * y.abs
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- Taking a nonnegative power of a nonnegative number. This is defined as a standalone definition
in order to speed up automation such as `cfc_cont_tac`.  -/
NNReal.nnrpow : NNReal → NNReal → NNReal
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.PolyCnstr.isValid.eq_1 : ∀ (c : Nat.Internal.Linear.PolyCnstr), c.isValid = bif c.eq then c.lhs.isZero && c.rhs.isZero else c.lhs.isZero
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.NormalizePattern.main : List Lean.Expr →
  Lean.Meta.Grind.SymbolPriorities → ℕ → Lean.MetaM (List Lean.Expr × List Lean.HeadIndex × Std.HashSet ℕ)
-- Mathlib.Data.List.Defs
List.map₂Left.eq_def : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → Option β → γ) (x : List α) (x_1 : List β),
  List.map₂Left f x x_1 =
    match x, x_1 with
    | [], x => []
    | a :: as, [] => List.map (fun a => f a none) (a :: as)
    | a :: as, b :: bs => f a (some b) :: List.map₂Left f as bs
-- Aesop.Forward.Substitution
Aesop.Substitution.instToMessageData : Lean.ToMessageData Aesop.Substitution
-- Mathlib.Analysis.PSeries
/-- Test for convergence of the `p`-series: the real-valued series `∑' n : ℕ, (n ^ p)⁻¹` converges
if and only if `1 < p`.  -/
Real.summable_nat_rpow_inv : ∀ {p : ℝ}, (Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
-- Mathlib.RepresentationTheory.Coinduced
/-- Given a monoid homomorphism `φ : G →* H`, an `H`-representation `B`, and a `G`-representation
`A`, there is a `k`-linear equivalence between the `G`-representation morphisms `res φ B ⟶ A` and
the `H`-representation morphisms `B ⟶ coind φ A`.

Note `Rep.resCoindHomEquiv.{t, u, v, w}` has the property that
even with all inputs explicitly given, the first universe cannot be synthesized.
 -/
Rep.resCoindHomEquiv : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) →
              (B : Rep.{max w t, u, w} k H) →
                (A : Rep.{max w t, u, v} k G) → (Rep.res φ B ⟶ A) ≃ₗ[k] B ⟶ Rep.coind.{u, v, w, max t w} φ A
-- Mathlib.Order.Interval.Set.SuccPred
Set.Ioc_pred_pred_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] [NoMinOrder α] (a b : α),
  Set.Ioc (Order.pred a) (Order.pred b) = Set.Ico a b
-- Mathlib.AlgebraicGeometry.Sites.Etale
/-- Big étale site: the étale precoverage on the category of schemes.  -/
AlgebraicGeometry.Scheme.etalePrecoverage : CategoryTheory.Precoverage AlgebraicGeometry.Scheme
-- Lean.Meta.RecursorInfo
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.getUnivLevelPos : Lean.Name → List Lean.Name → Lean.Level → List Lean.Level → Lean.MetaM (List Lean.Meta.RecursorUnivLevelPos)
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_isCocircuit_iff : ∀ {α : Type u_1} {M : Matroid α} {K C : Set α}, (M.contract C).IsCocircuit K ↔ M.IsCocircuit K ∧ Disjoint K C
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
/-- The trivialization of the tangent bundle at a point is the manifold derivative of the
extended chart.
Use with care as this abuses the defeq `TangentSpace 𝓘(𝕜, E) y = E` for `y : E`.  -/
TangentBundle.continuousLinearMapAt_trivializationAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] {x₀ x : M},
  x ∈ (chartAt H x₀).source →
    Bundle.Trivialization.continuousLinearMapAt 𝕜 (trivializationAt E (TangentSpace I) x₀) x =
      mfderiv% ↑(extChartAt I x₀) x
-- Mathlib.CategoryTheory.Limits.Chosen.End
CategoryTheory.Limits.chosenEnd.lift_π_assoc : ∀ {J : Type u_3} {C : Type u_4} [inst : CategoryTheory.Category.{v_3, u_4} C]
  [inst_1 : CategoryTheory.Category.{v_4, u_3} J] {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)}
  [inst_2 : CategoryTheory.Limits.ChosenEndsOfShape J C] {X : C} (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j))
  (j : J) {Z : C} (h : (F.obj (Opposite.op j)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.lift f hf)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.chosenEnd.π F j) h) =
    CategoryTheory.CategoryStruct.comp (f j) h
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.toSkeleton_fromSkeleton_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : CategoryTheory.Skeleton C),
  CategoryTheory.toSkeleton ((CategoryTheory.fromSkeleton C).obj X) = X
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun_congr : ∀ {Ω : Type u_1} {ι : Type u_2} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {β : ι → Type u_10}
  {mβ : (i : ι) → MeasurableSpace (β i)} {f g : (i : ι) → Ω → β i},
  (∀ (i : ι), f i =ᵐ[μ] g i) → (ProbabilityTheory.iIndepFun f μ ↔ ProbabilityTheory.iIndepFun g μ)
-- Mathlib.Tactic.Linter.DocString
_private.Mathlib.Tactic.Linter.DocString.0.Array.map_unattach.match_1.eq_1 : ∀ {α : Type u_1} {P : α → Prop} (motive : Subtype P → Sort u_2) (x : α) (h : P x)
  (h_1 : (x : α) → (h : P x) → motive ⟨x, h⟩),
  (match ⟨x, h⟩ with
    | ⟨x, h⟩ => h_1 x h) =
    h_1 x h
-- Mathlib.GroupTheory.QuotientGroup.Finite
AddGroup.fintypeOfKerEqRange.eq_1 : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : AddGroup F] [inst_1 : AddGroup G] [inst_2 : AddGroup H]
  [inst_3 : Fintype F] [inst_4 : Fintype H] (f : F →+ G) (g : G →+ H) (h : g.ker = f.range),
  AddGroup.fintypeOfKerEqRange f g h = AddGroup.fintypeOfKerLeRange f g ⋯
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.inv_toEquiv : ∀ (G : Type v) [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G]
  [inst_3 : IsIsometricSMul Gᵐᵒᵖ G], (IsometryEquiv.inv G).toEquiv = Equiv.inv G
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.tendsto_harmonic_sub_log : Filter.Tendsto (fun n => ↑(harmonic n) - Real.log ↑n) Filter.atTop (nhds Real.eulerMascheroniConstant)
-- Mathlib.NumberTheory.LSeries.Basic
LSeriesSummable.eq_1 : ∀ (f : ℕ → ℂ) (s : ℂ), LSeriesSummable f s = Summable (LSeries.term f s)
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.pred_ncard_le_ncard_sdiff_singleton`. -/
Set.pred_ncard_le_ncard_diff_singleton : ∀ {α : Type u_1} (s : Set α) (a : α), s.ncard - 1 ≤ (s \ {a}).ncard
-- Mathlib.Analysis.Calculus.Deriv.Add
deriv_fun_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {x : 𝕜},
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 g x → deriv (fun y => f y + g y) x = deriv f x + deriv g x
-- Mathlib.ModelTheory.Definability
Set.DefinableFun.ite : ∀ {M : Type u_1} {L : FirstOrder.Language} [inst : L.Structure M] {α : Type u_2} {A : Set M} {f : (α → M) → M}
  {p : (α → M) → Prop} {g : (α → M) → M} [inst_1 : DecidablePred p],
  A.Definable L (Set.ofPred p) →
    Set.DefinableFun L A f → Set.DefinableFun L A g → Set.DefinableFun L A fun v => if p v then f v else g v
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.abs_sin_le_abs : ∀ {x : ℝ}, |Real.sin x| ≤ |x|
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.instInhabitedFamilyOfElementsBot : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {P : CategoryTheory.Functor Cᵒᵖ (Type w)} → {X : C} → Inhabited (CategoryTheory.Presieve.FamilyOfElements P ⊥)
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The map of a Gaussian distribution by addition of a constant is a Gaussian.  -/
ProbabilityTheory.gaussianReal_map_add_const : ∀ {μ : ℝ} {v : NNReal} (y : ℝ),
  MeasureTheory.Measure.map (fun x => x + y) (ProbabilityTheory.gaussianReal μ v) =
    ProbabilityTheory.gaussianReal (μ + y) v
-- Mathlib.Order.DirectedInverseSystem
/-- Extend a partial family of bijections by one step.  -/
InverseSystem.pEquivOnSucc : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      {i : ι} →
        [inst : LinearOrder ι] →
          {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
            [inst_1 : SuccOrder ι] →
              {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} →
                [InverseSystem f] →
                  ¬IsMax i →
                    InverseSystem.PEquivOn f equivSucc (Set.Iic i) →
                      (∀ ⦃i : ι⦄ (hi : ¬IsMax i) (x : F (Order.succ i)), ((equivSucc hi) x).1 = f ⋯ x) →
                        InverseSystem.PEquivOn f equivSucc (Set.Iic (Order.succ i))
-- Mathlib.Order.Partition.Finpartition
Finpartition.extend_parts : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : IsModularLattice α] [inst_3 : DecidableEq α]
  {a b c : α} (P : Finpartition a) (hb : b ≠ ⊥) (hab : Disjoint a b) (hc : a ⊔ b = c),
  (P.extend hb hab hc).parts = insert b P.parts
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveColimits
CategoryTheory.isSheaf_pointwiseColimit : ∀ {A : Type u_1} {C : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] [inst_2 : CategoryTheory.Category.{v_3, u_3} J]
  [inst_3 : CategoryTheory.FinitaryExtensive C] [inst_4 : CategoryTheory.Limits.HasColimitsOfShape J A]
  [CategoryTheory.Limits.PreservesFiniteProducts CategoryTheory.Limits.colim]
  (G : CategoryTheory.Functor J (CategoryTheory.Sheaf (CategoryTheory.extensiveTopology C) A)),
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.extensiveTopology C)
    (CategoryTheory.Limits.pointwiseCocone
        (G.comp (CategoryTheory.sheafToPresheaf (CategoryTheory.extensiveTopology C) A))).pt
-- Mathlib.Algebra.Algebra.Unitization
Unitization.snd_mul : ∀ {R : Type u_1} {A : Type u_2} [inst : Mul R] [inst_1 : Add A] [inst_2 : Mul A] [inst_3 : SMul R A]
  (x₁ x₂ : Unitization R A),
  (x₁ * x₂).toProd.2 = x₁.toProd.1 • x₂.toProd.2 + x₂.toProd.1 • x₁.toProd.2 + x₁.toProd.2 * x₂.toProd.2
-- Lean.Meta.Tactic.Simp.Diagnostics
Lean.Meta.Simp.mkSimpDiagSummary : Lean.PHashMap Lean.Meta.Origin ℕ →
  optParam (Option (Lean.PHashMap Lean.Meta.Origin ℕ)) none → Lean.MetaM Lean.Meta.DiagSummary
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [inst_2 : LawfulBEq α],
  (↑m₁).WF →
    (↑m₂).WF →
      ∀ {k : α} [inst_3 : Inhabited (β k)], (m₁.inter m₂).get! k = if m₂.contains k = true then m₁.get! k else default
-- Init.Data.Order.PackageFactories
Std.Packages.LinearOrderOfOrdArgs.eq_of_compare : ∀ {α : Type u} (self : Std.Packages.LinearOrderOfOrdArgs α),
  let this := self.ord;
  let this_1 := self.le;
  ∀ (a b : α), compare a b = Ordering.eq → a = b
-- Mathlib.CategoryTheory.ObjectProperty.Orthogonal
/-- In a category with zero morphisms, the left orthogonal of a property of objects `P`
is the property of objects `X` such that any map `X ⟶ Y` vanishes when `P Y` holds.  -/
CategoryTheory.ObjectProperty.leftOrthogonal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasZeroMorphisms C] → CategoryTheory.ObjectProperty C → CategoryTheory.ObjectProperty C
-- Mathlib.LinearAlgebra.CliffordAlgebra.Fold
CliffordAlgebra.foldr_ι : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (Q : QuadraticForm R M) (f : M →ₗ[R] N →ₗ[R] N)
  (hf : ∀ (m : M) (x : N), (f m) ((f m) x) = Q m • x) (n : N) (m : M),
  ((CliffordAlgebra.foldr Q f hf) n) ((CliffordAlgebra.ι Q) m) = (f m) n
-- Init.Data.List.Lemmas
List.replicate_succ_ne_nil : ∀ {α : Type u_1} {n : ℕ} {a : α}, List.replicate (n + 1) a ≠ []
-- Mathlib.Topology.Sets.Closeds
/-- in a `T1Space`, atoms of `TopologicalSpace.Closeds α` are precisely the singletons.  -/
TopologicalSpace.Closeds.isAtom_iff : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {s : TopologicalSpace.Closeds α},
  IsAtom s ↔ ∃ x, s = {x}
-- Init.Data.String.Defs
String.instDecidableLePos : {s : String} → (l r : s.Pos) → Decidable (l ≤ r)
-- Mathlib.Analysis.Convex.Jensen
/-- A form of the **equality case of Jensen's equality** for the case of strict concave and
non-negative weights.  -/
StrictConcaveOn.map_sum_eq_iff_of_nonneg : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  StrictConcaveOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) →
      ∑ i ∈ t, w i = 1 →
        (∀ i ∈ t, p i ∈ s) →
          (f (∑ i ∈ t, w i • p i) = ∑ i ∈ t, w i • f (p i) ↔
            ∀ ⦃j : ι⦄, j ∈ t → w j ≠ 0 → ∀ ⦃k : ι⦄, k ∈ t → w k ≠ 0 → p j = p k)
-- Mathlib.Algebra.Lie.Basic
lieRingSelfModule : {L : Type v} → [inst : LieRing L] → LieRingModule L L
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.mod_lt : ∀ {R : Type u} [inst : EuclideanDomain R] (a : R) {b : R}, b ≠ 0 → EuclideanDomain.r (a % b) b
-- Init.Data.List.Lemmas
List.foldl_append_eq_append : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} {l' : List β},
  List.foldl (fun x1 x2 => x1 ++ f x2) l' l = l' ++ (List.map f l).flatten
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- A spectral object in an abelian category category `C` indexed by a category `ι`
consists of a family of functors `H n : ComposableArrows ι 1 ⥤ C` for all `n : ℤ`, and a
functorial long exact sequence
`⋯ ⟶ (H n₀).obj (mk₁ f) ⟶ (H n₀).obj (mk₁ (f ≫ g)) ⟶ (H n₀).obj (mk₁ g) ⟶ (H n₁).obj (mk₁ f) ⟶ ⋯`
when `n₀ + 1 = n₁` and `f` and `g` are composable morphisms in `ι`. (This will be
shortened as `H^n₀(f) ⟶ H^n₀(f ≫ g) ⟶ H^n₀(g) ⟶ H^n₁(f)` in the documentation.)  -/
CategoryTheory.Abelian.SpectralObject : (C : Type u_1) →
  (ι : Type u_2) →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [CategoryTheory.Category.{u_4, u_2} ι] → [CategoryTheory.Abelian C] → Type (max (max (max u_1 u_2) u_3) u_4)
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.mk : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] {φ : M →* N}
  {ψ : N →* P} {χ : outParam (M →* P)}, ψ.comp φ = χ → φ.CompTriple ψ χ
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `le_of_mul_le_mul_left`. -/
le_of_mul_le_mul_of_pos_left : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [PosMulReflectLE α],
  a * b ≤ a * c → 0 < a → b ≤ c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {he : t.erase k ≠ ∅}, (t.erase k).minKey he = t.minKey ⋯ ↔ ¬cmp k (t.minKey ⋯) = Ordering.eq
-- Mathlib.Probability.Kernel.Composition.Prod
ProbabilityTheory.Kernel.parallelComp_comp_copy : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) (η : ProbabilityTheory.Kernel α γ),
  (κ.parallelComp η).comp (ProbabilityTheory.Kernel.copy α) = κ.prod η
-- Mathlib.RingTheory.Localization.Module
LocalizedModule.coe_map_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {N : Type u_5} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {M' : Type u_3} {N' : Type u_4}
  [inst_5 : AddCommMonoid M'] [inst_6 : AddCommMonoid N'] [inst_7 : Module R M'] [inst_8 : Module R N']
  (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N') [inst_9 : IsLocalizedModule S g₁] [inst_10 : IsLocalizedModule S g₂]
  (l : M →ₗ[R] N),
  ⇑((LocalizedModule.map S) l) =
    ⇑(IsLocalizedModule.iso S g₂).symm ∘ ⇑((IsLocalizedModule.map S g₁ g₂) l) ∘ ⇑(IsLocalizedModule.iso S g₁)
-- Mathlib.Algebra.Group.Action.End
MulAut.smul_def : ∀ {M : Type u_2} [inst : Monoid M] (f : MulAut M) (a : M), f • a = f a
-- Mathlib.Tactic.NormNum.GCD
/-- Given natural number literals `ex` and `ey`, return their LCM as a natural number literal
and an equality proof. Panics if `ex` or `ey` aren't natural number literals.  -/
Mathlib.Meta.NormNum.proveNatLCM : (ex ey : Q(ℕ)) → (ed : Q(ℕ)) × Q(«$ex».lcm «$ey» = «$ed»)
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.comp_assoc : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {P : Type u_3} [inst_5 : AddCommMonoid P] [inst_6 : Module R P]
  {Q : Type u_4} [inst_7 : AddCommMonoid Q] [inst_8 : Module R Q] (f : M →ₚₗ[R] N) (g : N →ₚₗ[R] P) (h : P →ₚₗ[R] Q),
  h.comp (g.comp f) = (h.comp g).comp f
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
AddMonoidAlgebra.instHopfAlgebra.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : HopfAlgebra R A] {G : Type u_3}
  [inst_3 : AddGroup G],
  AddMonoidAlgebra.instHopfAlgebra =
    { toHopfAlgebraStruct := AddMonoidAlgebra.instHopfAlgebraStruct R A G, mul_antipode_rTensor_comul := ⋯,
      mul_antipode_lTensor_comul := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Symmetric
/-- A symmetric linear map `T` is zero if and only if `⟪T x, x⟫_ℝ = 0` for all `x`.
See `inner_map_self_eq_zero` for the complex version without the symmetric assumption.  -/
LinearMap.IsSymmetric.inner_map_self_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ((∀ (x : E), inner 𝕜 (T x) x = 0) ↔ T = 0)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Complex.isEquivalent_sinh : Asymptotics.IsEquivalent (nhds 0) Complex.sinh id
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (self : CategoryTheory.GlueData C) (i : self.J),
  self.t i i = CategoryTheory.CategoryStruct.id (self.V (i, i))
-- Init.Data.Fin.Lemmas
Fin.coe_sub_iff_le : ∀ {n : ℕ} {a b : Fin n}, ↑(a - b) = ↑a - ↑b ↔ b ≤ a
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.genEigenspace_le_smul : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (μ t : R) (k : ℕ∞), (f.genEigenspace μ) k ≤ ((t • f).genEigenspace (t * μ)) k
-- Init.Data.Nat.Lemmas
Nat.succ_sub_one : ∀ (n : ℕ), n.succ - 1 = n
-- Mathlib.Topology.List
List.tendsto_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : AddZeroClass α] [ContinuousAdd α] {l : List α},
  Filter.Tendsto List.sum (nhds l) (nhds l.sum)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.mem_prod : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] {s : Submonoid M} {t : Submonoid N}
  {p : M × N}, p ∈ s.prod t ↔ p.1 ∈ s ∧ p.2 ∈ t
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_ofNat : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo], ↑(OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- See `inner_smul_left` for the common special when `𝕜 = 𝕝`.  -/
inner_smul_left_eq_star_smul : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {𝕝 : Type u_4} [inst_3 : CommSemiring 𝕝] [inst_4 : StarRing 𝕝] [inst_5 : Algebra 𝕝 𝕜] [inst_6 : Module 𝕝 E]
  [IsScalarTower 𝕝 𝕜 E] [StarModule 𝕝 𝕜] (x y : E) (r : 𝕝), inner 𝕜 (r • x) y = (starRingEnd 𝕝) r • inner 𝕜 x y
-- Mathlib.Tactic.CategoryTheory.Reassoc
_private.Mathlib.Tactic.CategoryTheory.Reassoc.0.Mathlib.Tactic.Reassoc.reassocImpl : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM Lean.Name
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.instOfIsEmptyCarrierCarrierCommRingCat : ∀ {X Y : AlgebraicGeometry.Scheme} [IsEmpty ↥X] (f : X ⟶ Y), AlgebraicGeometry.IsClosedImmersion f
-- Mathlib.Algebra.Order.Ring.Synonym
toLex_natCast : ∀ {R : Type u_1} [inst : NatCast R] (n : ℕ), toLex ↑n = ↑n
-- Mathlib.Algebra.Group.Submonoid.Finsupp
Submonoid.exists_of_mem_closure_range : ∀ {M : Type u_1} [inst : CommMonoid M] {ι : Type u_2} (f : ι → M) (x : M) [inst_1 : Fintype ι],
  x ∈ Submonoid.closure (Set.range f) → ∃ a, x = ∏ i, f i ^ a i
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.homMk_comp_homMk : ∀ {V : SSet.Truncated 2}
  {x₀ x₁ x₂ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
  {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
  (h : e₀₁.CompStruct e₁₂ e₀₂),
  CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory.homMk e₀₁)
      (SSet.Truncated.HomotopyCategory.homMk e₁₂) =
    SSet.Truncated.HomotopyCategory.homMk e₀₂