mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.FineSubfamilyOn.index_countable : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s) [SecondCountableTopology X],
  h.index.Countable
-- Mathlib.MeasureTheory.Group.Prod
/-- The map `(x, y) ↦ (x, xy)` as a `MeasurableEquiv`.  -/
MeasurableEquiv.shearMulRight : (G : Type u_1) →
  [inst : MeasurableSpace G] → [inst_1 : Group G] → [MeasurableMul₂ G] → [MeasurableInv G] → G × G ≃ᵐ G × G
-- Mathlib.Topology.ContinuousMap.Interval
/-- The concatenation of compatible pairs of continuous maps on adjacent intervals, defined as a
`ContinuousMap` on a subtype of the product.  -/
ContinuousMap.concatCM : {α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] →
      [OrderTopology α] →
        {a b c : α} →
          [inst_3 : Fact (a ≤ b)] →
            [inst_4 : Fact (b ≤ c)] →
              {E : Type u_2} → [inst_5 : TopologicalSpace E] → C({ fg // fg.1 ⊤ = fg.2 ⊥ }, C(↑(Set.Icc a c), E))
-- Mathlib.Topology.Sion
Sion.exists_lt_iInf_of_lt_iInf_of_sup : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  X.Nonempty →
    IsCompact X →
      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
          ∀ [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F],
            Convex ℝ Y →
              (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                  ∀ [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F] {y1 : F},
                    y1 ∈ Y →
                      ∀ {y2 : F},
                        y2 ∈ Y → ∀ {t : β}, (∀ x ∈ X, t < max (f x y1) (f x y2)) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
-- Init.GrindInstances.Ring.SInt
Lean.Grind.Int64.intCast_ofNat : ∀ (x : ℕ), ↑(OfNat.ofNat x) = OfNat.ofNat x
-- Mathlib.GroupTheory.Submonoid.Center
Subsemigroup.centerCongr_apply_coe : ∀ {M : Type u_2} {N : Type u_1} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (r : ↥(Subsemigroup.center M)),
  ↑((Subsemigroup.centerCongr e) r) = e ↑r
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.mulMap_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  (A B : Subalgebra R S) (a : ↥A) (b : ↥B), (A.mulMap B) (a ⊗ₜ[R] b) = ↑a * ↑b
-- Mathlib.Algebra.Module.Presentation.Differentials
Algebra.Presentation.differentials.comm₁₂_single : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (pres : Algebra.Presentation R S ι σ) (r : σ),
  pres.toExtension.cotangentComplex ((Algebra.Presentation.differentials.hom₁ pres) fun₀ | r => 1) =
    pres.cotangentSpaceBasis.repr.symm (pres.differentialsRelations.relation r)
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.restrict_smul_one : ∀ {R : Type u_10} {M : Type u_11} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p : Submodule R M} (μ : R) (h : optParam (∀ x ∈ p, (μ • 1) x ∈ p) ⋯), LinearMap.restrict (μ • 1) h = μ • 1
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.oppositeRightAction_actionHom_op : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {d d' : D} {c c' : C} (f : d ⟶ d') (g : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f.op g.op =
    Opposite.op (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHom f g)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves limits, then `F.leftOp : Cᵒᵖ ⥤ D` preserves colimits.  -/
CategoryTheory.Limits.preservesColimitsOfSize_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.PreservesLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.PreservesColimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F.leftOp
-- Init.Data.List.Scan.Lemmas
List.scanl_eq_scanr_reverse : ∀ {β : Type u_1} {α : Type u_2} {init : β} {as : List α} {f : β → α → β},
  List.scanl f init as = (List.scanr (flip f) init as.reverse).reverse
-- Mathlib.RingTheory.Ideal.Height
Ideal.height_le_ringKrullDim_of_ne_top : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R}, I ≠ ⊤ → ↑I.height ≤ ringKrullDim R
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `spectralNorm K L y` is nonnegative.  -/
spectralNorm_nonneg : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] (y : L),
  0 ≤ spectralNorm K L y
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.opComm_apply_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (a : A ≃ₐ[R] Bᵐᵒᵖ) (a_1 : Aᵐᵒᵖ),
  (AlgEquiv.opComm a) a_1 = MulOpposite.unop (a (MulOpposite.unop a_1))
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
eq_zero_of_ne_zero_of_mul_left_eq_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x y : M₀} [NoZeroDivisors M₀], x ≠ 0 → x * y = 0 → y = 0
-- Mathlib.Algebra.Homology.Embedding.Basic
/-- The embedding from `down ℕ` to `up ℤ` with sends `n` to `-n`.  -/
ComplexShape.embeddingDownNat : (ComplexShape.down ℕ).Embedding (ComplexShape.up ℤ)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RiiSlice.instToIterator : {α : Type u} →
  Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RiiSliceData α)) Id
    (Std.Iterators.Types.Map (Std.DTreeMap.Internal.Zipper α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
      pure b.fst)
    α
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.addConst_k.eq_1 : ∀ (p : Int.Internal.Linear.Poly) (k : ℤ),
  p.addConst_k k =
    Int.Internal.Linear.Poly.rec (fun k' => Int.Internal.Linear.Poly.num (k.add k'))
      (fun k' v' x ih => Int.Internal.Linear.Poly.add k' v' ih) p
