mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Countable
CategoryTheory.instCountableCategoryOfCountableOfIsThin : ∀ {J : Type u} [Countable J] [inst : CategoryTheory.Category.{v_1, u} J] [Quiver.IsThin J],
  CategoryTheory.CountableCategory J
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `cyclotomic n` is monic.  -/
Polynomial.cyclotomic.monic : ∀ (n : ℕ) (R : Type u_1) [inst : Ring R], (Polynomial.cyclotomic n R).Monic
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.span_range_h'_eq_top : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N}
  [inst_5 : P.IsCrystallographic] (b : P.Base) [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι], Submodule.span R (Set.range RootPairing.GeckConstruction.h') = ⊤
-- Init.Data.List.Sublist
List.infix_append_iff_ne_nil : ∀ {α : Type u} {l xs ys : List α},
  l <:+: xs ++ ys ↔ l <:+: xs ∨ l <:+: ys ∨ ∃ l₁ l₂, l₁ ≠ [] ∧ l₂ ≠ [] ∧ l = l₁ ++ l₂ ∧ l₁ <:+ xs ∧ l₂ <+: ys
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_map : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (p : PowerSeries R) (n : ℕ),
  (PowerSeries.trunc n) ((PowerSeries.map f) p) = Polynomial.map f ((PowerSeries.trunc n) p)
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.mk.injEq : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] {M N : Action V G}
  (hom : M.V ⟶ N.V)
  (comm :
    autoParam
      (∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) hom = CategoryTheory.CategoryStruct.comp hom (N.ρ g))
      Action.Hom.comm._autoParam)
  (hom_1 : M.V ⟶ N.V)
  (comm_1 :
    autoParam
      (∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) hom_1 = CategoryTheory.CategoryStruct.comp hom_1 (N.ρ g))
      Action.Hom.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Mathlib.Algebra.Ring.BooleanRing
ofBoolRing_mul : ∀ {α : Type u_1} [inst : BooleanAlgebra α] (a b : AsBoolRing α), ofBoolRing (a * b) = ofBoolRing a ⊓ ofBoolRing b
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- An additive submagma of a left cancellative additive magma inherits left cancellation.  -/
AddMemClass.isLeftCancelAdd : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] [IsLeftCancelAdd M]
  (S : A), IsLeftCancelAdd ↥S
-- Mathlib.Order.Filter.AtTopBot.Group
/-- $\lim_{x\to+\infty}|x|_m=+\infty$  -/
Filter.tendsto_mabs_atTop_atTop : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : LinearOrder G], Filter.Tendsto mabs Filter.atTop Filter.atTop
-- Mathlib.Data.Num.Basic
PosNum.instOfNatHAddNatOfNat : {n : ℕ} → OfNat PosNum (n + 1)
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth_strictMono : StrictMono Cardinal.preBeth
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
CStarModule.inner_smul_right_real : ∀ {A : Type u_1} {E : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : AddCommGroup E]
  [inst_3 : Module ℂ A] [inst_4 : Module ℂ E] [inst_5 : PartialOrder A] [inst_6 : SMul A E] [inst_7 : Norm A]
  [inst_8 : Norm E] [inst_9 : CStarModule A E] [StarModule ℂ A] {z : ℝ} {x y : E}, inner A x (z • y) = z • inner A x y
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.mk_eq_of : ∀ {G : Type u} [inst : Group G] (a : G), Quot.mk (⇑(QuotientGroup.leftRel (commutator G))) a = Abelianization.of a
-- Mathlib.Tactic.FunProp.FunctionData
/-- Function data has been successfully generated.  -/
Mathlib.Meta.FunProp.MaybeFunctionData.data : Mathlib.Meta.FunProp.FunctionData → Mathlib.Meta.FunProp.MaybeFunctionData
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffine.mk : ∀ {X : AlgebraicGeometry.Scheme}, CategoryTheory.IsIso X.toSpecΓ → AlgebraicGeometry.IsAffine X
-- Init.Data.Vector.Count
/-- This lemma is only relevant for `grind`.  -/
Std.Internal.Vector.countP_eq_zero_of_forall : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : Vector α n}, (∀ x ∈ xs, ¬p x = true) → Vector.countP p xs = 0
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.inv : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] {s : Set α},
  IsUpperSet s → IsLowerSet s⁻¹
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.IsExpansionOn.mk : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'} {M : Type u_1} [inst : L.Structure M]
  [inst_1 : L'.Structure M],
  autoParam
      (∀ {n : ℕ} (f : L.Functions n) (x : Fin n → M),
        FirstOrder.Language.Structure.funMap (ϕ.onFunction f) x = FirstOrder.Language.Structure.funMap f x)
      FirstOrder.Language.LHom.IsExpansionOn.map_onFunction._autoParam →
    autoParam
        (∀ {n : ℕ} (R : L.Relations n) (x : Fin n → M),
          FirstOrder.Language.Structure.RelMap (ϕ.onRelation R) x = FirstOrder.Language.Structure.RelMap R x)
        FirstOrder.Language.LHom.IsExpansionOn.map_onRelation._autoParam →
      ϕ.IsExpansionOn M
-- Mathlib.Topology.MetricSpace.HausdorffDimension
ContinuousLinearEquiv.dimH_image : ∀ {𝕜 : Type u_4} {E : Type u_5} {F : Type u_6} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (e : E ≃L[𝕜] F) (s : Set E),
  dimH (⇑e '' s) = dimH s
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.instContinuousEvalConst : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4}
  {F : Type u_5} [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜₂ F]
  [inst_6 : TopologicalSpace E] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E],
  ContinuousEvalConst (E →SL[σ] F) E F
