mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.substAlgHom_coe : ∀ {R : Type u_2} [inst : CommRing R] {τ : Type u_3} {S : Type u_4} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {a : MvPowerSeries τ S} (ha : PowerSeries.HasSubst a) (p : Polynomial R),
  (PowerSeries.substAlgHom ha) ↑p = (Polynomial.aeval a) p
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.of_precomp : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {β : ι → Type u_8} {mβ : (i : ι) → MeasurableSpace (β i)}
  {_mα : MeasurableSpace α} {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α}
  {f : (x : ι) → Ω → β x} {ι' : Type u_9} {g : ι' → ι},
  Function.Surjective g →
    ProbabilityTheory.Kernel.iIndepFun (fun i => f (g i)) κ μ → ProbabilityTheory.Kernel.iIndepFun f κ μ
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
/-- To show that the pullback of the closed immersion `iX` along `f` is the closed immersion
`iY`, it suffices to check that the preimage of `ker iY` under `f` is `ker iX`.  -/
AlgebraicGeometry.isPullback_of_isClosedImmersion : ∀ {ZX ZY X Y : AlgebraicGeometry.Scheme} (iX : ZX ⟶ X) (iY : ZY ⟶ Y) (Zf : ZX ⟶ ZY) (f : X ⟶ Y)
  [AlgebraicGeometry.IsClosedImmersion iX] [AlgebraicGeometry.IsClosedImmersion iY],
  CategoryTheory.CategoryStruct.comp iX f = CategoryTheory.CategoryStruct.comp Zf iY →
    (AlgebraicGeometry.Scheme.Hom.ker iY).comap f = AlgebraicGeometry.Scheme.Hom.ker iX →
      CategoryTheory.IsPullback iX Zf f iY
-- Mathlib.Topology.Category.TopPair
TopPair.Homotopy.ext_iff : ∀ {X Y : TopPair} {f g : X ⟶ Y} {x y : TopPair.Homotopy f g}, x = y ↔ x.fst = y.fst ∧ x.snd = y.snd
-- Mathlib.Data.Set.Finite.Lattice
/-- **Alias** of `iSup_iInf_of_antitone`. -/
Set.iSup_iInf_of_antitone : ∀ {ι : Type u_1} {ι' : Type u_2} {α : Type u_3} [Finite ι] [inst : Preorder ι'] [Nonempty ι'] [IsCodirectedOrder ι']
  [inst_3 : Order.Frame α] {f : ι → ι' → α}, (∀ (i : ι), Antitone (f i)) → ⨆ j, ⨅ i, f i j = ⨅ i, ⨆ j, f i j
-- Init.Data.SInt.Lemmas
ISize.toInt_ofInt : ∀ {n : ℤ}, (ISize.ofInt n).toInt = n.bmod ISize.size
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.prodEquiv_apply : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] (f : (M →L[R] M₂) × (M →L[R] M₃)), ContinuousLinearMap.prodEquiv f = f.1.prod f.2
-- Mathlib.Data.Complex.Basic
Complex.ofReal_comp_add : ∀ {α : Type u_1} (f g : α → ℝ), Complex.ofReal ∘ (f + g) = Complex.ofReal ∘ f + Complex.ofReal ∘ g
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
MeasureTheory.measure_liminf_cofinite_eq_zero : ∀ {α : Type u_1} {ι : Type u_2} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α]
  [Countable ι] {μ : F} [Infinite ι] {s : ι → Set α}, ∑' (i : ι), μ (s i) ≠ ⊤ → μ (Filter.liminf s Filter.cofinite) = 0
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_neg : ∀ {a : UInt64}, (-a).toBitVec = -a.toBitVec
-- Mathlib.Order.CountableSupClosed
countableInfClosure_idem : ∀ {α : Type u_2} [inst : Preorder α] (s : Set α), countableInfClosure (countableInfClosure s) = countableInfClosure s
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Feature.builderOption.injEq : ∀ (o o_1 : Aesop.Frontend.BuilderOption),
  (Aesop.Frontend.Feature.builderOption o = Aesop.Frontend.Feature.builderOption o_1) = (o = o_1)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.MkPreResultResult.failed : Lean.Meta.Sym.MkPreResultResult✝
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.distinct_keys_toArray : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) (Std.DTreeMap.Internal.Impl.Const.toArray t).toList
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_X_le : ∀ {R : Type u} [inst : Semiring R], Polynomial.X.natDegree ≤ 1
-- Mathlib.GroupTheory.Generators
Group.Generators.mk.sizeOf_spec : ∀ {G : Type u_5} [inst : Group G] {ι : Type u_6} [inst_1 : SizeOf G] [inst_2 : SizeOf ι] (val : ι → G)
  (closure_eq_top : Subgroup.closure (Set.range val) = ⊤),
  sizeOf { val := val, closure_eq_top := closure_eq_top } = 1 + sizeOf closure_eq_top
