mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Ring.Equiv
/-- The two paths coercion can take to an `Equiv` are equivalent  -/
RingEquiv.toEquiv_commutes : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (f : R ≃+* S),
  (↑f).toEquiv = (↑f).toEquiv
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.Full.mapCommMon : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F : CategoryTheory.Functor C D} [inst_6 : F.Braided] [F.Full] [F.Faithful], F.mapCommMon.Full
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.instPartialOrder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : NonAssocSemiring α] →
      [inst_1 : Preorder α] → [inst_2 : NonAssocSemiring β] → [inst_3 : PartialOrder β] → PartialOrder (α →+*o β)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited β]
  {k a : α}, (t.erase k)[a]! = if cmp k a = Ordering.eq then default else t[a]!
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasUnifEigenvalue.mem_spectrum : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R}, f.HasUnifEigenvalue μ 1 → μ ∈ spectrum R f
-- Mathlib.SetTheory.Cardinal.Regular
/-- A regular cardinal is infinite.  -/
Cardinal.IsRegular.aleph0_le : ∀ {c : Cardinal.{u_1}}, c.IsRegular → Cardinal.aleph0 ≤ c
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
FundamentalGroupoid.punitEquivDiscretePUnit_counitIso : FundamentalGroupoid.punitEquivDiscretePUnit.counitIso =
  CategoryTheory.Iso.refl
    (((CategoryTheory.Functor.const (CategoryTheory.Discrete PUnit.{v + 1})).obj { as := PUnit.unit }).comp
      (CategoryTheory.Functor.star (FundamentalGroupoid PUnit.{u + 1})))
-- Mathlib.FieldTheory.Perfect
bijective_frobenius : ∀ (R : Type u_1) (p : ℕ) [inst : CommSemiring R] [inst_1 : ExpChar R p] [PerfectRing R p],
  Function.Bijective ⇑(frobenius R p)
-- Mathlib.Tactic.AdaptationNote
/-- `#adaptation_note /-- comment -/` adds an adaptation note to the current file.
Adaptation notes are comments that are used to indicate that a piece of code
has been changed to accommodate a change in Lean core.
They typically require further action/maintenance to be taken in the future.

This syntax works as a command, or inline in tactic or term mode.
 -/