-- Init.Data.Int.Basic
instOfNat : {n : ℕ} → OfNat ℤ n
-- Mathlib.Order.Interval.Set.ProjIcc
Set.projIcc_left : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α} (h : a ≤ b), Set.projIcc a b h a = ⟨a, ⋯⟩
-- Mathlib.Topology.Germ
forall_restrictGermPredicate_iff : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y} {A : Set X}
  {P : (x : X) → (nhds x).Germ Y → Prop}, (∀ (x : X), RestrictGermPredicate P A x ↑f) ↔ ∀ᶠ (x : X) in nhdsSet A, P x ↑f
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The center of a semiring acts commutatively on that semiring.  -/
Subsemiring.center.smulCommClass_left : ∀ {R' : Type u_1} [inst : Semiring R'], SMulCommClass (↥(Subsemiring.center R')) R' R'
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mrange.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f f_1 : F), f = f_1 → MonoidHom.mrange f = MonoidHom.mrange f_1
-- Mathlib.Topology.ContinuousMap.Star
/-- `ContinuousMap.compStarAlgHom'` is functorial.  -/
ContinuousMap.compStarAlgHom'_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (𝕜 : Type u_4) [inst_3 : CommSemiring 𝕜] (A : Type u_5) [inst_4 : TopologicalSpace A]
  [inst_5 : Semiring A] [inst_6 : IsTopologicalSemiring A] [inst_7 : Star A] [inst_8 : ContinuousStar A]
  [inst_9 : Algebra 𝕜 A] (g : C(Y, Z)) (f : C(X, Y)),
  ContinuousMap.compStarAlgHom' 𝕜 A (g.comp f) =
    (ContinuousMap.compStarAlgHom' 𝕜 A f).comp (ContinuousMap.compStarAlgHom' 𝕜 A g)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.isIso_toCycles : ∀ {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 : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ),
  CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ f)) →
    CategoryTheory.IsIso (X.toCycles f g fg h n)
-- Mathlib.Topology.UniformSpace.Completion
/-- Extend a uniformly continuous function `α → β` to a function `CauchyFilter α → β`.
Outputs junk when `f` is not uniformly continuous.  -/
CauchyFilter.extend : {α : Type u} → [inst : UniformSpace α] → {β : Type v} → [UniformSpace β] → (α → β) → CauchyFilter α → β
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.mem_bot : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] {x : E} [inst_6 : T1Space E],
  x ∈ ⊥ ↔ x = 0
