mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Diffeology.Basic
DiffeologicalSpace.CorePlotsOn.mk.sizeOf_spec : ∀ {X : Type u_1} [inst : SizeOf X]
  (isPlotOn : {n : ℕ} → {u : Set (EuclideanSpace ℝ (Fin n))} → IsOpen u → (EuclideanSpace ℝ (Fin n) → X) → Prop)
  (isPlotOn_congr :
    ∀ {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p q : EuclideanSpace ℝ (Fin n) → X},
      Set.EqOn p q u → (isPlotOn hu p ↔ isPlotOn hu q))
  (isPlot : {n : ℕ} → (EuclideanSpace ℝ (Fin n) → X) → Prop)
  (isPlotOn_univ :
    autoParam (∀ {n : ℕ} {p : EuclideanSpace ℝ (Fin n) → X}, isPlotOn ⋯ p ↔ isPlot p)
      DiffeologicalSpace.CorePlotsOn.isPlotOn_univ._autoParam)
  (isPlot_const : ∀ {n : ℕ} (x : X), isPlot fun x_1 => x)
  (isPlotOn_reparam :
    ∀ {n m : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} {v : Set (EuclideanSpace ℝ (Fin m))} {hu : IsOpen u}
      (hv : IsOpen v) {p : EuclideanSpace ℝ (Fin n) → X} {f : EuclideanSpace ℝ (Fin m) → EuclideanSpace ℝ (Fin n)},
      Set.MapsTo f v u → isPlotOn hu p → ContDiffOn ℝ (↑⊤) f v → isPlotOn hv (p ∘ f))
  (locality :
    ∀ {n : ℕ} {u : Set (EuclideanSpace ℝ (Fin n))} (hu : IsOpen u) {p : EuclideanSpace ℝ (Fin n) → X},
      (∀ x ∈ u, ∃ v, ∃ (hv : IsOpen v), x ∈ v ∧ isPlotOn hv p) → isPlotOn hu p)
  (dTopology : TopologicalSpace X)
  (isOpen_iff_preimages_plots :
    autoParam
      (∀ {u : Set X},
        TopologicalSpace.IsOpen u ↔ ∀ {n : ℕ} (p : EuclideanSpace ℝ (Fin n) → X), isPlot p → IsOpen (p ⁻¹' u))
      DiffeologicalSpace.CorePlotsOn.isOpen_iff_preimages_plots._autoParam),
  sizeOf
      { isPlotOn := isPlotOn, isPlotOn_congr := isPlotOn_congr, isPlot := isPlot, isPlotOn_univ := isPlotOn_univ,
        isPlot_const := isPlot_const, isPlotOn_reparam := isPlotOn_reparam, locality := locality,
        dTopology := dTopology, isOpen_iff_preimages_plots := isOpen_iff_preimages_plots } =
    1 + sizeOf dTopology
-- Lean.Meta.PProdN
/-- Reduces `⟨x,y⟩.1` or `⟨x,y⟩.fst` redexes for `PProd` and `And`
 -/
Lean.Meta.PProdN.reduceProjs : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.Group.Basic
nsmul_iterate : ∀ {M : Type u_4} [inst : AddMonoid M] (k n : ℕ), (fun x => k • x)^[n] = fun x => k ^ n • x
-- Mathlib.CategoryTheory.Shift.ShiftSequence
CategoryTheory.Functor.shiftMap_comp : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A) {M : Type u_4} [inst_2 : AddMonoid M]
  [inst_3 : CategoryTheory.HasShift C M] [inst_4 : F.ShiftSequence M] {X Y Z : C} {n : M}
  (f : X ⟶ (CategoryTheory.shiftFunctor C n).obj Y) (g : Y ⟶ Z) (a a' : M) (ha' : n + a = a'),
  F.shiftMap (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctor C n).map g)) a a' ha' =
    CategoryTheory.CategoryStruct.comp (F.shiftMap f a a' ha') ((F.shift a').map g)
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedFunctor.hom_ext : ∀ {V : Type v} [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] {D : Type u₂} [inst_3 : CategoryTheory.EnrichedCategory V D]
  {F G : CategoryTheory.EnrichedFunctor V C D} {α β : F ⟶ G}, (∀ (X : C), α.out.app X = β.out.app X) → α = β
-- Mathlib.Data.Analysis.Topology
LocallyFinite.Realizer.mk.inj : ∀ {α : Type u_1} {β : Type u_2} {inst : TopologicalSpace α} {F : Ctop.Realizer α} {f : β → Set α}
  {bas : (a : α) → { s // a ∈ F.F.f s }} {sets : (x : α) → Fintype ↑{i | (f i ∩ F.F.f ↑(bas x)).Nonempty}}
  {bas_1 : (a : α) → { s // a ∈ F.F.f s }} {sets_1 : (x : α) → Fintype ↑{i | (f i ∩ F.F.f ↑(bas_1 x)).Nonempty}},
  { bas := bas, sets := sets } = { bas := bas_1, sets := sets_1 } → bas = bas_1 ∧ sets ≍ sets_1
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.ofFun_toFun : ∀ {α : Type u_1} {β : Type u_2} (f : UniformFun α β), UniformFun.ofFun (UniformFun.toFun f) = f
-- Mathlib.Topology.Metrizable.Uniformity
/-- A `MetricSpace` instance compatible with a given `UniformSpace` structure.  -/
UniformSpace.metricSpace : (X : Type u_2) → [inst : UniformSpace X] → [(uniformity X).IsCountablyGenerated] → [T0Space X] → MetricSpace X
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State.mk.sizeOf_spec : ∀ (mvarId : Lean.MVarId) (xs eqs eqsNew : List Lean.FVarId),
  sizeOf { mvarId := mvarId, xs := xs, eqs := eqs, eqsNew := eqsNew } =
    1 + sizeOf mvarId + sizeOf xs + sizeOf eqs + sizeOf eqsNew
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.mulOp_symm_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β] (f : αᵐᵒᵖ ≃+ βᵐᵒᵖ),
  AddEquiv.mulOp.symm f = MulOpposite.opAddEquiv.trans (f.trans MulOpposite.opAddEquiv.symm)
-- Mathlib.RingTheory.OreLocalization.Ring
OreLocalization.left_distrib : ∀ {R : Type u_1} [inst : Semiring R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S]
  (x y z : OreLocalization S R), x * (y + z) = x * y + x * z
-- Init.Data.AC
Lean.Data.AC.eval.eq_2 : ∀ {α : Sort u_1} (β : Sort u) [inst : Lean.Data.AC.EvalInformation α β] (ctx : α) (l r : Lean.Data.AC.Expr),
  Lean.Data.AC.eval β ctx (l.op r) =
    Lean.Data.AC.EvalInformation.evalOp ctx (Lean.Data.AC.eval β ctx l) (Lean.Data.AC.eval β ctx r)
-- Mathlib.Data.Nat.Choose.Basic
Nat.multichoose_zero_succ : ∀ (k : ℕ), Nat.multichoose 0 (k + 1) = 0
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.IsCyclicallyReduced.nil : ∀ {α : Type u}, FreeGroup.IsCyclicallyReduced []
-- Mathlib.Data.Fintype.EquivFin
Finite.of_subsingleton : ∀ {α : Sort u_4} [Subsingleton α], Finite α
-- Mathlib.AlgebraicGeometry.Modules.Tilde
AlgebraicGeometry.tilde.instModuleCarrierCarrierStalkAbPresheaf : {R : CommRingCat} →
  (M : ModuleCat ↑R) →
    (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑R)) → Module ↑R ↑((AlgebraicGeometry.tilde M).presheaf.stalk x)
-- Init.Data.BitVec.Basic
BitVec.instMod : {n : ℕ} → Mod (BitVec n)
-- Lean.Elab.MutualInductive
/-- The elaborated header with the `indFVar` registered for this inductive type.  -/
Lean.Elab.Command.ElabHeaderResult : Type
-- Lean.Elab.MutualInductive
/-- Function to collect additional fvars that might be missed by the constructors.
It is permissible to include fvars that do not exist in the local context (`structure` for example includes its field fvars).  -/
Lean.Elab.Command.InductiveElabStep2.collectUsedFVars : Lean.Elab.Command.InductiveElabStep2 → StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_sub_closedBall_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), {x} - Metric.closedBall 0 δ = Metric.closedBall x δ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.isSupportedType : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Init.Data.UInt.Bitwise
UInt64.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : UInt64}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.Algebra.Homology.Embedding.Connect
/-- If `h : ConnectData K L`, then `h.cochainComplex` identifies to `K` in degrees `≤ -1`.  -/
CochainComplex.ConnectData.restrictionLEIso : {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) →
            HomologicalComplex.restriction h.cochainComplex (ComplexShape.embeddingUpIntLE (-1)) ≅ K
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Functions.apply₂.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (f : L.Functions 2) (t₁ t₂ : L.Term α),
  f.apply₂ t₁ t₂ = FirstOrder.Language.func f ![t₁, t₂]
-- Init.Data.List.Monadic
List.zipWithM.match_1.congr_eq_1 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (motive : List α → List β → Array γ → Sort u_4) (x : List α)
  (x_1 : List β) (x_2 : Array γ)
  (h_1 : (a : α) → (as : List α) → (b : β) → (bs : List β) → (acc : Array γ) → motive (a :: as) (b :: bs) acc)
  (h_2 : (x : List α) → (x_3 : List β) → (acc : Array γ) → motive x x_3 acc) (a : α) (as : List α) (b : β) (bs : List β)
  (acc : Array γ),
  x = a :: as →
    x_1 = b :: bs →
      x_2 = acc →
        (match x, x_1, x_2 with
          | a :: as, b :: bs, acc => h_1 a as b bs acc
          | x, x_3, acc => h_2 x x_3 acc) ≍
          h_1 a as b bs acc
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_val_Ioi : ∀ {n : ℕ} (a : Fin n), Finset.image Fin.val (Finset.Ioi a) = Finset.Ioo (↑a) n
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability in the right endpoint.

If `f : ℝ → E` is integrable on `a..b` and `f` is continuous at `b`, then `u ↦ ∫ x in a..u, f x` has
derivative `f b` at `b` in the sense of strict differentiability.  -/
intervalIntegral.integral_hasStrictDerivAt_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
      ContinuousAt f b → HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) (f b) b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get!_union_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : Inhabited α] [inst_1 : EquivBEq α]
  [inst_2 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Init.Data.List.Impl
/-- Auxiliary for `eraseIdxTR`: `eraseIdxTR.go l n xs acc = acc.toList ++ eraseIdx xs a`,
unless `a` is not present in which case it returns `l`  -/
_private.Init.Data.List.Impl.0.List.eraseIdxTR.go : {α : Type u_1} → List α → List α → ℕ → Array α → List α
-- Mathlib.Data.List.Chain
List.isChain_map_of_isChain : ∀ {α : Type u_1} {β : Type u_2} {R : α → α → Prop} {S : β → β → Prop} (f : α → β),
  (∀ (a b : α), R a b → S (f a) (f b)) → ∀ {l : List α}, List.IsChain R l → List.IsChain S (List.map f l)
-- Init.Data.BitVec.Lemmas
BitVec.getElem_extractLsb' : ∀ {n start len : ℕ} {x : BitVec n} {i : ℕ} (h : i < len), (BitVec.extractLsb' start len x)[i] = x.getLsbD (start + i)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd'_hom_app_hom₃ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (a b n : ℤ)
  (h : a + b = n) (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorAdd' C a b n h).hom.app X).hom₃ =
    (CategoryTheory.shiftFunctorAdd' C a b n h).hom.app X.obj₃
-- Lean.Meta.Tactic.Simp.Attr
Lean.Meta.mkSimpAttr : Lean.Name → String → Lean.Meta.SimpExtension → autoParam Lean.Name Lean.Meta.mkSimpAttr._auto_1 → IO Unit
-- Mathlib.Algebra.Polynomial.Lifts
/-- A monic polynomial lifts if and only if it can be lifted to a monic polynomial
of the same degree.  -/
Polynomial.lifts_and_degree_eq_and_monic : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} [Nontrivial S] {p : Polynomial S},
  p ∈ Polynomial.lifts f → p.Monic → ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree ∧ q.Monic
-- Mathlib.Data.Matrix.Basis
Matrix.single_add : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : AddZeroClass α]
  (i : m) (j : n) (a b : α), Matrix.single i j (a + b) = Matrix.single i j a + Matrix.single i j b
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.queryNum : LeanSearchClient.SearchServer → Lean.CoreM ℕ
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.fac_pull : ∀ {Δ : SimplexCategoryᵒᵖ} (A : CategoryTheory.SimplicialObject.Splitting.IndexSet Δ) {Δ' : SimplexCategoryᵒᵖ}
  (θ : Δ ⟶ Δ'),
  CategoryTheory.CategoryStruct.comp (A.pull θ).e
      (CategoryTheory.Limits.image.ι (CategoryTheory.CategoryStruct.comp θ.unop A.e)) =
    CategoryTheory.CategoryStruct.comp θ.unop A.e
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (G : CategoryTheory.Functor C D) [inst_4 : G.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) G],
  CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit G f =
    CategoryTheory.Limits.isColimitOfHasCokernelOfPreservesColimit G f
-- Mathlib.Combinatorics.SimpleGraph.Walk.Traversal
/-- Use `firstDart_eq_head_darts` to rewrite in the reverse direction.  -/
SimpleGraph.Walk.head_darts_eq_firstDart : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} {p : G.Walk v w} (hnil : p.darts ≠ []), p.darts.head hnil = p.firstDart ⋯
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatTrans.naturality_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) {X Y : C} (e : X ≅ Y),
  CategoryTheory.CategoryStruct.comp (F.map e.inv) (CategoryTheory.CategoryStruct.comp (α.app X) (G.map e.hom)) =
    α.app Y
