mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.map_sub_right_ae : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : AddGroup G] [MeasurableAdd G] (μ : MeasureTheory.Measure G)
  [μ.IsAddRightInvariant] (x : G), Filter.map (fun t => t - x) (MeasureTheory.ae μ) = MeasureTheory.ae μ
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.isTopologicalGroup : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  [inst_1 : (i : ι) → TopologicalSpace (R i)] [hBopen : Fact (∀ (i : ι), IsOpen ↑(B i))]
  [inst_2 : (i : ι) → Group (R i)] [inst_3 : ∀ (i : ι), SubgroupClass (S i) (R i)]
  [∀ (i : ι), IsTopologicalGroup (R i)],
  IsTopologicalGroup (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) Filter.cofinite)
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.left_eq_or_eq : ∀ {α : Type u_1} {β : Type u_2} {x y z w : α} {e : β} {G : Graph α β}, G.IsLink e x y → G.IsLink e z w → x = z ∨ x = w
-- Mathlib.Data.ZMod.IntUnitsPower
mul_uzpow : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (s₁ s₂ : ℤˣ) (x : R),
  (s₁ * s₂) ^ x = s₁ ^ x * s₂ ^ x
-- Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
/-- Any standard Borel space embeds measurably into the reals.  -/
MeasureTheory.exists_measurableEmbedding_real : ∀ (α : Type u_1) [inst : MeasurableSpace α] [StandardBorelSpace α], ∃ f, MeasurableEmbedding f
-- Mathlib.Algebra.Algebra.Equiv
MulSemiringAction.toAlgEquiv_symm_apply : ∀ {G : Type u_2} (R : Type u_3) (A : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G A] [inst_5 : SMulCommClass G R A] (g : G) (a : A),
  (MulSemiringAction.toAlgEquiv R A g).symm a = g⁻¹ • a
-- Init.Data.Int.DivMod.Lemmas
Int.bdiv_add_bmod' : ∀ (x : ℤ) (m : ℕ), x.bdiv m * ↑m + x.bmod m = x
-- Lean.Widget.InteractiveCode
Lean.Widget.SubexprInfo.mk.sizeOf_spec : ∀ (info : Lean.Server.WithRpcRef Lean.Elab.InfoWithCtx) (subexprPos : Lean.SubExpr.Pos)
  (diffStatus? : Option Lean.Widget.DiffTag),
  sizeOf { info := info, subexprPos := subexprPos, diffStatus? := diffStatus? } =
    1 + sizeOf info + sizeOf subexprPos + sizeOf diffStatus?
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.LeanSemanticToken.mk.sizeOf_spec : ∀ (stx : Lean.Syntax) (type : Lean.Lsp.SemanticTokenType) (priority : ℕ),
  sizeOf { stx := stx, type := type, priority := priority } = 1 + sizeOf stx + sizeOf type + sizeOf priority
-- Mathlib.Probability.Process.Kolmogorov
ProbabilityTheory.IsAEKolmogorovProcess.edist_eq_zero_of_const_eq_zero : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace T] {mΩ : MeasurableSpace Ω}
  [inst_1 : PseudoEMetricSpace E] {p q : ℝ} {P : MeasureTheory.Measure Ω} {X : T → Ω → E},
  ProbabilityTheory.IsAEKolmogorovProcess X P p q 0 → ∀ (s t : T), ∀ᵐ (ω : Ω) ∂P, edist (X s ω) (X t ω) = 0
-- Mathlib.Algebra.Group.Commute.Defs
Commute.pow_right : ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, Commute a b → ∀ (n : ℕ), Commute a (b ^ n)
-- Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant
CategoryTheory.Functor.IsEventuallyConstantFrom.coconeιApp.congr_simp : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {F : CategoryTheory.Functor J C} {i₀ : J}
  (h : F.IsEventuallyConstantFrom i₀) [inst_2 : CategoryTheory.IsFiltered J] (j : J), h.coconeιApp j = h.coconeιApp j
-- Mathlib.Order.Interval.Finset.DenselyOrdered
WithTop.denselyOrdered_set_iff_subsingleton : ∀ {X : Type u_1} [inst : LinearOrder X] [LocallyFiniteOrder X] {s : Set (WithTop X)}, DenselyOrdered ↑s ↔ s.Subsingleton
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.LocalTimeType.mk.inj : ∀ {gmtOffset : ℤ} {isDst : Bool} {abbreviationIndex : UInt8} {gmtOffset_1 : ℤ} {isDst_1 : Bool}
  {abbreviationIndex_1 : UInt8},
  { gmtOffset := gmtOffset, isDst := isDst, abbreviationIndex := abbreviationIndex } =
      { gmtOffset := gmtOffset_1, isDst := isDst_1, abbreviationIndex := abbreviationIndex_1 } →
    gmtOffset = gmtOffset_1 ∧ isDst = isDst_1 ∧ abbreviationIndex = abbreviationIndex_1