-- Lean.Elab.Term.TermElabM
/-- Manages reuse information for nested tactics by `split`ting given syntax into an outer and inner
part. `act` is then run on the inner part but with reuse information adjusted as following:
* If the old (from `tacSnap?`'s `SyntaxGuarded.stx`) and new (from `stx`) outer syntax are not
  identical according to `Syntax.eqWithInfo`, reuse is disabled.
* Otherwise, the old syntax as stored in `tacSnap?` is updated to the old *inner* syntax.
* In any case, `withReuseContext` is used on the new inner syntax to further prepare the monadic
  context.

For any tactic that participates in reuse, `withNarrowedTacticReuse` should be applied to the
tactic's syntax and `act` should be used to do recursive tactic evaluation of nested parts. Also,
after this function, `getAndEmptySnapshotTasks` should be called and the result stored in a snapshot
so that the tasks don't end up in a snapshot further up and are cancelled together with it; see
note [Incremental Cancellation].
 -/
Lean.Elab.Term.withNarrowedTacticReuse : {m : Type → Type} →
  {α : Type} →
    [Monad m] →
      [MonadReaderOf Lean.Elab.Term.Context m] →
        [MonadLiftT BaseIO m] →
          [MonadWithReaderOf Lean.Core.Context m] →
            [MonadWithReaderOf Lean.Elab.Term.Context m] →
              [Lean.MonadOptions m] →
                (Lean.Syntax → Lean.Syntax × Lean.Syntax) → (Lean.Syntax → m α) → Lean.Syntax → m α
-- Mathlib.Algebra.Group.Defs
mul_right_injective : ∀ {G : Type u_1} [inst : Mul G] [IsLeftCancelMul G] (a : G), Function.Injective fun x => a * x
-- Mathlib.Topology.Separation.Basic
/-- **Alias** of `Dense.sdiff_finite`.

---

Removing a finite set from a dense set in a space without isolated points, one still
obtains a dense set.  -/
Dense.diff_finite : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] [∀ (x : X), (nhdsWithin x {x}ᶜ).NeBot] {s : Set X},
  Dense s → ∀ {t : Set X}, t.Finite → Dense (s \ t)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) (h : S₁.LeftHomologyData) [inst_2 : CategoryTheory.Epi φ.τ₁]
  [inst_3 : CategoryTheory.IsIso φ.τ₂] [inst_4 : CategoryTheory.Mono φ.τ₃],
  (CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono φ h).i = CategoryTheory.CategoryStruct.comp h.i φ.τ₂
-- Mathlib.Algebra.Group.Hom.Instances
/-- The expression `fun m q ↦ f m (g q)` as an `AddMonoidHom`.

Note that the expression `fun q n ↦ f (g q) n` is simply `AddMonoidHom.comp`.

This also exists as a `LinearMap` version, `LinearMap.compl₂`  -/
AddMonoidHom.compl₂ : {M : Type uM} →
  {N : Type uN} →
    {P : Type uP} →
      {Q : Type uQ} →
        [inst : AddZeroClass M] →
          [inst_1 : AddZeroClass N] →
            [inst_2 : AddCommMonoid P] → [inst_3 : AddZeroClass Q] → (M →+ N →+ P) → (Q →+ N) → M →+ Q →+ P
-- Mathlib.Data.Multiset.UnionInter
Multiset.Nodup.add_iff : ∀ {α : Type u_1} {s t : Multiset α}, s.Nodup → t.Nodup → ((s + t).Nodup ↔ Disjoint s t)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Basic
/-- A normal epi category is a category in which every epimorphism is normal.  -/
CategoryTheory.IsNormalEpiCategory : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_pow : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : AddMonoid ι] [inst_2 : Semiring M]
  (f : AddMonoidAlgebra M ι) (n : ℕ), (f ^ n).toDirectSum = f.toDirectSum ^ n
