mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv_spanSingleton : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P] {P' : Type u_5} [inst_4 : CommRing P'] [inst_5 : Algebra R P']
  [inst_6 : IsLocalization S P'] (x : P),
  (FractionalIdeal.canonicalEquiv S P P') (FractionalIdeal.spanSingleton S x) =
    FractionalIdeal.spanSingleton S ((IsLocalization.map P' (RingHom.id R) ⋯) x)
-- Lean.Data.Json.Printer
_private.Lean.Data.Json.Printer.0.Lean.Json.CompressWorkItemQueue.popValue! : Lean.Json.CompressWorkItemQueue✝ → Lean.Json × Lean.Json.CompressWorkItemQueue✝
-- Init.Data.Array.Extract
Array.extract_eq_empty_iff : ∀ {α : Type u_1} {i j : ℕ} {as : Array α}, as.extract i j = #[] ↔ min j as.size ≤ i
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.topEquiv_apply : ∀ {R : Type u} [inst : NonAssocRing R] (r : ↥⊤), Subring.topEquiv r = ↑r
-- Mathlib.Algebra.Lie.CartanCriterion
_private.Mathlib.Algebra.Lie.CartanCriterion.0.LieModule.exists_polynomial_eval_sub_aux : ∀ {ι : Type u_4} {R : Type u_5} {K : Type u_6} [Finite ι] [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  {E : Submodule R K} (a : ι → K) (ha : ∀ (i : ι), a i ∈ E) (f : ↥E →+ R),
  ∃ r, ∀ (i j : ι), Polynomial.eval (a i - a j) r = (algebraMap R K) (f ⟨a i, ⋯⟩) - (algebraMap R K) (f ⟨a j, ⋯⟩)
-- Init.Data.String.PosRaw
String.instHSubRaw : HSub String.Pos.Raw String String.Pos.Raw
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m₁ \ m₂).contains k = (m₁.contains k && !m₂.contains k)
-- Std.Data.Iterators.Lemmas.Producers.Array
Array.iter_eq_toIter_iterM : ∀ {β : Type w} {array : Array β}, array.iter = (array.iterM Id).toIter
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_vadd_closedEBall : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal),
  (fun x => c +ᵥ x) ⁻¹' Metric.closedEBall x r = Metric.closedEBall (-c +ᵥ x) r
-- Mathlib.Probability.Kernel.Proper
/-- **Alias** of the forward direction of `ProbabilityTheory.Kernel.isProper_iff_inter_eq_indicator_mul`. -/
ProbabilityTheory.Kernel.IsProper.inter_eq_indicator_mul : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X},
  𝓑 ≤ 𝓧 →
    π.IsProper →
      ∀ ⦃A : Set X⦄,
        MeasurableSet A → ∀ ⦃B : Set X⦄, MeasurableSet B → ∀ (x : X), (π x) (A ∩ B) = B.indicator 1 x * (π x) A
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.uniqueBaseOn_isBasis_iff : ∀ {α : Type u_1} {E I X J : Set α}, X ⊆ E → ((Matroid.uniqueBaseOn I E).IsBasis J X ↔ J = X ∩ I)
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
/-- Root number  -/
WeakFEPair.ε : {E : Type u_1} → [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℂ E] → WeakFEPair E → ℂ
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_const_right : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {w : ι → ℝ} (f : ι → 𝕜) (a : 𝕜),
  ⟪f, Function.const ι a⟫_[𝕜, w] = a * ∑ i, w i • (starRingEnd 𝕜) (f i)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableSet.of_union₃_range_cover : ∀ {α : Type u_1} {α₁ : Type u_6} {α₂ : Type u_7} {α₃ : Type u_8} {mα : MeasurableSpace α} {mα₁ : MeasurableSpace α₁}
  {mα₂ : MeasurableSpace α₂} {mα₃ : MeasurableSpace α₃} {i₁ : α₁ → α} {i₂ : α₂ → α} {i₃ : α₃ → α} {s : Set α},
  MeasurableEmbedding i₁ →
    MeasurableEmbedding i₂ →
      MeasurableEmbedding i₃ →
        Set.univ ⊆ Set.range i₁ ∪ Set.range i₂ ∪ Set.range i₃ →
          MeasurableSet (i₁ ⁻¹' s) → MeasurableSet (i₂ ⁻¹' s) → MeasurableSet (i₃ ⁻¹' s) → MeasurableSet s
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.le_aleph0_iff_subtype_countable : ∀ {α : Type u} {p : α → Prop}, Cardinal.mk { x // p x } ≤ Cardinal.aleph0 ↔ {x | p x}.Countable
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapCocycles₂_comp_i_apply : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u_1, u, u} k H}
  {B : Rep.{u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (x : ↥(groupCohomology.cocycles₂ A)),
  (ModuleCat.Hom.hom (groupCohomology.shortComplexH2 B).g).ker.subtype
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.mapCocycles₂ f φ)) x) =
    ((Rep.Hom.hom φ).compLeft (G × G))
      ((LinearMap.funLeft k (↑A) (Prod.map ⇑f ⇑f))
        ((ModuleCat.Hom.hom (groupCohomology.shortComplexH2 A).g).ker.subtype x))
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.Presentation.reindex.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Presentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ),
  P.reindex e f =
    { toGenerators := P.reindex e, relation := ⇑(MvPolynomial.rename ⇑e.symm) ∘ P.relation ∘ ⇑f,
      span_range_relation_eq_ker := ⋯ }
-- Lean.Expr
/-- Given `f a_1 ... a_n`, returns `#[a_1, ..., a_n]`.
Note that `f` may be an application.
The resulting array has size `n` even if `f.getAppNumArgs < n`.
 -/
Lean.Expr.getAppArgsN : Lean.Expr → ℕ → Array Lean.Expr
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Lift a `f : {a : M // a ≠ 0} → α` function to `FiniteArchimedeanClass M → α`.  -/
FiniteArchimedeanClass.lift : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] →
      [inst_2 : IsOrderedAddMonoid M] →
        {α : Type u_2} →
          (f : { a // a ≠ 0 } → α) →
            (∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ = FiniteArchimedeanClass.mk ↑b ⋯ → f a = f b) →
              FiniteArchimedeanClass M → α
-- Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
rank_lt_rank_dual : ∀ {K V : Type u} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Cardinal.aleph0 ≤ Module.rank K V → Module.rank K V < Module.rank K (V →ₗ[K] K)
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovary_iff_forall_mul_nonneg`. -/
Monovary.sub_mul_sub_nonneg : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α},
  Monovary f g → ∀ (i j : ι), 0 ≤ (f j - f i) * (g j - g i)
-- Mathlib.RingTheory.Spectrum.Maximal.Basic
MaximalSpectrum.toPrimeSpectrum_injective : ∀ {R : Type u_1} [inst : CommSemiring R], Function.Injective MaximalSpectrum.toPrimeSpectrum
-- Mathlib.Algebra.Divisibility.Units
isRelPrime_self : ∀ {α : Type u_1} [inst : CommMonoid α] {x : α}, IsRelPrime x x ↔ IsUnit x
-- Std.Time.Format.Modifier
Std.Time.Modifier.D.inj : ∀ {presentation presentation_1 : Std.Time.Number},
  Std.Time.Modifier.D presentation = Std.Time.Modifier.D presentation_1 → presentation = presentation_1
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
ringKrullDim_le_ringKrullDim_quotient_add_encard : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R],
  ∀ s ⊆ ↑(Ring.jacobson R), ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span s) + ↑s.encard
-- Mathlib.Order.Interval.Set.Infinite
Set.instInfiniteElemIoiOfNoMaxOrder : ∀ {α : Type u_1} [inst : Preorder α] [NoMaxOrder α] {a : α}, Infinite ↑(Set.Ioi a)
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.empty_M : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_4} {H : Type u_5} {M : Type u_6}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} [inst_5 : TopologicalSpace M] [inst_6 : ChartedSpace H M]
  [inst_7 : IsManifold I k M] [inst_8 : IsEmpty M], (SingularManifold.empty X M I).M = M
-- Mathlib.CategoryTheory.Galois.Basic
/-- `C` has pullbacks (G1).  -/
CategoryTheory.PreGaloisCategory.hasPullbacks : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{u₂, u₁} C} [self : CategoryTheory.PreGaloisCategory C],
  CategoryTheory.Limits.HasPullbacks C
-- Mathlib.RingTheory.Finiteness.Subalgebra
Submodule.FG.mul : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {M N : Submodule R A}, M.FG → N.FG → (M * N).FG
-- Std.Async.System
/-- Gets an environment variable.
 -/
Std.Async.System.getEnvVar : String → IO (Option String)
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.quot_neg : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J RingCat)
  (x : RingCat.Colimits.Prequotient F),
  Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x.neg =
    -have this := Quot.mk (⇑(RingCat.Colimits.colimitSetoid F)) x;
      this
-- Mathlib.Geometry.Euclidean.Sphere.OrthRadius
EuclideanGeometry.Sphere.mem_orthRadius_iff_inner_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p x : P},
  x ∈ s.orthRadius p ↔ inner ℝ (p -ᵥ s.center) (x -ᵥ p) = 0
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.equivIntOfUnique.eq_1 : ∀ {α : Type u} [inst : Unique α],
  FreeGroup.equivIntOfUnique =
    { toFun := fun x => ((FreeGroup.map 1) x).sum, invFun := fun x => FreeGroup.of default ^ x, left_inv := ⋯,
      right_inv := ⋯ }
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.msgToInteractiveAux.mkContextInfo : Lean.NamingContext → Lean.MessageDataContext → Lean.Elab.ContextInfo
-- Mathlib.RingTheory.Extension.Presentation.Basic
_private.Mathlib.RingTheory.Extension.Presentation.Basic.0.Algebra.Presentation.aux_eq_comp : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ),
  Algebra.Presentation.aux✝ Q P =
    (MvPolynomial.mapAlgHom (MvPolynomial.aeval P.val)).comp ↑(MvPolynomial.sumAlgEquiv R ι' ι)
-- Init.Grind.Order
Lean.Grind.Order.of_nat_eq : ∀ (a b : ℕ) (x y : ℤ), ↑a = x → ↑b = y → a = b → x = y
-- Mathlib.FieldTheory.SplittingField.IsSplittingField
Polynomial.IsSplittingField.splits' : ∀ {K : Type v} {L : Type w} {inst : Field K} {inst_1 : Field L} {inst_2 : Algebra K L} {f : Polynomial K}
  [self : Polynomial.IsSplittingField K L f], (Polynomial.map (algebraMap K L) f).Splits
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).minKey ⋯ = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.instT2Space : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  [T2Space 𝕜], T2Space (WeakDual 𝕜 E)
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.coe_extended_eq_span : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  (I : FractionalIdeal M K), ↑(FractionalIdeal.extended L hf I) = Submodule.span B (⇑(IsLocalization.map L f hf) '' ↑I)
-- Init.Control.Lawful.Instances
ExceptT.lift_pure : ∀ {m : Type u_1 → Type u_2} {α ε : Type u_1} [inst : Monad m] [LawfulMonad m] (a : α), ExceptT.lift (pure a) = pure a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHint.paddingRight? : Lean.Lsp.InlayHint → Option Bool
-- Lean.Expr
Lean.instReprData_1 : Repr Lean.Expr.Data
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.Mod.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.MonObj A] (A_1 : CategoryTheory.Mod D A),
  (CategoryTheory.Mod.forget A).obj A_1 = A_1.X
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_int32ToBitVec : ∀ (x : Int32), Int64.ofBitVec (BitVec.signExtend 64 x.toBitVec) = x.toInt64
-- Mathlib.ModelTheory.Equivalence
FirstOrder.Language.Theory.sup_imp : ∀ {L : FirstOrder.Language} {T : L.Theory} {α : Type w} {n : ℕ} {φ ψ θ : L.BoundedFormula α n},
  T.Imp φ θ → T.Imp ψ θ → T.Imp (φ ⊔ ψ) θ
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go.match_1.eq_3 : ∀ (motive : Lean.Level → Lean.Level → Sort u_1) (u₁ u₂ v : Lean.Level)
  (h_1 : (x : Lean.Level) → motive x Lean.Level.zero) (h_2 : (u v₁ v₂ : Lean.Level) → motive u (v₁.max v₂))
  (h_3 : (u₁ u₂ v : Lean.Level) → motive (u₁.max u₂) v) (h_4 : (a u₂ v : Lean.Level) → motive (a.imax u₂) v)
  (h_5 : (u v : Lean.Level) → motive u.succ v.succ) (h_6 : (x x_1 : Lean.Level) → motive x x_1),
  (v = Lean.Level.zero → False) →
    (∀ (v₁ v₂ : Lean.Level), v = v₁.max v₂ → False) →
      (match u₁.max u₂, v with
        | x, Lean.Level.zero => h_1 x
        | u, v₁.max v₂ => h_2 u v₁ v₂
        | u₁.max u₂, v => h_3 u₁ u₂ v
        | a.imax u₂, v => h_4 a u₂ v
        | u.succ, v.succ => h_5 u v
        | x, x_1 => h_6 x x_1) =
        h_3 u₁ u₂ v
-- Mathlib.Order.SuccPred.Basic
Order.pred_lt_pred_iff_of_not_isMin : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α},
  ¬IsMin b → ¬IsMin a → (Order.pred b < Order.pred a ↔ b < a)
-- Mathlib.Order.Filter.Basic
Filter.inf_principal_eq_bot : ∀ {α : Type u} {f : Filter α} {s : Set α}, f ⊓ Filter.principal s = ⊥ ↔ sᶜ ∈ f
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listEncode.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (n : ℕ)
  (h_1 : (n : ℕ) → motive n FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (n l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin n)) → motive n (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (φ₁ φ₂ : L.BoundedFormula α x) → motive x (φ₁.imp φ₂))
  (h_5 : (x : ℕ) → (φ : L.BoundedFormula α (x + 1)) → motive x φ.all),
  (match n, FirstOrder.Language.BoundedFormula.falsum with
    | n, FirstOrder.Language.BoundedFormula.falsum => h_1 n
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | n, FirstOrder.Language.BoundedFormula.rel R ts => h_3 n l R ts
    | x, φ₁.imp φ₂ => h_4 x φ₁ φ₂
    | x, φ.all => h_5 x φ) =
    h_1 n
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.coe_nnnorm : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] (f : ↥(MeasureTheory.Lp E p μ)), ↑‖f‖₊ = ‖f‖
-- Init.Grind.Module.NatModuleNorm
_private.Init.Grind.Module.NatModuleNorm.0.Lean.Grind.Linarith.Expr.denoteN.match_1.eq_5 : ∀ (motive : Lean.Grind.Linarith.Expr → Sort u_1) (v : Lean.Grind.Linarith.Var)
  (h_1 : (a b : Lean.Grind.Linarith.Expr) → motive (a.sub b)) (h_2 : (a : Lean.Grind.Linarith.Expr) → motive a.neg)
  (h_3 : (k : ℤ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.intMul k a))
  (h_4 : Unit → motive Lean.Grind.Linarith.Expr.zero)
  (h_5 : (v : Lean.Grind.Linarith.Var) → motive (Lean.Grind.Linarith.Expr.var v))
  (h_6 : (a b : Lean.Grind.Linarith.Expr) → motive (a.add b))
  (h_7 : (k : ℕ) → (a : Lean.Grind.Linarith.Expr) → motive (Lean.Grind.Linarith.Expr.natMul k a)),
  (match Lean.Grind.Linarith.Expr.var v with
    | a.sub b => h_1 a b
    | a.neg => h_2 a
    | Lean.Grind.Linarith.Expr.intMul k a => h_3 k a
    | Lean.Grind.Linarith.Expr.zero => h_4 ()
    | Lean.Grind.Linarith.Expr.var v => h_5 v
    | a.add b => h_6 a b
    | Lean.Grind.Linarith.Expr.natMul k a => h_7 k a) =
    h_5 v
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.exact₁' : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (self : CategoryTheory.Abelian.SpectralObject C ι) (n₀ n₁ : ℤ) (h : n₀ + 1 = n₁)
  (D : CategoryTheory.ComposableArrows ι 2),
  (CategoryTheory.ComposableArrows.mk₂ ((self.δ' n₀ n₁ h).app D)
      ((self.H n₁).map
        ((CategoryTheory.ComposableArrows.mapFunctorArrows ι 0 1 0 2 2 CategoryTheory.Abelian.SpectralObject._proof_6
              CategoryTheory.Abelian.SpectralObject._proof_8 CategoryTheory.Abelian.SpectralObject._proof_10
              CategoryTheory.Abelian.SpectralObject._proof_2 CategoryTheory.Abelian.SpectralObject._proof_4).app
          D))).Exact
-- Mathlib.Algebra.Group.Equiv.Basic
/-- The `AddEquiv` between two `AddMonoid`s with a unique element.  -/
AddEquiv.ofUnique : {M : Type u_16} → {N : Type u_17} → [Unique M] → [Unique N] → [inst : Add M] → [inst_1 : Add N] → M ≃+ N
-- Mathlib.Algebra.NonAssoc.PreLie.Basic
/-- Every left pre-Lie algebra is a right pre-Lie algebra with the opposite multiplication  -/
LeftPreLieAlgebra.instRightPreLieAlgebraMulOpposite : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] → [inst_1 : LeftPreLieRing L] → [LeftPreLieAlgebra R L] → RightPreLieAlgebra R Lᵐᵒᵖ
-- Mathlib.Control.Fold
Monoid.Foldl.mk : {α : Type u} → (α → α) → Monoid.Foldl α
-- Lean.Parser.Term
Lean.Parser.Term.waitIfTypeContainsMVar.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Dynamics.Ergodic.Action.OfMinimal
/-- Let `f : G →* G` be a group endomorphism of a topological group with second countable topology.
If the preimages of `1` under the iterations of `f` are dense,
then it is pre-ergodic with respect to any finite inner regular left invariant measure.  -/
MonoidHom.preErgodic_of_dense_iUnion_preimage_one : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [SecondCountableTopology G]
  [inst_4 : MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [MeasureTheory.IsFiniteMeasure μ]
  [μ.InnerRegular] [μ.IsMulLeftInvariant] (f : G →* G), Dense (⋃ n, (⇑f)^[n] ⁻¹' 1) → PreErgodic (⇑f) μ
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- Given an `n`-th primitive root of unity `ζ`, where `2 ≤ n`, we have that `∑ i ∈ range j, ζ ^ i`
is a unit for all `j` coprime with `n`. This is the unit given by
`associated_pow_sub_one_pow_of_coprime` (see
`pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum`).  -/
IsPrimitiveRoot.geom_sum_isUnit : ∀ {n j : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [IsDomain A],
  IsPrimitiveRoot ζ n → 2 ≤ n → j.Coprime n → IsUnit (∑ i ∈ Finset.range j, ζ ^ i)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
mvfderiv_comp_apply : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M' → M} {g : M → 𝕜} (x : M'),
  MDiffAt g (f x) → MDiffAt f x → ∀ (v : TangentSpace I' x), (d% (g ∘ f) x) v = (d% g (f x)) ((mfderiv% f x) v)
-- Mathlib.CategoryTheory.CodiscreteCategory
CategoryTheory.Codiscrete.eq_iso_hom : ∀ {A : Type u} {x y : CategoryTheory.Codiscrete A} (f : x ⟶ y), f = (x.iso y).hom
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
linearIndependent_equiv : ∀ {ι : Type u'} {ι' : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (e : ι ≃ ι') {f : ι' → M}, LinearIndependent R (f ∘ ⇑e) ↔ LinearIndependent R f
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_Ico : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Preorder α] [CompactIccSpace α] (a b : α),
  Bornology.IsBounded (Set.Ico a b)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial_seq : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {n : ℕ},
  (Tactic.ComputeAsymptotics.MultiseriesExpansion.monomial (basis_hd :: basis_tl) n).seq =
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomial basis_hd basis_tl n
-- Mathlib.CategoryTheory.Limits.Cones
/-- The category of cones on a given diagram.  -/
CategoryTheory.Limits.Cone.category : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          CategoryTheory.Category.{v₃, max (max u₃ u₁) v₃} (CategoryTheory.Limits.Cone F)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
HasStrictFDerivAt.cos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Real.cos (f x)) (-Real.sin (f x) • f') x
-- Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology
Ideal.nonarchimedean : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R), NonarchimedeanRing R
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalWithReducibleAndInstances : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.hom_inv_id_tensor' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ⟶ W) [inst_2 : CategoryTheory.IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.inv f) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id V) g)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id V) h)
-- Mathlib.Data.Quot
/-- Map a function `f : α → β` such that `ra x y` implies `rb (f x) (f y)`
to a map `Quot ra → Quot rb`.  -/
Quot.map : {α : Sort u_1} →
  {β : Sort u_2} →
    {ra : α → α → Prop} → {rb : β → β → Prop} → (f : α → β) → (∀ ⦃a b : α⦄, ra a b → rb (f a) (f b)) → Quot ra → Quot rb
-- Mathlib.RingTheory.Ideal.Cotangent
IsLocalRing.instIsScalarTowerResidueFieldCotangentSpace : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R],
  IsScalarTower R (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R)
-- Mathlib.Algebra.Opposites
MulOpposite.instMul.eq_1 : ∀ {α : Type u_1} [inst : Mul α],
  MulOpposite.instMul = { mul := fun x y => MulOpposite.op (MulOpposite.unop y * MulOpposite.unop x) }
-- Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Basic
ProbabilityTheory.IsGaussian.hasGaussianLaw_id : ∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommMonoid E] [inst_2 : Module ℝ E] {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ], ProbabilityTheory.HasGaussianLaw id μ