-- Std.Time.Date.Basic
/-- Convert `Hour.Offset` into `Day.Offset`.
 -/
Std.Time.Hour.Offset.toDays : Std.Time.Hour.Offset → Std.Time.Day.Offset
-- Std.Do.PostCond
Std.Do.ExceptConds.entails.eq_1 : ∀ (x_2 y_2 : Std.Do.ExceptConds Std.Do.PostShape.pure), x_2.entails y_2 = True
-- Batteries.CodeAction.Misc
/-- Returns the explicit arguments given a type. The second argument of this
function is an accumulator.  -/
Batteries.CodeAction.getExplicitArgs : Lean.Expr → Array Lean.Name → Array Lean.Name
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.coconeUnopOfConeEquiv_functor_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ} (c : (CategoryTheory.Limits.Cone F)ᵒᵖ),
  CategoryTheory.Limits.coconeUnopOfConeEquiv.functor.obj c = CategoryTheory.Limits.coconeUnopOfCone (Opposite.unop c)
-- Mathlib.Data.List.Sort
List.SortedGT.getElem_le_getElem_iff : ∀ {α : Type u_1} {l : List α} [inst : LinearOrder α],
  l.SortedGT → ∀ {i j : ℕ} {hi : i < l.length} {hj : j < l.length}, l[i] ≤ l[j] ↔ j ≤ i
-- Std.Sync.SharedMutex
/-- `mutex.tryAtomicallyRead k` tries to lock `mutex` for shared read access and runs `k` with read
access to the mutex's state if it succeeds. If successful, it returns the value of `k`
as `some`, otherwise `none`.

Calling `mutex.tryAtomicallyRead` while already holding the underlying `BaseSharedMutex` in the
same thread is undefined behavior.
 -/
Std.SharedMutex.tryAtomicallyRead : {m : Type → Type u_1} →
  {α β : Type} → [Monad m] → [MonadLiftT BaseIO m] → [MonadFinally m] → Std.SharedMutex α → ReaderT α m β → m (Option β)
-- Lean.Parser.Module.Syntax
Lean.Parser.Module.meta.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.ReduceModChar
Tactic.ReduceModChar.CharP.neg_mul_eq_sub_one_mul : ∀ {α : Type u_1} [inst : Ring α] (n : ℕ),
  CharP α n →
    ∀ (a b : α) (na : ℕ) (na' : α), Mathlib.Meta.NormNum.IsNat ((↑n - 1) * a) na → ↑na = na' → -(a * b) = na' * b
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.bind₁_verschiebungPoly_wittPolynomial : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] (n : ℕ),
  (MvPolynomial.bind₁ WittVector.verschiebungPoly) (wittPolynomial p ℤ n) =
    if n = 0 then 0 else ↑p * wittPolynomial p ℤ (n - 1)
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_neg : ∀ {a : UInt16}, (-a).toBitVec = -a.toBitVec
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
/-- **Alias** of `ContMDiffOn.curry_left`.

---

Curried `C^n` functions are `C^n` in the first coordinate.  -/
ContMDiffOn.along_fst : ∀ {𝕜 : 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 : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : M → M' → N} {s : Set (M × M')},
  ContMDiffOn (I.prod I') J n (Function.uncurry f) s → ∀ {y : M'}, ContMDiffOn I J n (fun x => f x y) {x | (x, y) ∈ s}
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.Basic
CategoryTheory.LocalizerMorphism.instHasLeftResolutionsIdOfContainsIdentities : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁}
  [W₁.ContainsIdentities], (CategoryTheory.LocalizerMorphism.id W₁).HasLeftResolutions