-- Mathlib.Data.List.Sigma
List.dlookup_cons_eq : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a),
  List.dlookup a (⟨a, b⟩ :: l) = some b
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.nat_lt_aleph0 : ∀ (n : ℕ), ↑n < Cardinal.aleph0
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {fallback v : β},
  (m.insert k v).getD a fallback = if (k == a) = true then v else m.getD a fallback
-- Mathlib.Analysis.PSeriesComplex
Complex.summable_one_div_nat_cpow : ∀ {p : ℂ}, (Summable fun n => 1 / ↑n ^ p) ↔ 1 < p.re
-- Mathlib.GroupTheory.Perm.Basic
Equiv.swap_smul_involutive : ∀ {α : Type u} {β : Type v} [inst : DecidableEq α] [inst_1 : MulAction (Equiv.Perm α) β] (i j : α),
  Function.Involutive fun x => Equiv.swap i j • x
-- Mathlib.FieldTheory.IsAlgClosed.Classification
_private.Mathlib.FieldTheory.IsAlgClosed.Classification.0.IsAlgClosed.ringEquiv_of_Cardinal_eq_of_charP : ∀ {K : Type u} {L : Type v} [inst : Field K] [inst_1 : Field L] [IsAlgClosed K] [IsAlgClosed L] (p : ℕ)
  [Fact (Nat.Prime p)] [CharP K p] [CharP L p], Cardinal.aleph0 < Cardinal.mk K → Nonempty (K ≃ L) → Nonempty (K ≃+* L)
-- Lean.Meta.Sym.Arith.Types
/-- `NoNatZeroDivisors` instance for `type` if available.  -/
Lean.Meta.Sym.Arith.CommRing.noZeroDivInst? : Lean.Meta.Sym.Arith.CommRing → Option Lean.Expr
-- Mathlib.CategoryTheory.Limits.Types.PreservesLimit
/-- Let `F : J ⥤ Cᵒᵖ` be a functor. This is the family of morphisms
which consists of the single morphism
`colimit (F.leftOp ⋙ shrinkYoneda) ⟶ shrinkYoneda.obj (limit F).unop`
if `F` has a limit, or is the empty family otherwise.  -/
CategoryTheory.Presheaf.preservesLimitHomFamily : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} J] →
        [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] →
          (F : CategoryTheory.Functor J Cᵒᵖ) →
            [inst_3 : Small.{w, u'} J] →
              (h : PLift (CategoryTheory.Limits.HasLimit F)) →
                CategoryTheory.Presheaf.preservesLimitHomFamilySrc F ⟶
                  CategoryTheory.Presheaf.preservesLimitHomFamilyTgt F h
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.Gamma_nat_eq_factorial : ∀ (n : ℕ), Complex.Gamma (↑n + 1) = ↑n.factorial
-- Mathlib.Order.Nucleus
Nucleus.mk : {X : Type u_2} →
  [inst : SemilatticeInf X] →
    (toInfHom : InfHom X X) →
      (∀ (x : X), toInfHom.toFun (toInfHom.toFun x) ≤ toInfHom.toFun x) → (∀ (x : X), x ≤ toInfHom.toFun x) → Nucleus X
-- Mathlib.Topology.UniformSpace.Separation
IndiscreteTopology.uniformContinuous : ∀ {β : Type v} [inst : UniformSpace β] {α : Type u_1} [u : UniformSpace α] [IndiscreteTopology β] {f : α → β},
  UniformContinuous f
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- (Implementation): Use `ChartedSpace.locallyRingedSpaceMap`.  -/
ChartedSpace.locallyRingedSpaceMapAux : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_1} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_2} →
            [inst_3 : TopologicalSpace HM] →
              {IM : ModelWithCorners 𝕜 EM HM} →
                {M : Type u} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace HM M] →
                      {EN : Type u_3} →
                        [inst_6 : NormedAddCommGroup EN] →
                          [inst_7 : NormedSpace 𝕜 EN] →
                            {HN : Type u_4} →
                              [inst_8 : TopologicalSpace HN] →
                                {IN : ModelWithCorners 𝕜 EN HN} →
                                  {N : Type u} →
                                    [inst_9 : TopologicalSpace N] →
                                      [inst_10 : ChartedSpace HN N] →
                                        (f : M → N) →
                                          ContMDiff IM IN (↑⊤) f →
                                            ((ChartedSpace.locallyRingedSpace IM M).toPresheafedSpace ⟶
                                              (ChartedSpace.locallyRingedSpace IN N).toPresheafedSpace)