-- Mathlib.Analysis.Normed.Ring.Basic
Units.nnnorm_pos : ∀ {α : Type u_2} [inst : NormedRing α] [Nontrivial α] (x : αˣ), 0 < ‖↑x‖₊
-- Mathlib.Combinatorics.Additive.Dissociation
mulDissociated_iff_sum_eq_subsingleton : ∀ {α : Type u_1} [inst : CommGroup α] {s : Set α},
  MulDissociated s ↔ ∀ (a : α), {t | ↑t ⊆ s ∧ ∏ x ∈ t, x = a}.Subsingleton
-- Mathlib.Topology.Order
nhds_nhdsAdjoint_of_ne : ∀ {α : Type u} {a b : α} (f : Filter α), b ≠ a → nhds b = pure b
-- Mathlib.Order.Antisymmetrization
AntisymmRel.rfl : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Refl r] {a : α}, AntisymmRel r a a
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
/-- A continuous affine equivalence, denoted `P₁ ≃ᴬ[k] P₂`, between two affine topological spaces
is an affine equivalence such that forward and inverse maps are continuous.  -/
ContinuousAffineEquiv : (k : Type u_1) →
  (P₁ : Type u_2) →
    (P₂ : Type u_3) →
      {V₁ : Type u_4} →
        {V₂ : Type u_5} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [Module k V₁] →
                [AddTorsor V₁ P₁] →
                  [TopologicalSpace P₁] →
                    [inst_5 : AddCommGroup V₂] →
                      [Module k V₂] → [AddTorsor V₂ P₂] → [TopologicalSpace P₂] → Type (max (max (max u_2 u_3) u_4) u_5)
-- Lean.Meta.MonadSimp
Lean.Meta.MonadSimp.simp : {m : Type → Type} → [self : Lean.Meta.MonadSimp m] → Lean.Expr → m Lean.Meta.MonadSimp.Result
-- Mathlib.Data.Finsupp.Lex
Finsupp.Colex.addLeftStrictMono : ∀ {α : Type u_1} {N : Type u_2} [inst : LinearOrder α] [inst_1 : AddMonoid N] [inst_2 : LinearOrder N]
  [AddLeftStrictMono N], AddLeftStrictMono (Colex (α →₀ N))
-- Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp
/-- The equivalences `Mon (Type u) ≌ MonCat.{u}` and `Grp (Type u) ≌ GrpCat.{u}`
are naturally compatible with the forgetful functors to `MonCat` and `Mon (Type u)`.
 -/
grpTypeEquivalenceGrpForget : GrpTypeEquivalenceGrp.functor.comp (CategoryTheory.forget₂ GrpCat MonCat) ≅
  (CategoryTheory.Grp.forget₂Mon (Type u)).comp MonTypeEquivalenceMon.functor
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
/-- Special case of `Function.Periodic.intervalIntegrable`: A periodic function is interval integrable
over every interval if it is interval integrable over the period starting from zero.
 -/
Function.Periodic.intervalIntegrable₀ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℝ → E} {T : ℝ},
  Function.Periodic f T →
    T ≠ 0 →
      IntervalIntegrable f MeasureTheory.volume 0 T → ∀ (a₁ a₂ : ℝ), IntervalIntegrable f MeasureTheory.volume a₁ a₂