-- Mathlib.RingTheory.Congruence.BigOperators
RingCon.coe_dfinsuppSumAddHom : ∀ {ι : Type u_1} {β : ι → Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : Mul M]
  [inst_3 : (i : ι) → AddCommMonoid (β i)] (c : RingCon M) (h : (i : ι) → β i →+ M) (f : Π₀ (i : ι), β i),
  ↑((DFinsupp.sumAddHom h) f) = (DFinsupp.sumAddHom fun i => c.toAddCon.mk'.comp (h i)) f
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic
/-- The adjunction `Hom(Cⁿ(-, X), F) ≃ Hom(X, F(Δ[n]))` for `R : C` and `F : SSet ⥤ C`.  -/
SSet.chainComplexFunctorAdjunction : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasCoproducts C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        (n : ℕ) →
          (CategoryTheory.Functor.postcompose₂.obj (HomologicalComplex.eval C (ComplexShape.down ℕ) n)).obj
              (SSet.chainComplexFunctor C) ⊣
            (CategoryTheory.evaluation SSet C).obj (SSet.stdSimplex.obj { len := n })
-- Lean.Meta.Tactic.Backtrack
/-- Maximum recursion depth.  -/
Lean.Meta.Tactic.Backtrack.BacktrackConfig.maxDepth : Lean.Meta.Tactic.Backtrack.BacktrackConfig → ℕ
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.annihilator.eq_1 : ∀ (R : Type u_1) [inst : CommMonoidWithZero R] {n : ℕ} (H : Set (ZMod n)ˣ),
  DirichletCharacter.annihilator R H =
    (MulChar.domRestrictHom (Submonoid.map (Units.coeHom (ZMod n)) (Submonoid.closure H)) R).ker
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
/-- The diagram
```
v.adicCompletionIntegers ℚ  <-----  ℤ_[primesEquiv v]
      |                               |
      |                               |
      v                               v
v.adicCompletion ℚ  <-------------  ℚ_[primesEquiv v]
```
commutes.  -/
Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R)
  (x : ℤ_[↑(Rat.HeightOneSpectrum.primesEquiv v)]),
  ↑((Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv v).symm x) =
    (Rat.HeightOneSpectrum.adicCompletion.padicEquiv v).symm ↑x
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.equivalenceFromModel.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L L_1 : CategoryTheory.Functor C D) (e_L : L = L_1)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : L.IsLocalization W],
  CategoryTheory.Localization.equivalenceFromModel L W = CategoryTheory.Localization.equivalenceFromModel L_1 W
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instConcreteCategoryContinuousLinearMapIdCarrier : (R : Type u) →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      CategoryTheory.ConcreteCategory (TopModuleCat R) fun x1 x2 => ↑x1.toModuleCat →L[R] ↑x2.toModuleCat
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEFinStronglyMeasurable.inf : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
  {f g : α → β} [inst_1 : Zero β] [inst_2 : SemilatticeInf β] [ContinuousInf β],
  MeasureTheory.AEFinStronglyMeasurable f μ →
    MeasureTheory.AEFinStronglyMeasurable g μ → MeasureTheory.AEFinStronglyMeasurable (f ⊓ g) μ
-- Std.Time.Time.Unit.Basic
/-- Converts a `Nanosecond.Offset` to an `Hour.Offset`.
 -/
Std.Time.Hour.Offset.ofNanoseconds : Std.Time.Nanosecond.Offset → Std.Time.Hour.Offset
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- `Mor₂` expressions defined below will have the `isoLift? : Option IsoLift` field.
For `η : Mor₂` such that `η.isoLift? = some isoLift`, we have the following data:
- `isoLift.e`: an expression for a 2-isomorphism `η'`, given as a `Mor₂Iso` term,
- `isoLift.eq`: a lean expression for the proof that `η'.hom = η`.
 -/
Mathlib.Tactic.BicategoryLike.IsoLift : Type
-- Init.Data.Int.Gcd
Int.gcd_add_mul_right_right : ∀ (m n k : ℤ), m.gcd (n + k * m) = m.gcd n
-- Mathlib.Order.BoundedOrder.Basic
dite_ne_bot : ∀ {α : Type u} [inst : Bot α] {p : Prop} [inst_1 : Decidable p] {a : p → α} {b : ¬p → α},
  (∀ (h : p), a h ≠ ⊥) → (∀ (h : ¬p), b h ≠ ⊥) → (if h : p then a h else b h) ≠ ⊥
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix.injEq : ∀ (lhs : Bool) (s : Lean.Grind.AC.Seq) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr)
  (lhs_1 : Bool) (s_1 : Lean.Grind.AC.Seq) (c₁_1 : Lean.Meta.Grind.AC.EqCnstr) (c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr),
  (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix lhs s c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_prefix lhs_1 s_1 c₁_1 c₂_1) =
    (lhs = lhs_1 ∧ s = s_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
/-- The projection `∫ F ⥤ 𝒮` given by projecting both objects and homs to the first factor.  -/
CategoryTheory.Pseudofunctor.Grothendieck.forget : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat) →
      CategoryTheory.Functor F.Grothendieck 𝒮
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.instTopWideSubquiver : {V : Type u_1} → [inst : Quiver V] → Top (WideSubquiver V)
-- Mathlib.Algebra.Order.ToIntervalMod
/-- The unique integer such that this multiple of `p`, subtracted from `b`, is in `Ico a (a + p)`.  -/
toIcoDiv : {α : Type u_1} →
  [inst : AddCommGroup α] →
    [inst_1 : LinearOrder α] → [IsOrderedAddMonoid α] → [hα : Archimedean α] → {p : α} → 0 < p → α → α → ℤ
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- A version of `MultilinearMap.cons_add` for `AlternatingMap`.  -/
AlternatingMap.map_vecCons_add : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {n : ℕ} (f : M [⋀^Fin n.succ]→ₗ[R] N) (m : Fin n → M) (x y : M),
  f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContext : Type