-- Mathlib.CategoryTheory.Sites.Whiskering
_private.Mathlib.CategoryTheory.Sites.Whiskering.0.CategoryTheory.Limits.WalkingMulticospan.functorExt.match_1.eq_1 : ∀ {J : CategoryTheory.Limits.MulticospanShape} (motive : CategoryTheory.Limits.WalkingMulticospan J → Sort u_3)
  (i : J.L) (h_1 : (i : J.L) → motive (CategoryTheory.Limits.WalkingMulticospan.left i))
  (h_2 : (i : J.R) → motive (CategoryTheory.Limits.WalkingMulticospan.right i)),
  (match CategoryTheory.Limits.WalkingMulticospan.left i with
    | CategoryTheory.Limits.WalkingMulticospan.left i => h_1 i
    | CategoryTheory.Limits.WalkingMulticospan.right i => h_2 i) =
    h_1 i
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instNonUnitalNonAssocSemiring : {𝕜 : Type u_2} →
  {α : Type u_5} →
    [inst : Preorder α] →
      [LocallyFiniteOrder α] → [inst_2 : NonUnitalNonAssocSemiring 𝕜] → NonUnitalNonAssocSemiring (IncidenceAlgebra 𝕜 α)
-- Batteries.Data.List.Basic
List.takeDTR.go.eq_1 : ∀ {α : Type u_1} (dflt : α) (a : Array α) (n : ℕ) (x_3 : α) (xs : List α),
  List.takeDTR.go dflt n.succ (x_3 :: xs) a = List.takeDTR.go dflt n xs (a.push x_3)
-- Mathlib.Data.Real.Basic
Real.instSemilatticeSup : SemilatticeSup ℝ
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.singleton_inj : ∀ {x y : ZFSet.{u_1}}, {x} = {y} ↔ x = y
-- Init.Data.UInt.Bitwise
UInt32.toFin_and : ∀ (a b : UInt32), (a &&& b).toFin = a.toFin &&& b.toFin
-- Mathlib.Analysis.LocallyConvex.Bounded
NormedSpace.isVonNBounded_ball : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  (r : ℝ), Bornology.IsVonNBounded 𝕜 (Metric.ball 0 r)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.nonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S},
  CategoryTheory.CategoryStruct.comp g₁ f₁ = CategoryTheory.CategoryStruct.comp g₂ f₂ →
    CategoryTheory.CategoryStruct.comp g₁ f₁ = b → Nonempty (h.LiftStruct g₁ g₂ b)
-- Mathlib.Algebra.AffineMonoid.Irreducible
/-- A finitely generated additive monoid with a single unit has finitely many irreducible
elements.  -/
finite_addIrreducible : ∀ {M : Type u_1} [inst : AddCommMonoid M] [Subsingleton (AddUnits M)] [AddMonoid.FG M], {p | AddIrreducible p}.Finite
-- Std.Time.Date.PlainDate
/-- Subtracts `Month.Offset` from a `PlainDate`, rolling over excess days as needed.
 -/
Std.Time.PlainDate.subMonthsRollOver : Std.Time.PlainDate → Std.Time.Month.Offset → Std.Time.PlainDate
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.not_mem_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α}, a ∉ ∅
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.mk.injEq : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F}
  (desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt)
  (fac :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (j : J),
        CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc s) = s.ι.app j)
      CategoryTheory.Limits.IsColimit.fac._autoParam)
  (uniq :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc s)
      CategoryTheory.Limits.IsColimit.uniq._autoParam)
  (desc_1 : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt)
  (fac_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (j : J),
        CategoryTheory.CategoryStruct.comp (t.ι.app j) (desc_1 s) = s.ι.app j)
      CategoryTheory.Limits.IsColimit.fac._autoParam)
  (uniq_1 :
    autoParam
      (∀ (s : CategoryTheory.Limits.Cocone F) (m : t.pt ⟶ s.pt),
        (∀ (j : J), CategoryTheory.CategoryStruct.comp (t.ι.app j) m = s.ι.app j) → m = desc_1 s)
      CategoryTheory.Limits.IsColimit.uniq._autoParam),
  ({ desc := desc, fac := fac, uniq := uniq } = { desc := desc_1, fac := fac_1, uniq := uniq_1 }) = (desc = desc_1)