-- Mathlib.Algebra.Group.Defs
/-- Typeclass for expressing that a type `M` with multiplication and a one satisfies
`1 * a = a` and `a * 1 = a` for all `a : M`.  -/
MulOneClass : Type u → Type u
-- Mathlib.CategoryTheory.Dialectica.Monoidal
CategoryTheory.Dial.associator_inv_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] (X Y Z : CategoryTheory.Dial C),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv.F =
    CategoryTheory.Limits.prod.lift
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst))
      (CategoryTheory.Limits.prod.lift
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd
          (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd))
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd))
-- Lean.Server.ServerTask
Lean.Server.ServerTask.mapCheap : {α : Type u_1} → {β : Type u_2} → (α → β) → Lean.Server.ServerTask α → Lean.Server.ServerTask β
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_isBasis_union_union : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α},
  M.IsBasis' (J ∪ I) (X ∪ I) → Disjoint J I → Disjoint X I → (M.contract I).IsBasis' J X
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The obvious fully faithful functor `toKaroubi` sends an object `X : C` to the obvious
formal direct factor of `X` given by `𝟙 X`.  -/
CategoryTheory.Idempotents.toKaroubi : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi C)
-- Mathlib.Order.Monotone.Basic
antitoneOn_comp_ofDual_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {s : Set α},
  AntitoneOn (f ∘ ⇑OrderDual.ofDual) s ↔ MonotoneOn f s
-- Mathlib.GroupTheory.Submonoid.Center
Submonoid.centerCongr.eq_1 : ∀ {M : Type u_2} {N : Type u_1} [inst : MulOneClass M] [inst_1 : MulOneClass N] (e : M ≃* N),
  Submonoid.centerCongr e = Subsemigroup.centerCongr e
-- Mathlib.AlgebraicTopology.TopologicalSimplex
SimplexCategory.instNonemptyCarrierObjTopCatToTop : ∀ (n : SimplexCategory), Nonempty ↑(SimplexCategory.toTop.{u}.obj n)
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropWithinAt_congr_of_mem : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g g' : M → M'} {s : Set M} {x : M},
  G.LocalInvariantProp G' P →
    ChartedSpace.LiftPropWithinAt P g s x → (∀ y ∈ s, g' y = g y) → x ∈ s → ChartedSpace.LiftPropWithinAt P g' s x
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parent_rootD : ∀ (self : Batteries.UnionFind) (x : ℕ), self.parent (self.rootD x) = self.rootD x
-- Mathlib.Analysis.Complex.ReImTopology
Complex.interior_preimage_re : ∀ (s : Set ℝ), interior (Complex.re ⁻¹' s) = Complex.re ⁻¹' interior s
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.mem_rat_span_latticeBasis : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : K),
  (NumberField.canonicalEmbedding K) x ∈ Submodule.span ℚ (Set.range ⇑(NumberField.canonicalEmbedding.latticeBasis K))
-- Mathlib.RingTheory.Algebraic.StronglyTranscendental
IsStronglyTranscendental.of_surjective_left : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T] {x : T},
  IsStronglyTranscendental R x → Function.Surjective ⇑(algebraMap R S) → IsStronglyTranscendental S x
-- Mathlib.Logic.Equiv.Set
Equiv.swap_bijOn_exchange : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Set α},
  a ∈ s → b ∉ s → Set.BijOn (⇑(Equiv.swap a b)) s (insert b (s \ {a}))
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.nhdsKer_singleton : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [Topology.IsUpperSet α] (a : α),
  nhdsKer {a} = Set.Ici a
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.inv_hom_apply : ∀ {M N : SemiNormedGrp₁} (e : M ≅ N) (r : M.carrier),
  ↑(SemiNormedGrp₁.Hom.hom e.inv) (↑(SemiNormedGrp₁.Hom.hom e.hom) r) = r