-- Mathlib.Analysis.Convex.Between
wbtw_smul_vadd_smul_vadd_of_nonpos_of_le : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x : P) (v : V) {r₁ r₂ : R},
  r₁ ≤ 0 → r₂ ≤ r₁ → Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)
-- Lean.Data.PrefixTree
Lean.PrefixTreeNode.Node.inj : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {a : Option β}
  {a_1 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp} {a_2 : Option β}
  {a_3 : Std.TreeMap.Raw α (Lean.PrefixTreeNode α β cmp) cmp},
  Lean.PrefixTreeNode.Node a a_1 = Lean.PrefixTreeNode.Node a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- The sigma type associated to a family of compactly generated spaces is compactly generated.  -/
instCompactlyGeneratedSpaceSigma : ∀ {ι : Type u} {X : ι → Type v} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), CompactlyGeneratedSpace (X i)],
  CompactlyGeneratedSpace ((i : ι) × X i)
-- Mathlib.FieldTheory.IsPerfectClosure
/-- Given a natural number `p`, the `p`-nilradical of a ring is defined to be the
nilradical if `p > 1` (`pNilradical_eq_nilradical`), and defined to be the zero ideal if `p ≤ 1`
(`pNilradical_eq_bot'`). Equivalently, it is the ideal consisting of elements `x` such that
`x ^ p ^ n = 0` for some `n` (`mem_pNilradical`).  -/
pNilradical : (R : Type u_1) → [inst : CommSemiring R] → ℕ → Ideal R
-- Mathlib.Control.ULiftable
Option.instULiftable : ULiftable Option Option
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
_private.Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv.0.GenContFract.squashGCF.match_3.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comp_f₀ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex.SnakeInput C} (f : S₁.Hom S₂) (g : S₂.Hom S₃),
  (f.comp g).f₀ = CategoryTheory.CategoryStruct.comp f.f₀ g.f₀
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.Context.mk : Lean.Meta.TransparencyMode → (Lean.Expr → Lean.MetaM Lean.Meta.Simp.Result) → Mathlib.Tactic.AtomM.Context
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_blsub_le_lift : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}), (o.blsub f).cof ≤ Cardinal.lift.{v, u} o.card
-- Mathlib.Order.Hom.Bounded
BotHom.symm_dual_id : ∀ {α : Type u_2} [inst : LE α] [inst_1 : OrderBot α], BotHom.dual.symm (TopHom.id αᵒᵈ) = BotHom.id α
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.postcomp₂_naturality_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) {a_1 b_1 : Bᵒᵖ} (g : a_1 ⟶ b_1)
  (X : ↑(CategoryTheory.Cat.of (Opposite.unop a_1 ⟶ a))),
  ((CategoryTheory.Bicategory.postcomp₂ f).naturality g).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator g.unop X f).inv
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqAuthority : BEq Std.Http.URI.Authority
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.hom_ext : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D),
  (∀ (i : ι), f.f i = g.f i) → f = g
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
/-- The 1-cycles of the complex of inhomogeneous chains of `A` are isomorphic to
`cycles₁ A`, which is a simpler type.  -/
groupHomology.isoCycles₁ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → groupHomology.cycles A 1 ≅ ModuleCat.of k ↥(groupHomology.cycles₁ A)
-- Mathlib.Algebra.Homology.HasNoLoop
ComplexShape.not_rel_of_eq : ∀ {ι : Type u_1} (c : ComplexShape ι) [c.HasNoLoop] {j j' : ι}, j = j' → ¬c.Rel j j'
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.Quotient.mkₐ_toRingHom : ∀ (R₁ : Type u_1) {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] (I : Ideal A)
  [inst_3 : I.IsTwoSided], (Ideal.Quotient.mkₐ R₁ I).toRingHom = Ideal.Quotient.mk I
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json.mk.sizeOf_spec : ∀ (name : Lean.Name) (builder : Aesop.BuilderName) (phase : Aesop.PhaseName) (scope : Aesop.ScopeName)
  (rendered : String),
  sizeOf { name := name, builder := builder, phase := phase, scope := scope, rendered := rendered } =
    1 + sizeOf name + sizeOf builder + sizeOf phase + sizeOf scope + sizeOf rendered
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_id_comp_hom_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ : B} (f : b₀ ⟶ b₁)
  {Z : F.obj b₀ ⟶ F.obj b₁}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id b₀)) (F.map f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.mapComp' (CategoryTheory.CategoryStruct.id b₀) f f ⋯).hom h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (F.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId b₀).inv (F.map f)) h)
-- Lean.Meta.Tactic.Grind.Internalize
/-- Returns true if `e` is a nonparametric literal.
For example, `BitVec` and `Fin` are parametric literals, but `Nat` is not.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.isNonParametricLitValue : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Order.WithBot
WithTop.untopD_le : ∀ {α : Type u_1} [inst : PartialOrder α] {y : WithTop α} {a b : α}, y ≤ ↑b → WithTop.untopD a y ≤ b
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.liftNC_single : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {R : Type u_5} [inst_1 : NonUnitalNonAssocSemiring R]
  (f : k →+ R) (g : G → R) (a : G) (b : k), (SkewMonoidAlgebra.liftNC f g) (SkewMonoidAlgebra.single a b) = f b * g a
-- Mathlib.Analysis.InnerProductSpace.JointEigenspace
/-- If A and B are commuting symmetric operators on a finite-dimensional inner product space
then the eigenspaces of the restriction of B to any eigenspace of A exhaust that eigenspace.  -/
LinearMap.IsSymmetric.iSup_eigenspace_inf_eigenspace_of_commute : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {α : 𝕜} {A B : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E],
  B.IsSymmetric → Commute A B → ⨆ γ, Module.End.eigenspace A α ⊓ Module.End.eigenspace B γ = Module.End.eigenspace A α
-- Mathlib.Topology.Homotopy.Basic
/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections.  -/
ContinuousMap.HomotopyWith.Simps.apply : {X : Type u} →
  {Y : Type v} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        {f₀ f₁ : C(X, Y)} → {P : C(X, Y) → Prop} → f₀.HomotopyWith f₁ P → ↑unitInterval × X → Y
-- Std.Data.ExtTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the largest key that is
less than or equal to the given key.
 -/
Std.ExtTreeMap.getKeyLE : {α : Type u} →
  {β : Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.add_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f g : A ⟶ B),
  Rep.Hom.hom (f + g) = Rep.Hom.hom f + Rep.Hom.hom g
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.inv.instIsMulRightInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : DivisionMonoid G] [MeasurableMul G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant], μ.inv.IsMulRightInvariant
-- Mathlib.RingTheory.PowerSeries.Binomial
PowerSeries.binomialSeries_coeff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : BinomialRing R] [inst_2 : Semiring A] [inst_3 : SMul R A]
  (r : R) (n : ℕ), (PowerSeries.coeff n) (PowerSeries.binomialSeries A r) = Ring.choose r n • 1