-- Mathlib.Data.Finsupp.Single
Finsupp.mapRange_single : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} [inst : Zero M] [inst_1 : Zero N] {f : M → N} {hf : f 0 = 0} {a : α}
  {b : M}, (Finsupp.mapRange f hf fun₀ | a => b) = fun₀ | a => f b
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipPrefixWhile_eq_skipPrefixWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.skipPrefixWhile pat = String.Pos.ofToSlice (s.toSlice.skipPrefixWhile pat)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_le_size_insert : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, m.size ≤ (m.insert k v).size
-- Mathlib.Data.Finset.Disjoint
Finset.disjUnion_comm : ∀ {α : Type u_2} (s t : Finset α) (h : Disjoint s t), s.disjUnion t h = t.disjUnion s ⋯
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_of_contains_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {f : α → Bool} {k : α},
  (Std.TreeSet.filter f t).contains k = true → t.contains k = true
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples : ∀ {α : Type u_1} [inst : AddGroup α] [Infinite α] {g : α}, (∀ (x : α), x ∈ AddSubgroup.zmultiples g) → addOrderOf g = 0
-- Std.Http.Data.Method
/-- Move a resource to a new URI.
Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.9
 -/
Std.Http.Method.move : Std.Http.Method
-- Mathlib.Tactic.FunProp.Theorems
/-- Composition theorem e.g. `Continuous f → Continuous g → Continuous fun x ↦ f (g x)`