-- Init.Data.Nat.ToString
Nat.digitChar_eq_nine : ∀ {n : ℕ}, n.digitChar = '9' ↔ n = 9
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Finset.instMeasurableSingletonClass : ∀ {α : Type u_1} [Countable α], MeasurableSingletonClass (Finset α)
-- Mathlib.Analysis.Distribution.AEEqOfIntegralContDiff
/-- If a locally integrable function `f` on a finite-dimensional real vector space has zero integral
when multiplied by any smooth compactly supported function, then `f` vanishes almost everywhere.  -/
ae_eq_zero_of_integral_contDiff_smul_eq_zero : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type u_2}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [CompleteSpace F] [inst_6 : MeasurableSpace E]
  [BorelSpace E] {f : E → F} {μ : MeasureTheory.Measure E},
  MeasureTheory.LocallyIntegrable f μ →
    (∀ (g : E → ℝ), ContDiff ℝ (↑⊤) g → HasCompactSupport g → ∫ (x : E), g x • f x ∂μ = 0) → ∀ᵐ (x : E) ∂μ, f x = 0
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.unit_naturality : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) ⦃X Y : C⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (T.η.app Y) = CategoryTheory.CategoryStruct.comp (T.η.app X) (T.map f)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft.injEq : ∀ (e : Lean.Expr) (f g h : Mathlib.Tactic.BicategoryLike.Mor₁) (η : Mathlib.Tactic.BicategoryLike.Mor₂Iso)
  (e_1 : Lean.Expr) (f_1 g_1 h_1 : Mathlib.Tactic.BicategoryLike.Mor₁) (η_1 : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  (Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e f g h η =
      Mathlib.Tactic.BicategoryLike.Mor₂Iso.whiskerLeft e_1 f_1 g_1 h_1 η_1) =
    (e = e_1 ∧ f = f_1 ∧ g = g_1 ∧ h = h_1 ∧ η = η_1)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.contains_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k}, (m.insertIfNew k v).contains a = (k == a || m.contains a)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolParams.mk.injEq : ∀ (textDocument textDocument_1 : Lean.Lsp.TextDocumentIdentifier),
  ({ textDocument := textDocument } = { textDocument := textDocument_1 }) = (textDocument = textDocument_1)
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.DSimp.Methods.mk.inj : ∀ {pre post pre_1 post_1 : Lean.Meta.Sym.DSimp.DSimproc},
  { pre := pre, post := post } = { pre := pre_1, post := post_1 } → pre = pre_1 ∧ post = post_1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.all_eq_skipPrefixWhile_beq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  s.all pat = (s.skipPrefixWhile pat == s.endPos)
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.uniqueBaseOn_isNonloop_iff : ∀ {α : Type u_1} {e : α} {I E : Set α}, (Matroid.uniqueBaseOn I E).IsNonloop e ↔ e ∈ I ∩ E
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.ComonObj.instTensorUnit_counit : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.ComonObj.counit = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Category.Ring.Basic
/-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.

An example where this is needed is in applying `TopCat.Presheaf.restrictOpen` to commutative rings.
 -/