-- Aesop.Tree.Data
Aesop.RappData.id : {Goal MVarCluster : Type} → Aesop.RappData Goal MVarCluster → Aesop.RappId
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getLE!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  t₁.Equiv t₂ → t₁.getLE! k = t₂.getLE! k
-- Mathlib.Data.Matrix.Diagonal
Matrix.diag_add : ∀ {n : Type u_3} {α : Type v} [inst : Add α] (A B : Matrix n n α), (A + B).diag = A.diag + B.diag
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- `Multifork.toPiFork` as a functor.  -/
CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        {c : CategoryTheory.Limits.Fan I.left} →
          CategoryTheory.Limits.IsLimit c →
            {d : CategoryTheory.Limits.Fan I.right} →
              (hd : CategoryTheory.Limits.IsLimit d) →
                CategoryTheory.Functor (CategoryTheory.Limits.Multifork I)
                  (CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd))
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Given a Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and another morphism
`φ' : a' ⟶ b` which also lifts `f`. Then any morphism `ψ : a' ⟶ a` lifting `𝟙 R` such that
`g ≫ ψ = φ'` must equal the map induced from the universal property of `φ`.  -/
CategoryTheory.Functor.IsCartesian.map_uniq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [inst_2 : p.IsCartesian f φ] {a' : 𝒳}
  (φ' : a' ⟶ b) [inst_3 : p.IsHomLift f φ'] (ψ : a' ⟶ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ],
  CategoryTheory.CategoryStruct.comp ψ φ = φ' → ψ = CategoryTheory.Functor.IsCartesian.map p f φ φ'
-- Mathlib.RingTheory.LocalProperties.InjectiveDimension
ModuleCat.injectiveDimension_eq_iSup_localizedModule_prime : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] [IsNoetherianRing R] (M : ModuleCat R),
  CategoryTheory.injectiveDimension M = ⨆ p, CategoryTheory.injectiveDimension (M.localizedModule p.asIdeal.primeCompl)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.ext : ∀ {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {f g : SlashInvariantForm Γ k},
  (∀ (x : UpperHalfPlane), f x = g x) → f = g
-- Mathlib.Algebra.Polynomial.Div
Polynomial.divByMonic_eq_of_not_monic : ∀ {R : Type u} [inst : Ring R] {q : Polynomial R} (p : Polynomial R), ¬q.Monic → p /ₘ q = 0
-- Mathlib.Analysis.Complex.TaylorSeries
/-- A function that is complex differentiable on the open ball of radius `r` around `c`
is given by evaluating its Taylor series at `c` on this open ball.  -/
Complex.taylorSeries_eq_on_ball' : ∀ ⦃c : ℂ⦄ ⦃r : ℝ⦄ ⦃z : ℂ⦄,
  z ∈ Metric.ball c r →
    ∀ {f : ℂ → ℂ},
      DifferentiableOn ℂ f (Metric.ball c r) → ∑' (n : ℕ), (↑n.factorial)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.mk.sizeOf_spec : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [inst : SizeOf ι] (toPrepartition : BoxIntegral.Prepartition I)
  (tag : BoxIntegral.Box ι → ι → ℝ) (tag_mem_Icc : ∀ (J : BoxIntegral.Box ι), tag J ∈ BoxIntegral.Box.Icc I),
  sizeOf { toPrepartition := toPrepartition, tag := tag, tag_mem_Icc := tag_mem_Icc } = 1 + sizeOf toPrepartition
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonFoldingRangeParams : Lean.FromJson Lean.Lsp.FoldingRangeParams
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.Measure.rnDeriv_mul_rnDeriv' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν κ : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [MeasureTheory.SigmaFinite κ],
  ν.AbsolutelyContinuous κ → μ.rnDeriv ν * ν.rnDeriv κ =ᵐ[ν] μ.rnDeriv κ
-- Mathlib.Algebra.Tropical.Basic
Tropical.untrop_trop : ∀ {R : Type u} (x : R), Tropical.untrop (Tropical.trop x) = x
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat),
  AddGrpCat.FilteredColimits.colimit F = AddGrpCat.of ↑(AddGrpCat.FilteredColimits.G F)
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_δ₀Iter_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter_δ₀Iter._auto_1) {Z : C}
  (h : X.obj (Opposite.op { len := n }) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.σ₀Iter i hi) (CategoryTheory.CategoryStruct.comp (X.δ₀Iter i hi) h) = h