-- Mathlib.Topology.ContinuousMap.Algebra
/-- Evaluation at a point, as a continuous linear map.  -/
ContinuousMap.evalCLM : {α : Type u_1} →
  [inst : TopologicalSpace α] →
    (R : Type u_3) →
      {M : Type u_5} →
        [inst_1 : TopologicalSpace M] →
          [inst_2 : Semiring R] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : ContinuousAdd M] →
                [inst_5 : Module R M] → [inst_6 : ContinuousConstSMul R M] → α → C(α, M) →L[R] M
-- Mathlib.MeasureTheory.Group.Measure
/-- An alternative way to prove that `μ` is left invariant under addition.  -/
MeasureTheory.forall_measure_preimage_add_iff : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Add G] [MeasurableAdd G] (μ : MeasureTheory.Measure G),
  (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g + h) ⁻¹' A) = μ A) ↔ μ.IsAddLeftInvariant
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.coe_toSL2R : ∀ (z : UpperHalfPlane), ↑z.toSL2R = !![√z.im, z.re / √z.im; 0, 1 / √z.im]
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.reindexRange_repr_self : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) (i : ι), b.reindexRange.repr (b i) = fun₀ | ⟨b i, ⋯⟩ => 1
-- Mathlib.CategoryTheory.Comma.Over.Pullback
CategoryTheory.Over.pullback_obj_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasPullbacksAlong f] (g : CategoryTheory.Over Y),
  ((CategoryTheory.Over.pullback f).obj g).hom = CategoryTheory.Limits.pullback.snd g.hom f
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.CartesianMonoidalCategory.lift_apply : ∀ {X Y Z : Type u} {f : X ⟶ Y} {g : X ⟶ Z} {x : X},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CartesianMonoidalCategory.lift f g)) x =
    ((CategoryTheory.ConcreteCategory.hom f) x, (CategoryTheory.ConcreteCategory.hom g) x)
-- Mathlib.Order.Bounds.Basic
lowerBounds_mono_of_isCoinitialFor : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α}, IsCoinitialFor s t → lowerBounds t ⊆ lowerBounds s
-- Init.Data.SInt.Lemmas
Int8.toInt64_le : ∀ {a b : Int8}, a.toInt64 ≤ b.toInt64 ↔ a ≤ b
-- Mathlib.Algebra.Homology.ExactSequence
/-- The short complex consisting of maps `S.map' i j` and `S.map' j k` when we know
that `S : ComposableArrows C n` satisfies `S.IsComplex`.  -/
CategoryTheory.ComposableArrows.sc' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {n : ℕ} →
        (S : CategoryTheory.ComposableArrows C n) →
          S.IsComplex →
            (i j k : ℕ) →
              autoParam (i + 1 = j) CategoryTheory.ComposableArrows.sc'._auto_1 →
                autoParam (j + 1 = k) CategoryTheory.ComposableArrows.sc'._auto_3 →
                  autoParam (k ≤ n) CategoryTheory.ComposableArrows.sc'._auto_5 → CategoryTheory.ShortComplex C
-- Mathlib.CategoryTheory.ComposableArrows.Two
/-- The morphism `mk₁ fg ⟶ mk₁ g` when `f ≫ g = fg` for some morphism `f`.  -/
CategoryTheory.ComposableArrows.twoδ₁Toδ₀ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {i j k : C} →
      (f : i ⟶ j) →
        (g : j ⟶ k) →
          (fg : i ⟶ k) →
            autoParam (CategoryTheory.CategoryStruct.comp f g = fg) CategoryTheory.ComposableArrows.twoδ₁Toδ₀._auto_1 →
              (CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ g)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncLTι_comp_truncGEπ_app_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) (n : ℤ) (X : C) {Z : C} (h : (t.truncGE n).obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.truncLTι n).app X)
      (CategoryTheory.CategoryStruct.comp ((t.truncGEπ n).app X) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.GroupTheory.Nilpotent
Group.nilpotencyClass_le_one_of_isSimple_of_isNilpotent : ∀ {G : Type u_1} [inst : Group G] [IsSimpleGroup G] [Group.IsNilpotent G], Group.nilpotencyClass G ≤ 1
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_id : ∀ (R : CommRingCat),
  AlgebraicGeometry.Spec.map (CategoryTheory.CategoryStruct.id R) =
    CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R)