CommRingCat.forget_obj_eq_coe : CommRingCat → CommRingCat → Prop
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) {i' j' k' l' : ι}
  (f₁' : i' ⟶ j') (f₂' : j' ⟶ k') (f₃' : k' ⟶ l') {i'' j'' k'' l'' : ι} (f₁'' : i'' ⟶ j'') (f₂'' : j'' ⟶ k'')
  (f₃'' : k'' ⟶ l'')
  (α : CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃ ⟶ CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃')
  (β : CategoryTheory.ComposableArrows.mk₃ f₁' f₂' f₃' ⟶ CategoryTheory.ComposableArrows.mk₃ f₁'' f₂'' f₃'')
  (n₀ n₁ n₂ : ℤ) (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexMap_comp._auto_3)
  {Z : CategoryTheory.ShortComplex C} (h : X.shortComplex f₁'' f₂'' f₃'' n₀ n₁ n₂ ⋯ ⋯ ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (X.shortComplexMap f₁ f₂ f₃ f₁'' f₂'' f₃'' (CategoryTheory.CategoryStruct.comp α β) n₀ n₁ n₂ hn₁ hn₂) h =
    CategoryTheory.CategoryStruct.comp (X.shortComplexMap f₁ f₂ f₃ f₁' f₂' f₃' α n₀ n₁ n₂ hn₁ hn₂)
      (CategoryTheory.CategoryStruct.comp (X.shortComplexMap f₁' f₂' f₃' f₁'' f₂'' f₃'' β n₀ n₁ n₂ hn₁ hn₂) h)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.map₂Iso_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {U : CategoryTheory.Functor A B} {V : B} {F : C ≌ A} {G : D ≌ B}
  (α : F.functor.comp U ⟶ S.comp G.functor) (α' : F.inverse.comp S ⟶ U.comp G.inverse)
  (hα'α :
    CategoryTheory.CategoryStruct.comp S.leftUnitor.hom
        (CategoryTheory.CategoryStruct.comp S.rightUnitor.inv
          (CategoryTheory.CategoryStruct.comp (S.whiskerLeft G.unitIso.hom) (S.associator G.functor G.inverse).inv)) =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.unitIso.hom S)
        (CategoryTheory.CategoryStruct.comp (F.functor.associator F.inverse S).hom
          (CategoryTheory.CategoryStruct.comp (F.functor.whiskerLeft α')
            (CategoryTheory.CategoryStruct.comp (F.functor.associator U G.inverse).inv
              (CategoryTheory.Functor.whiskerRight α G.inverse)))))
  (hαα' :
    CategoryTheory.CategoryStruct.comp (F.inverse.whiskerLeft α)
        (CategoryTheory.CategoryStruct.comp (F.inverse.associator S G.functor).inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α' G.functor)
            (CategoryTheory.CategoryStruct.comp (U.associator G.inverse G.functor).hom
              (U.whiskerLeft G.counitIso.hom)))) =
      CategoryTheory.CategoryStruct.comp (F.inverse.associator F.functor U).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight F.counitIso.hom U)
          (CategoryTheory.CategoryStruct.comp U.leftUnitor.hom U.rightUnitor.inv)))
  (β : G.functor.obj T ⟶ V) (β' : G.inverse.obj V ⟶ T)
  (hββ' : CategoryTheory.CategoryStruct.comp (G.inverse.map β) β' = G.unitIso.inv.app T)
  (hβ'β : CategoryTheory.CategoryStruct.comp (G.functor.map β') β = G.counitIso.hom.app V),
  (CategoryTheory.CostructuredArrow.map₂Iso α α' hα'α hαα' β β' hββ' hβ'β).functor =
    CategoryTheory.CostructuredArrow.map₂ α β
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.re_inner_smul_ofReal_smul_self : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x : F) {t : ℝ},
  RCLike.re (inner 𝕜 (↑t • x) (↑t • x)) = InnerProductSpace.Core.normSq x * t * t
-- Mathlib.Order.BooleanGenerators
IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α} [IsCompactlyGenerated α],
  IsCompactlyGenerated.BooleanGenerators S → ∀ (a : α), IsAtom a → a ≤ sSup S → a ∈ S
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.turanGraph_zero : ∀ {n : ℕ}, SimpleGraph.turanGraph n 0 = ⊤
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.add_comp : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {π₃ : ContRepresentation R G U}
  (f g : ContIntertwiningMap π₂ π₃) (h : ContIntertwiningMap π₁ π₂), (f + g).comp h = f.comp h + g.comp h
-- Mathlib.Order.Monotone.Defs
StrictAnti.imp : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a b : α},
  StrictAnti f → a < b → f b < f a
-- Mathlib.Data.List.Sort
List.sortedGE_map_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {l : List αᵒᵈ}, (List.map (⇑OrderDual.ofDual) l).SortedGE ↔ l.SortedLE
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.summable_sigma : ∀ {α : Type u_1} {β : α → Type u_4} {f : (x : α) × β x → NNReal},
  Summable f ↔ (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩
-- Mathlib.Order.Monotone.Defs
StrictMono.strictMonoOn : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono f → ∀ (s : Set α), StrictMonoOn f s
-- Mathlib.Analysis.SpecialFunctions.Integrability.Basic
/-- See `intervalIntegrable_rpow'` for a version with a weaker hypothesis on `r`, but assuming the
measure is volume.  -/
intervalIntegral.intervalIntegrable_rpow : ∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [MeasureTheory.IsLocallyFiniteMeasure μ] {r : ℝ},
  0 ≤ r ∨ 0 ∉ Set.uIcc a b → IntervalIntegrable (fun x => x ^ r) μ a b
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.instTotallyDisconnectedSpaceAutFunctorFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat),
  TotallyDisconnectedSpace (CategoryTheory.Aut F)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensLegend.mk.inj : ∀ {tokenTypes tokenModifiers tokenTypes_1 tokenModifiers_1 : Array String},
  { tokenTypes := tokenTypes, tokenModifiers := tokenModifiers } =
      { tokenTypes := tokenTypes_1, tokenModifiers := tokenModifiers_1 } →
    tokenTypes = tokenTypes_1 ∧ tokenModifiers = tokenModifiers_1