-- Lean.Parser.Term
/-- Representation of an expression with metadata used during pretty printing for the `pp.mdata` option.
 -/
Lean.Parser.Term.mdataDiagnostic : Lean.Parser.Parser
-- Init.Tactics
/-- `all_goals tac` runs `tac` on each goal, concatenating the resulting goals.
If the tactic fails on any goal, the entire `all_goals` tactic fails.

See also `any_goals tac`.
 -/
Lean.Parser.Tactic.allGoals : Lean.ParserDescr
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.stronglyMeasurable_condExp : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E], MeasureTheory.StronglyMeasurable μ[f | m]
-- Mathlib.Topology.OmegaCompletePartialOrder
isωSup_ωSup : ∀ {α : Type u_1} [inst : OmegaCompletePartialOrder α] (c : OmegaCompletePartialOrder.Chain α),
  Scott.IsωSup c (OmegaCompletePartialOrder.ωSup c)
-- Mathlib.Algebra.Category.Grp.Basic
/-- Typecheck an `AddMonoidHom` as a morphism in `AddCommGrpCat`.  -/
AddCommGrpCat.ofHom : {X Y : Type u} →
  [inst : AddCommGroup X] → [inst_1 : AddCommGroup Y] → (X →+ Y) → (AddCommGrpCat.of X ⟶ AddCommGrpCat.of Y)
-- Mathlib.CategoryTheory.SingleObj
CategoryTheory.SingleObj.differenceFunctor_obj : ∀ {G : Type u} [inst : Group G] {C : Type v} [inst_1 : CategoryTheory.Category.{w, v} C] (f : C → G) (x : C),
  (CategoryTheory.SingleObj.differenceFunctor f).obj x = ()
-- Mathlib.CategoryTheory.ConcreteCategory.Bundled
/-- `Bundled` is a type bundled with a type class instance for that type. Only
the type class is exposed as a parameter.  -/
CategoryTheory.Bundled : (Type u → Type v) → Type (max (u + 1) v)
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.lt_next_iff_le : ∀ {s : String.Slice} {p q : s.Pos} {h : q ≠ s.endPos}, p < q.next h ↔ p ≤ q
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.Context.mk.inj : ∀ {cat : Lean.Name} {forceParens : Bool} {cat_1 : Lean.Name} {forceParens_1 : Bool},
  { cat := cat, forceParens := forceParens } = { cat := cat_1, forceParens := forceParens_1 } →
    cat = cat_1 ∧ forceParens = forceParens_1