-- Mathlib.GroupTheory.ArchimedeanDensely
LinearOrderedAddCommGroup.closure_equiv_closure.eq_1 : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [inst_2 : IsOrderedAddMonoid G]
  [inst_3 : AddCommGroup G'] [inst_4 : LinearOrder G'] [inst_5 : IsOrderedAddMonoid G'] (x : G) (y : G')
  (hxy : x = 0 ↔ y = 0),
  LinearOrderedAddCommGroup.closure_equiv_closure x y hxy =
    if hx : x = 0 then
      { toFun := fun x_1 => ⟨0, ⋯⟩, invFun := fun x_1 => ⟨0, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_add' := ⋯,
        map_le_map_iff' := ⋯ }
    else
      let x' := max x (-x);
      have hx' := ⋯;
      have xpos := ⋯;
      let y' := max y (-y);
      have hy' := ⋯;
      have ypos := ⋯;
      have hxc := ⋯;
      have hyc := ⋯;
      have Hx := ⋯;
      have Hy := ⋯;
      { toAddEquiv := addEquivOfAddOrderOfEq Hx Hy ⋯, map_le_map_iff' := ⋯ }
-- Mathlib.Topology.Order.OrderClosed
/-- **Alias** of `nhds_inf_atTop`. -/
inf_nhds_atTop : ∀ {α : Type u} [inst : Preorder α] [NoTopOrder α] [inst_2 : TopologicalSpace α] [ClosedIciTopology α] (a : α),
  nhds a ⊓ Filter.atTop = ⊥
-- Mathlib.Algebra.Homology.HomotopyCategory.Shift
CochainComplex.shiftFunctor_obj_X' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) (n p : ℤ), ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X p = K.X (p + n)
-- Mathlib.Algebra.Polynomial.Module.Basic
PolynomialModule.coeff_sum : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (s : Finset ι) (f : ι → PolynomialModule R M), (∑ i ∈ s, f i).coeff = ∑ i ∈ s, (f i).coeff
-- Mathlib.FieldTheory.Perfect
coe_frobeniusEquiv_symm_comp_coe_frobenius : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [inst_2 : PerfectRing R p],
  ⇑(frobeniusEquiv R p).symm ∘ ⇑(frobenius R p) = id
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.mapM.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (a : α) (as : List α) (bs : List β)
  (h_1 : (bs : List β) → motive [] bs) (h_2 : (a : α) → (as : List α) → (bs : List β) → motive (a :: as) bs),
  (match a :: as, bs with
    | [], bs => h_1 bs
    | a :: as, bs => h_2 a as bs) =
    h_2 a as bs
-- Mathlib.RingTheory.Norm.Defs
Algebra.norm_self : ∀ (R : Type u_1) [inst : CommRing R], Algebra.norm R = MonoidHom.id R
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.isIso_locallyRingedSpaceAdjunction_counit : CategoryTheory.IsIso AlgebraicGeometry.ΓSpec.locallyRingedSpaceAdjunction.counit
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.singleton_smul_singleton : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {a : α} {b : β}, {a} • {b} = {a • b}
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.neg.inj : ∀ {a a_1 : Lean.Grind.CommRing.Expr}, a.neg = a_1.neg → a = a_1
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the functor on the right component  -/
CategoryTheory.Limits.CatCospanTransform.right : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A' : Type u₄} →
                  {B' : Type u₅} →
                    {C' : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                CategoryTheory.Limits.CatCospanTransform F G F' G' → CategoryTheory.Functor C C'
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- If every finite set of linearly independent vectors has cardinality at most `n`,
then the same is true for arbitrary sets of linearly independent vectors.
 -/
linearIndependent_bounded_of_finset_linearIndependent_bounded : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {n : ℕ},
  (∀ (s : Finset M), (LinearIndependent R fun i => ↑i) → s.card ≤ n) →
    ∀ (s : Set M), LinearIndependent R Subtype.val → Cardinal.mk ↑s ≤ ↑n
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.map_comp_mk : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : CommRing k] [inst_1 : Monoid G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  {ρ : Representation k G V} {τ : Representation k G W} (f : ρ.IntertwiningMap τ),
  Representation.Coinvariants.map ρ τ f ∘ₗ Representation.Coinvariants.mk ρ = Representation.Coinvariants.mk τ ∘ₗ ↑f
-- Mathlib.Data.NNReal.Defs
/-- An `Algebra` over `ℝ` restricts to an `Algebra` over `ℝ≥0`.  -/
NNReal.instAlgebraOfReal : {A : Type u_1} → [inst : Semiring A] → [Algebra ℝ A] → Algebra NNReal A
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.singleHom_apply : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M] (a : R × Multiplicative M),
  AddMonoidAlgebra.singleHom a = AddMonoidAlgebra.single (Multiplicative.toAdd a.2) a.1
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- The first morphism of the factorisation.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.ι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [inst_2 : CategoryTheory.EnoughInjectives C] →
            (n : ℤ) → K ⟶ CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.mid✝ f n