adaptationNoteTermStx : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Sheafification
CategoryTheory.sheafificationAdjunction_unit_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] [inst_2 : CategoryTheory.HasWeakSheafify J D]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  (CategoryTheory.sheafificationAdjunction J D).unit.app P = CategoryTheory.toSheafify J P
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rio.isEmpty.eq_1 : ∀ {α : Type u} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.Least? α] (r : Std.Rio α),
  r.isEmpty = decide (∀ (a : α), Std.PRange.least? = some a → ¬a < r.upper)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.spectrum_algebraMap_subset : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : TopologicalSpace A] [inst_6 : Ring A]
  [inst_7 : StarRing A] [inst_8 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] (r : R),
  spectrum R ((algebraMap R A) r) ⊆ {r}
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanFinrank_eq_iInf : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p : Submodule R M),
  p.spanFinrank = ⨅ s, (↑s).card
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.nfpFamily_lt_ord_of_isRegular : ∀ {ι : Type u} {f : ι → Ordinal.{u} → Ordinal.{u}} {c : Cardinal.{u}},
  c.IsRegular →
    Cardinal.mk ι < c →
      c ≠ Cardinal.aleph0 →
        ∀ {a : Ordinal.{u}}, (∀ (i : ι), ∀ b < c.ord, f i b < c.ord) → a < c.ord → Ordinal.nfpFamily f a < c.ord
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_natAddEmb_uIcc : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.map (Fin.natAddEmb m) (Finset.uIcc i j) = Finset.uIcc (Fin.natAdd m i) (Fin.natAdd m j)
-- Mathlib.Data.List.Sublists
List.sublistsLenAux_append : ∀ {α : Type u} {β : Type v} {γ : Type w} (n : ℕ) (l : List α) (f : List α → β) (g : β → γ) (r : List β) (s : List γ),
  List.sublistsLenAux n l (g ∘ f) (List.map g r ++ s) = List.map g (List.sublistsLenAux n l f r) ++ s
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.instFunLike.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] (φ : M →* N) (A : Type u_4) [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] (B : Type u_5) [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B],
  MulDistribMulActionHom.instFunLike φ A B = { coe := fun m => m.toFun, coe_injective := ⋯ }
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.single_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {a : α}, (RBTree.RBSet.single a).toList = [a]
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
MeasureTheory.ProbabilityMeasure.map_apply_of_aemeasurable : ∀ {Ω : Type u_1} {Ω' : Type u_2} [inst : MeasurableSpace Ω] [inst_1 : MeasurableSpace Ω']
  (ν : MeasureTheory.ProbabilityMeasure Ω) {f : Ω → Ω'} (f_aemble : AEMeasurable f ↑ν) {A : Set Ω'},
  MeasurableSet A → (ν.map f_aemble) A = ν (f ⁻¹' A)
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_mem_range_opow : ∀ (o a : Ordinal.{u_1}), Ordinal.veblen o a ∈ Set.range fun x => Ordinal.omega0 ^ x
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- `{a} ≃ Unit` as measurable spaces.  -/
MeasurableEquiv.Set.singleton : {α : Type u_1} → [inst : MeasurableSpace α] → (a : α) → ↑{a} ≃ᵐ Unit
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.idealSetMap.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (a : NumberField.mixedEmbedding.mixedSpace K)
  (ha : a ∈ NumberField.mixedEmbedding.fundamentalCone.idealSet K J),
  NumberField.mixedEmbedding.fundamentalCone.idealSetMap K J ⟨a, ha⟩ = ⟨a, ⋯⟩
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_sub_const_Ioi : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x - a) '' Set.Ioi b = Set.Ioi (b - a)
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- If `f` is locally integrable, and `f =O[cocompact] g` for some `g` integrable at `cocompact`,
then `f` is integrable.  -/
MeasureTheory.LocallyIntegrable.integrable_of_isBigO_cocompact : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F}
  [inst_1 : TopologicalSpace α] [SecondCountableTopology α] [inst_3 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_4 : NormedAddCommGroup F] [(Filter.cocompact α).IsMeasurablyGenerated],
  MeasureTheory.LocallyIntegrable f μ →
    f =O[Filter.cocompact α] g →
      MeasureTheory.IntegrableAtFilter g (Filter.cocompact α) μ → MeasureTheory.Integrable f μ
-- Mathlib.Order.WellFounded
WellFounded.wellFounded_iff_has_min : ∀ {α : Type u_1} {r : α → α → Prop}, WellFounded r ↔ ∀ (s : Set α), s.Nonempty → ∃ m ∈ s, ∀ x ∈ s, ¬r x m
-- Mathlib.LinearAlgebra.TensorPower.Basic
PiTensorProduct.isEmptyEquiv.congr_simp : ∀ (ι : Type u_1) {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] [inst_3 : IsEmpty ι],
  PiTensorProduct.isEmptyEquiv ι = PiTensorProduct.isEmptyEquiv ι
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
/-- Schwartz functions are in `L^p` for any `p`.  -/
SchwartzMap.memLp : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E] [SecondCountableTopologyEither E F]
  (f : SchwartzMap E F) (p : ENNReal) (μ : autoParam (MeasureTheory.Measure E) SchwartzMap.memLp._auto_1)
  [hμ : μ.HasTemperateGrowth], MeasureTheory.MemLp (⇑f) p μ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm.injEq : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) (e : Lean.Meta.Grind.Arith.CommRing.RingExpr)
  (p : Lean.Grind.CommRing.Poly) (c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr)
  (e_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr) (p_1 : Lean.Grind.CommRing.Poly),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm c e p =
      Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.commRingNorm c_1 e_1 p_1) =
    (c = c_1 ∧ e = e_1 ∧ p = p_1)