The numbers `fArgId` and `gArgId` store the argument index for `f` and `g` in the composition
theorem.  -/
Mathlib.Meta.FunProp.LambdaTheoremArgs.comp : ℕ → ℕ → Mathlib.Meta.FunProp.LambdaTheoremArgs
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.contStack.eq_1 : Turing.PartrecToTM2.contStack Turing.ToPartrec.Cont.halt = []
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
trdeg_le_of_surjective : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {A' : Type v}
  [inst_3 : CommRing A'] [inst_4 : Algebra R A'] (f : A →ₐ[R] A'),
  Function.Surjective ⇑f → Algebra.trdeg R A' ≤ Algebra.trdeg R A
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.span_int_coroot_support : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base),
  Submodule.span ℤ (⇑P.coroot '' ↑b.support) = Submodule.span ℤ (Set.range ⇑P.coroot)
-- Mathlib.Tactic.MoveAdd
/-- `sumList prepOp left_assoc? exs` assumes that `prepOp` is an `Expr`ession representing a
binary operation already fully applied up until its last two arguments and assumes that the
last two arguments are the operands of the operation.
Such an expression is the result of `prepareOp`.

If `exs` is the list `[e₁, e₂, ..., eₙ]` of `Expr`essions, then `sumList prepOp left_assoc? exs`
returns
* `prepOp (prepOp( ... prepOp (prepOp e₁ e₂) e₃) ... eₙ)`, if `left_assoc?` is `false`, and
* `prepOp e₁ (prepOp e₂ (... prepOp (prepOp eₙ₋₁  eₙ))`, if `left_assoc?` is `true`.
 -/
Mathlib.MoveAdd.sumList : Lean.Expr → Bool → List Lean.Expr → Lean.Expr
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.isQuotientMap_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsQuotientMap ⇑DomAddAct.mk
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.instInhabitedEntry : Inhabited Lean.Meta.SimpAll.Entry
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift_comp_lift_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) {Q : Type u_4} [inst_2 : CommMonoid Q] (k : S.LocalizationMap Q) {A : Type u_5}
  [inst_3 : CommMonoid A] {l : M →* A} (hl : ∀ (w : ↥S), IsUnit (l ↑w)), (k.lift hl).comp (f.lift ⋯) = f.lift hl
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_singleton_subset_iff`. -/
Set.diff_singleton_subset_iff : ∀ {α : Type u_1} {s t : Set α} {a : α}, s \ {a} ⊆ t ↔ s ⊆ insert a t
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_refl : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α], Equiv.Perm.sign (Equiv.refl α) = 1
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_inv_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology] (φ : S₁ ⟶ S₂)
  (h₁ : S₁.LeftHomologyData) (h₂ : S₂.LeftHomologyData),
  CategoryTheory.CategoryStruct.comp h₁.homologyIso.inv (CategoryTheory.ShortComplex.homologyMap φ) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftHomologyMap' φ h₁ h₂) h₂.homologyIso.inv
-- Mathlib.Topology.Sheaves.Skyscraper
instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [CategoryTheory.Limits.HasColimits C], (skyscraperSheafFunctor p₀).IsRightAdjoint
-- Lean.Attributes
Lean.instMonadLiftImportMAttrM : MonadLift Lean.ImportM Lean.AttrM
-- Mathlib.MeasureTheory.Measure.AEMeasurable
MeasureTheory.Measure.map_finset_sum : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {ι : Type u_7} {β : Type u_8} {mβ : MeasurableSpace β}
  {m : ι → MeasureTheory.Measure α} {f : α → β} {s : Finset ι},
  AEMeasurable f (∑ i ∈ s, m i) →
    MeasureTheory.Measure.map f (∑ i ∈ s, m i) = ∑ i ∈ s, MeasureTheory.Measure.map f (m i)
-- Mathlib.Tactic.CongrExclamation
/-- Convert a goal into an `Eq` goal if possible (since we have a better shot at those).
Also, if `tryClose := true`, then try to close the goal using an assumption, `Subsingleton.Elim`,
or definitional equality.  -/
Lean.MVarId.preCongr! : Lean.MVarId → Bool → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- `AddMonoidAlgebra.domCongr` as an `AddMonoidHom` from `AddAut`.  -/
AddMonoidAlgebra.domCongrAut : (R : Type u_1) →
  (A : Type u_4) →
    {M : Type u_7} →
      [inst : CommSemiring R] →
        [inst_1 : AddMonoid M] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R A] → AddAut M →+ Additive (AddMonoidAlgebra A M ≃ₐ[R] AddMonoidAlgebra A M)
-- Lean.DocString.Parser
/-- Formatter for `ifVersoModuleDocs`—formats according to the underlying formatters.
 -/
Lean.Doc.Parser.ifVersoModuleDocs.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.not_insertIfNew_eq_empty : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, ¬m.insertIfNew k v = ∅
-- Mathlib.Data.List.MinMax
List.not_of_mem_foldl_argAux : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] {l : List α},
  Std.Irrefl r → IsTrans α r → ∀ {a m : α} {o : Option α}, a ∈ l → m ∈ List.foldl (List.argAux r) o l → ¬r a m
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.toMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : CategoryTheory.Grp C), A.toMon = { X := A.X, mon := A.grp.toMonObj }
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).minKey? = t.minKey? ↔ ∀ {km : α}, t.minKey? = some km → ¬cmp k km = Ordering.eq
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.commRingEquiv_single_one : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (m : M),
  MonoidAlgebra.commRingEquiv (MonoidAlgebra.single m 1) = MonoidAlgebra.single 1 (MonoidAlgebra.single m 1)
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- Given a presentation `P` and equivalences `ι' ≃ ι` and
`σ' ≃ σ`, this is the induced presentation with variables indexed
by `ι'` and relations indexed by `σ'`  -/
Algebra.Presentation.reindex : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              Algebra.Presentation R S ι σ →
                {ι' : Type u_1} → {σ' : Type u_2} → ι' ≃ ι → σ' ≃ σ → Algebra.Presentation R S ι' σ'
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Functor.pi'CompEval_hom_app : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (F : (i : I) → CategoryTheory.Functor A (C i)) (i : I) (X : A),
  (CategoryTheory.Functor.pi'CompEval F i).hom.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
-- Init.Data.Vector.Count
Vector.countP_eq_size : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, Vector.countP p xs = n ↔ ∀ a ∈ xs, p a = true
-- Mathlib.Topology.UniformSpace.Basic
instBotUniformSpace : {α : Type ua} → Bot (UniformSpace α)
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.addMonoidHomCongrRight_refl : ∀ {M : Type u_4} {N : Type u_8} [inst : AddZeroClass M] [inst_1 : AddCommMonoid N],
  (AddEquiv.refl N).addMonoidHomCongrRight = AddEquiv.refl (M →+ N)
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.support_integralNormalization : ∀ {R : Type u} [inst : Semiring R] [IsCancelMulZero R] {f : Polynomial R}, f.integralNormalization.support = f.support
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- **Alias** of `OpenPartialHomeomorph.isOpenEmbedding`.

---

An open partial homeomorphism whose source is all of `X` defines an open embedding of `X` into
`Y`. The converse is also true; see `IsOpenEmbedding.toOpenPartialHomeomorph`.  -/
OpenPartialHomeomorph.to_isOpenEmbedding : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y), e.source = Set.univ → Topology.IsOpenEmbedding ↑e
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g)
          (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) h)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_sub_product : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α},
  Finset.image (fun x => x.1 - x.2) (s ×ˢ t) = s - t