-- Mathlib.GroupTheory.Submonoid.Inverses
AddSubmonoid.leftNeg_leftNeg_le : ∀ {M : Type u_1} [inst : AddMonoid M] (S : AddSubmonoid M), S.leftNeg.leftNeg ≤ S
-- Mathlib.CategoryTheory.FintypeCat
/-- Given any object of `FintypeCat.Skeleton`, this returns the associated natural number.  -/
FintypeCat.Skeleton.len : FintypeCat.Skeleton → ℕ
-- Mathlib.LinearAlgebra.Projectivization.Action
Matrix.ProjectiveSpecialLinearGroup.smul_proj_mk : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι]
  (g : Matrix.SpecialLinearGroup ι K) (p : Projectivization K (ι → K)), ↑g • p = g • p
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- Constant map as a `C^n` map  -/
ContMDiffMap.const : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {E' : Type u_3} →
            [inst_3 : NormedAddCommGroup E'] →
              [inst_4 : NormedSpace 𝕜 E'] →
                {H : Type u_4} →
                  [inst_5 : TopologicalSpace H] →
                    {H' : Type u_5} →
                      [inst_6 : TopologicalSpace H'] →
                        {I : ModelWithCorners 𝕜 E H} →
                          {I' : ModelWithCorners 𝕜 E' H'} →
                            {M : Type u_6} →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace H M] →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] → {n : WithTop ℕ∞} → M' → ContMDiffMap I I' M M' n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get?_eq_some_get : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} (h : a ∈ m), m.get? a = some (m.get a h)
-- Mathlib.Analysis.InnerProductSpace.PiL2
LinearIsometryEquiv.ofEq.congr_simp : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] {R' : Type u_12} [inst_1 : Ring R'] [inst_2 : Module R' E]
  (p q : Submodule R' E) (hpq : p = q), LinearIsometryEquiv.ofEq p q hpq = LinearIsometryEquiv.ofEq p q hpq
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.cochainComplex_d : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (n m : ℤ),
  h.cochainComplex.d n m = h.d n m
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiffAt.fst : ∀ {𝕜 : 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 : Type u_8}
  [inst_11 : NormedAddCommGroup F] [inst_12 : NormedSpace 𝕜 F] {G : Type u_9} [inst_13 : TopologicalSpace G]
  {J : ModelWithCorners 𝕜 F G} {N : Type u_10} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n : WithTop ℕ∞} {f : N → M × M'} {x : N}, ContMDiffAt J (I.prod I') n f x → ContMDiffAt J I n (fun x => (f x).1) x
-- Lean.Meta.Tactic.Grind.Cases
Lean.Meta.Grind.CasesEntry.mk.injEq : ∀ (declName : Lean.Name) (eager : Bool) (declName_1 : Lean.Name) (eager_1 : Bool),
  ({ declName := declName, eager := eager } = { declName := declName_1, eager := eager_1 }) =
    (declName = declName_1 ∧ eager = eager_1)
-- Mathlib.Order.Filter.Finite
Filter.EventuallyEq.iUnion : ∀ {α : Type u} {ι : Sort x} {l : Filter α} [Finite ι] {s t : ι → Set α},
  (∀ (i : ι), s i =ᶠ[l] t i) → ⋃ i, s i =ᶠ[l] ⋃ i, t i
-- Mathlib.Topology.MetricSpace.Polish
instTopologicalSpaceSum.eq_1 : ∀ {X : Type u} {Y : Type v} [t₁ : TopologicalSpace X] [t₂ : TopologicalSpace Y],
  instTopologicalSpaceSum = TopologicalSpace.coinduced Sum.inl t₁ ⊔ TopologicalSpace.coinduced Sum.inr t₂
-- Mathlib.Data.Part
Part.mul_def : ∀ {α : Type u_1} [inst : Mul α] (a b : Part α),
  a * b = do
    let y ← a
    Part.map (fun x => y * x) b
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.t_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] (D : CategoryTheory.GlueData C) (i j : D.J) {Z : C}
  (h : D.V (i, j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (D.t i j) (CategoryTheory.CategoryStruct.comp (D.t j i) h) = h
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.maxOn?.eq_def : ∀ {β : Type u_1} {α : Type u_2} [i : LE β] [inst : DecidableLE β] (f : α → β) (l : List α),
  List.maxOn? f l = List.minOn? f l