-- Mathlib.Algebra.Category.ModuleCat.Ulift
ModuleCat.uliftFunctorForgetIso_inv_app_hom_apply : ∀ (R : Type u) [inst : Ring R] (X : ModuleCat R)
  (a : ((ModuleCat.uliftFunctor.{v', u_1, u} R).comp (CategoryTheory.forget (ModuleCat R))).obj X),
  (CategoryTheory.ConcreteCategory.hom ((ModuleCat.uliftFunctorForgetIso R).inv.app X)) a = a
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Coalgebra.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C C} [inst_1 : SizeOf C] (V : C)
  (str : V ⟶ F.obj V), sizeOf { V := V, str := str } = 1 + sizeOf V + sizeOf str
-- Batteries.Data.List.Basic
/-- Tail-recursive version of `inits`.  -/
List.initsTR : {α : Type u_1} → List α → List (List α)
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` creates small limits if it creates limits of shape `J` for any small `J`.  -/
CategoryTheory.CreatesLimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        CategoryTheory.Functor C D → Type (max (max (max (max u₁ u₂) v₁) v₂) (v₂ + 1))
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Iso.sumBoxProdDistrib_apply : ∀ {V₁ : Type u_5} {V₂ : Type u_6} {W : Type u_7} (G₁ : SimpleGraph V₁) (G₂ : SimpleGraph V₂) (H : SimpleGraph W)
  (p : (V₁ ⊕ V₂) × W),
  (SimpleGraph.Iso.sumBoxProdDistrib G₁ G₂ H) p = Sum.map (fun x => (x, p.2)) (fun x => (x, p.2)) p.1
-- Mathlib.Analysis.Convex.Segment
segment_subset_iff : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {s : Set E} {x y : E},
  segment 𝕜 x y ⊆ s ↔ ∀ (a b : 𝕜), 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s
-- Mathlib.GroupTheory.OrderOfElement
/-- If `n * x = 0`, but `n/p * x ≠ 0` for
all prime factors `p` of `n`, then `x` has order `n` in `G`.  -/
addOrderOf_eq_of_nsmul_and_div_prime_nsmul : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} {n : ℕ},
  0 < n → n • x = 0 → (∀ (p : ℕ), Nat.Prime p → p ∣ n → (n / p) • x ≠ 0) → addOrderOf x = n
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.PlacedTile.ext : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  {ps : DiscreteTiling.Protoset G X ιₚ} {x y : DiscreteTiling.PlacedTile ps},
  x.index = y.index → x.groupElts ≍ y.groupElts → x = y
-- Init.Data.Order.Ord
Std.LawfulEqCmp.mk : ∀ {α : Type u} {cmp : α → α → Ordering} [toReflCmp : Std.ReflCmp cmp],
  (∀ {a b : α}, cmp a b = Ordering.eq → a = b) → Std.LawfulEqCmp cmp
-- Batteries.Data.Float.Lemmas
Float.Model.UnpackedFloat.isNaNBits.eq_1 : ∀ {spec : Float.Model.Format} (b : BitVec spec.numBits),
  Float.Model.UnpackedFloat.isNaNBits b =
    decide
      (Float.Model.UnpackedFloat.unpackExponent b = -1#spec.exponentBits ∧
        Float.Model.UnpackedFloat.unpackMantissa b ≠ 0#spec.mantissaBitsWithoutImplicit)
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- An explicit limit cone for a functor `F : J ⥤ LightProfinite`, for a countable category `J`
defined in terms of `CompHaus.limitCone`, which is defined in terms of `TopCat.limitCone`.  -/
LightProfinite.limitCone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.CountableCategory J] → (F : CategoryTheory.Functor J LightProfinite) → CategoryTheory.Limits.Cone F
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleMatch.mk.inj : ∀ {name type : String} {doc? : Option String} {name_1 type_1 : String} {doc?_1 : Option String},
  { name := name, type := type, doc? := doc? } = { name := name_1, type := type_1, doc? := doc?_1 } →
    name = name_1 ∧ type = type_1 ∧ doc? = doc?_1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_eq_comap_nhds_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α], uniformity α = Filter.comap (fun p => dist p.1 p.2) (nhds 0)
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpTheorems.erase : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] →
        [Lean.MonadOptions m] → Lean.Meta.SimpTheorems → Lean.Meta.Origin → m Lean.Meta.SimpTheorems
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.rotateLeft.congr_simp : ∀ {s : String.Slice} {p p_1 : s.Pos} (e_p : p = p_1) {t₁ t₁_1 : String} (e_t₁ : t₁ = t₁_1) {t₂ t₂_1 : String}
  (e_t₂ : t₂ = t₂_1) {t₃ t₃_1 : String} (e_t₃ : t₃ = t₃_1) (h : p.Splits (t₁ ++ t₂) t₃), h.rotateLeft = ⋯.rotateLeft
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toAlgHom_op : ∀ {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] (f : A ≃ₐ[R] B), ↑(AlgEquiv.op f) = AlgHom.op ↑f
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.natTrans_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : CategoryTheory.Comma L R), (CategoryTheory.Comma.natTrans L R).app X = X.hom
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.mem_funs : ∀ {x y f : ZFSet.{u}}, f ∈ x.funs y ↔ x.IsFunc y f
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.instInhabitedStmt' : Inhabited Turing.PartrecToTM2.Stmt'
-- Mathlib.Algebra.Order.Sub.Basic
tsub_min : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b : α}, a - min a b = a - b
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- Bounded closed sets in `WeakDual 𝕜 E` are compact when `𝕜` is a proper space.  -/
WeakDual.isCompact_of_bounded_of_closed : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)}, Bornology.IsBounded s → IsClosed s → IsCompact s
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι_mapBifunctor₂₃Desc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} {K₁ : HomologicalComplex C₁ c₁} {K₂ : HomologicalComplex C₂ c₂} {K₃ : HomologicalComplex C₃ c₃}
  (c₁₂ : ComplexShape ι₁₂) {c₂₃ : ComplexShape ι₂₃} {c₄ : ComplexShape ι₄} [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄]
  [inst_23 : HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] {j : ι₄} {A : C₄}
  (f : (i₁ : ι₁) → (i₂ : ι₂) → ⋯) (i₁ : ι₁) (i₂ : ι₂), ⋯
-- Mathlib.LinearAlgebra.Vandermonde
Matrix.vandermonde.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (v : Fin n → R), Matrix.vandermonde v = Matrix.of fun i j => v i ^ ↑j
-- Lean.Compiler.IR.Format
Lean.IR.instToStringDecl : ToString Lean.IR.Decl
-- Init.Data.Vector.Attach
/-- This lemma identifies maps over arrays of subtypes, where the function only depends on the value, not the proposition,
and simplifies these to the function directly taking the value.
 -/
Vector.map_subtype : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {p : α → Prop} {xs : Vector { x // p x } n} {f : { x // p x } → β} {g : α → β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Vector.map f xs = Vector.map g xs.unattach
-- Mathlib.GroupTheory.Index
Subgroup.index_mul_card : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.index * Nat.card ↥H = Nat.card G
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
Filter.IsIncreasingApproximateUnit.eventually_isSelfAdjoint : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {l : Filter A},
  l.IsIncreasingApproximateUnit → ∀ᶠ (x : A) in l, IsSelfAdjoint x
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.instHasColimitsOfShapeOfHasCountableColimitsOfCountableCategory : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableColimits C]
  (J : Type u_3) [inst_2 : CategoryTheory.Category.{v, u_3} J] [CategoryTheory.CountableCategory J],
  CategoryTheory.Limits.HasColimitsOfShape J C
-- Mathlib.MeasureTheory.Integral.FinMeasAdditive
MeasureTheory.SimpleFunc.setToSimpleFunc_zero : ∀ {α : Type u_1} {F : Type u_3} {F' : Type u_4} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F]
  [inst_2 : NormedAddCommGroup F'] [inst_3 : NormedSpace ℝ F'] {m : MeasurableSpace α}
  (f : MeasureTheory.SimpleFunc α F), MeasureTheory.SimpleFunc.setToSimpleFunc 0 f = 0
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.mk : {R : Type u_3} →
  [inst : CommSemiring R] →
    {A : Type u_4} →
      [inst_1 : Semiring A] →
        [inst_2 : TopologicalSpace A] →
          {B : Type u_5} →
            [inst_3 : Semiring B] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : Algebra R A] →
                  [inst_6 : Algebra R B] →
                    (toAlgHom : A →ₐ[R] B) →
                      autoParam (Continuous (↑↑toAlgHom.toRingHom).toFun) ContinuousAlgHom.cont._autoParam → A →A[R] B
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- Product of two continuous homomorphisms on different spaces.  -/
ContinuousMonoidHom.prodMap : {A : Type u_2} →
  {B : Type u_3} →
    {C : Type u_4} →
      {D : Type u_5} →
        [inst : Monoid A] →
          [inst_1 : Monoid B] →
            [inst_2 : Monoid C] →
              [inst_3 : Monoid D] →
                [inst_4 : TopologicalSpace A] →
                  [inst_5 : TopologicalSpace B] →
                    [inst_6 : TopologicalSpace C] →
                      [inst_7 : TopologicalSpace D] → (A →ₜ* C) → (B →ₜ* D) → A × B →ₜ* C × D
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.chosenEnd.lift_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} {X : Type (max w u)}
  (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j))
  (x : X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.chosenEnd.lift f hf)) x =
    ⟨fun j => (CategoryTheory.ConcreteCategory.hom (f j)) x, ⋯⟩
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- The variation of a function on `Ici a` is the sum of the variation on `Ioi a` and the
contribution of `a`, i.e., the distance between the right limit and the value at `a`.
We give a version relative to a set `s`.  -/
eVariationOn.eVariationOn_on_inter_Ici_eq_Ioi_add_edist : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α} {a : α} {l : E},
  (nhdsWithin a (s ∩ Set.Ioi a)).NeBot →
    a ∈ s →
      Filter.Tendsto f (nhdsWithin a (s ∩ Set.Ioi a)) (nhds l) →
        eVariationOn f (s ∩ Set.Ici a) = eVariationOn f (s ∩ Set.Ioi a) + edist (f a) l
-- Mathlib.Data.Nat.ModEq
Nat.add_div_le_add_div : ∀ (a b c : ℕ), a / c + b / c ≤ (a + b) / c
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.inclusion.eq_1 : ∀ {G : Type u_1} [inst : Group G] {S : Type u_4} [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] [inst_3 : LE S]
  [inst_4 : IsConcreteLE S G] {H K : S} (h : H ≤ K), SubgroupClass.inclusion h = MonoidHom.mk' (fun x => ⟨↑x, ⋯⟩) ⋯
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.equivComma_functor_map_right_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Functor (CategoryTheory.WithInitial C) D} (η : X ⟶ Y) (X_1 : C),
  (CategoryTheory.WithInitial.equivComma.functor.map η).right.app X_1 = η.app (CategoryTheory.WithInitial.incl.obj X_1)
-- Mathlib.CategoryTheory.Sites.Point.Presheaf
CategoryTheory.GrothendieckTopology.instSmallPointBotPointsBotOfSmall : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [Small.{w, u} C],
  CategoryTheory.ObjectProperty.Small.{w, max u w, max (max u v) (w + 1)}
    (CategoryTheory.GrothendieckTopology.pointsBot C)
-- Mathlib.Data.Matrix.Basic
AddEquiv.mapMatrix_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : Add α] [inst_1 : Add β] (f : α ≃+ β)
  (M : Matrix m n α), f.mapMatrix M = M.map ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- Two maps from a wide coequalizer are equal if they are equal when composed with the wide
coequalizer map  -/
CategoryTheory.Limits.wideCoequalizer.hom_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] [Nonempty J] {W : C}
  {k l : CategoryTheory.Limits.wideCoequalizer f ⟶ W},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideCoequalizer.π f) l →
    k = l
-- Init.Data.List.Sort.Lemmas
_private.Init.Data.List.Sort.Lemmas.0.List.mergeSort.eq_3 : ∀ {α : Type u_1} (x : α → α → Bool) (a b : α) (xs : List α),
  (a :: b :: xs).mergeSort x =
    ((↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩).1).mergeSort x).merge
      ((↑(List.MergeSort.Internal.splitInTwo ⟨a :: b :: xs, ⋯⟩).2).mergeSort x) x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.equiv_of_beq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)],
  m₁.WF → m₂.WF → m₁.beq m₂ = true → m₁.Equiv m₂
-- Mathlib.Tactic.Linter.Multigoal
/-- The "multiGoal" linter emits a warning when there are multiple active goals.  -/
_private.Mathlib.Tactic.Linter.Multigoal.0.Mathlib.Linter.Style.multiGoal.multiGoalLinter : Lean.Linter
-- Mathlib.Data.FinEnum
FinEnum.fin : {n : ℕ} → FinEnum (Fin n)