mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Measure
/-- The image of an inner regular measure under right addition is again inner regular.  -/
MeasureTheory.innerRegular_map_add_right : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.InnerRegular] (g : G),
  (MeasureTheory.Measure.map (fun x => x + g) μ).InnerRegular
-- Mathlib.Order.Basic
/-- To prove associativity of a commutative binary operation `○`, we only to check
`(a ○ b) ○ c ≤ a ○ (b ○ c)` for all `a`, `b`, `c`.  -/
associative_of_commutative_of_le : ∀ {α : Type u_2} [inst : PartialOrder α] {f : α → α → α},
  Std.Commutative f → (∀ (a b c : α), f (f a b) c ≤ f a (f b c)) → Std.Associative f
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
/-- `x : FamilyOfElementsOnObjects F Y` is compatible if for any object `Z` such that
there exists a morphism `f : Z → Y i`, then the pullback of `x i` by `f` is independent
of `f` and `i`.  -/
CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} →
      {I : Type u_1} → {Y : I → C} → CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y → Prop
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_union_Icc_eq_Iic : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iio a ∪ Set.Icc a b = Set.Iic b
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.flipping_inverse_obj_obj_obj : ∀ {C : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} D]
  {E : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} E]
  (F : CategoryTheory.Functor D (CategoryTheory.Functor C E)) (k : C) (j : D),
  ((CategoryTheory.Functor.flipping.inverse.obj F).obj k).obj j = (F.obj j).obj k
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.instIsOverRestrict : ∀ {X Y S : AlgebraicGeometry.Scheme} [inst : X.Over S] [inst_1 : Y.Over S] (f : X.PartialMap Y)
  [AlgebraicGeometry.Scheme.PartialMap.IsOver S f] (U : X.Opens) (hU : Dense ↑U) (hU' : U ≤ f.domain),
  AlgebraicGeometry.Scheme.PartialMap.IsOver S (f.restrict U hU hU')
-- Mathlib.Data.Set.Functor
Set.instAlternative : Alternative Set
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.brecOn : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}
  {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop} {a a_1 : R} (t : RingConGen.Rel r a a_1),
  (∀ (a a_2 : R) (t : RingConGen.Rel r a a_2), RingConGen.Rel.below t → motive a a_2 t) → motive a a_1 t
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
/-- For `f : ℕ → ℝ≥0`, then `∑' k, f (k + i)` tends to zero. This does not require a summability
assumption on `f`, as otherwise all sums are zero.  -/
NNReal.tendsto_sum_nat_add : ∀ (f : ℕ → NNReal), Filter.Tendsto (fun i => ∑' (k : ℕ), f (k + i)) Filter.atTop (nhds 0)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) finite products
preserves finite biproducts.  -/
CategoryTheory.Limits.preservesBiproduct_of_preservesProduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C}
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F],
  CategoryTheory.Limits.PreservesBiproduct f F
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.funext_iff : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {F G : L →ᴸ L'},
  F = G ↔ F.onFunction = G.onFunction ∧ F.onRelation = G.onRelation
-- Std.Sat.AIG.RelabelNat
/-- Map an `AIG` with arbitrary atom identifiers to one that uses `Nat` as atom identifiers. This is
useful for preparing an `AIG` for CNF translation if it doesn't already use `Nat` identifiers.
 -/
Std.Sat.AIG.relabelNat : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → Std.Sat.AIG α → Std.Sat.AIG ℕ
-- Mathlib.Order.CompleteLattice.Basic
sSup_singleton : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {a : α}, sSup {a} = a
-- Mathlib.Topology.Bornology.Hom
/-- `id` as a `LocallyBoundedMap`.  -/
LocallyBoundedMap.id : (α : Type u_2) → [inst : Bornology α] → LocallyBoundedMap α α
-- Std.Data.HashMap.Basic
/-- Removes all mappings of the hash map for which the given function returns `false`.  -/
Std.HashMap.filter : {α : Type u} → {β : Type v} → {x : BEq α} → {x_1 : Hashable α} → (α → β → Bool) → Std.HashMap α β → Std.HashMap α β
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.fromOfGlobalSections_morphismRestrict : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {X : AlgebraicGeometry.Scheme} (f : A →+* ↑(X.presheaf.obj (Opposite.op ⊤)))
  (hf : Ideal.map f (HomogeneousIdeal.irrelevant 𝒜).toIdeal = ⊤) {r : A} {n : ℕ} (hn : 0 < n) (hr : r ∈ 𝒜 n),
  AlgebraicGeometry.Proj.fromOfGlobalSections 𝒜 f hf ∣_ AlgebraicGeometry.Proj.basicOpen 𝒜 r =
    CategoryTheory.CategoryStruct.comp (X.isoOfEq ⋯).hom
      (AlgebraicGeometry.Proj.toBasicOpenOfGlobalSections 𝒜 f ⋯ hn hr)
-- Mathlib.Algebra.Algebra.Rat
RingHomClass.toLinearMapClassRat : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : DivisionRing R] [inst_1 : CharZero R] [inst_2 : DivisionRing S]
  [inst_3 : CharZero S] [inst_4 : FunLike F R S] [RingHomClass F R S], LinearMapClass F ℚ R S
-- Mathlib.RingTheory.LocalProperties.Basic
RingHom.PropertyIsLocal.ofLocalizationSpanTarget : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.PropertyIsLocal P → RingHom.OfLocalizationSpanTarget P
-- Mathlib.Order.WithBot
WithTop.decidableLE.eq_3 : ∀ {α : Type u_1} [inst : LE α] [inst_1 : DecidableLE α] (a_1 b_1 : α),
  WithTop.decidableLE (some b_1) (some a_1) = decidable_of_iff' (b_1 ≤ a_1) ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.del.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_19),
  sizeOf (Lean.Compiler.LCNF.Code.del fvarId k h) = 1 + sizeOf fvarId + sizeOf k + sizeOf h
-- Mathlib.Topology.MetricSpace.PiNat
/-- In a product space `Π n, E n`, then `firstDiff x y` is the first index at which `x` and `y`
differ. If `x = y`, then by convention we set `firstDiff x x = 0`.  -/
PiNat.firstDiff : {E : ℕ → Type u_2} → ((n : ℕ) → E n) → ((n : ℕ) → E n) → ℕ
-- Mathlib.Topology.MetricSpace.Algebra
LipschitzMul.mk : ∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : Monoid β],
  (∃ C, LipschitzWith C fun p => p.1 * p.2) → LipschitzMul β
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- In a complete space, a continuous linear endomorphism `T` is **positive** if it is
symmetric and `∀ x, 0 ≤ re ⟪T x, x⟫`.  -/
ContinuousLinearMap.isPositive_def' : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {T : E →L[𝕜] E}, T.IsPositive ↔ IsSelfAdjoint T ∧ ∀ (x : E), 0 ≤ T.reApplyInnerSelf x
-- Mathlib.Order.LiminfLimsup
Filter.limsup_top_eq_ciSup : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {u : β → α} [Nonempty β],
  BddAbove (Set.range u) → Filter.limsup u ⊤ = ⨆ i, u i
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.nnnorm_smulRight : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E 𝕜) (z : G), ‖f.smulRight z‖₊ = ‖f‖₊ * ‖z‖₊
-- Mathlib.RingTheory.Congruence.Defs
RingCon.quot_mk_eq_coe : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R) (x : R), Quot.mk (⇑c) x = ↑x
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
/-- The homogeneous cochains of a topological representation.  -/
TopRep.homogeneousCochains : {k : Type u_1} →
  {G : Type u_2} →
    [inst : Ring k] →
      [inst_1 : Group G] →
        [inst_2 : TopologicalSpace k] →
          [inst_3 : TopologicalSpace G] → [IsTopologicalGroup G] → TopRep k G → CochainComplex (TopModuleCat k) ℕ
-- Lean.Data.Lsp.Basic
Lean.Lsp.instDecidableEqMarkupContent : DecidableEq Lean.Lsp.MarkupContent
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).inv
      (CategoryTheory.CategoryStruct.comp (s.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (t.π.app j) h
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : BEq α]
  [Std.LawfulBEqCmp cmp] [inst_2 : Std.TransCmp cmp] {k : α}, t.keys.contains k = t.contains k
-- Mathlib.Analysis.LConvolution
/-- Convolution is associative.  -/
MeasureTheory.lconvolution_assoc : ∀ {G : Type u_1} {mG : MeasurableSpace G} [inst : AddGroup G] [MeasurableAdd₂ G] [MeasurableNeg G]
  {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant] [MeasureTheory.SFinite μ] {f g k : G → ENNReal},
  Measurable f →
    Measurable g →
      Measurable k →
        MeasureTheory.lconvolution f (MeasureTheory.lconvolution g k μ) μ =
          MeasureTheory.lconvolution (MeasureTheory.lconvolution f g μ) k μ
-- Mathlib.Topology.NhdsSet
monotone_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X], Monotone nhdsSet
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extendCyclesIso_hom_naturality_assoc : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c')
  {j : ι} {j' : ι'} (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : L.HasHomology j]
  [inst_5 : (K.extend e).HasHomology j'] [inst_6 : (L.extend e).HasHomology j'] {Z : C} (h : L.cycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap (HomologicalComplex.extendMap φ e) j')
      (CategoryTheory.CategoryStruct.comp (L.extendCyclesIso e hj').hom h) =
    CategoryTheory.CategoryStruct.comp (K.extendCyclesIso e hj').hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ j) h)
-- Mathlib.RingTheory.AdjoinRoot
/-- The power basis `1, root g, ..., root g ^ (d - 1)` for `AdjoinRoot g`,
where `g` is a monic polynomial of degree `d`.  -/
AdjoinRoot.powerBasis' : {R : Type u_1} → [inst : CommRing R] → {g : Polynomial R} → g.Monic → PowerBasis R (AdjoinRoot g)
-- Mathlib.Algebra.Order.Group.Abs
mabs_max_le_max_mabs_mabs : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] {a b : G}, |max a b|ₘ ≤ max |a|ₘ |b|ₘ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.neg_point : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F} (P : W.Point), (-P).point = W.negMap P.point
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.Opposite
CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type v} [inst_1 : CategoryTheory.SmallCategory D]
  (F : CategoryTheory.Functor D Cᵒᵖ) [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.IsGrothendieckAbelian.{v, v, u} C] [Nonempty D] [F.Full],
  (F.comp (CategoryTheory.Abelian.IsGrothendieckAbelian.OppositeModuleEmbedding.embedding F)).Full
-- Mathlib.Data.Finsupp.BigOperators
Finset.support_sum_subset : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] (s : Finset (ι →₀ M)),
  (s.sum id).support ⊆ s.sup Finsupp.support
-- Init.Data.Array.DecidableEq
List.beq_toArray : ∀ {α : Type u_1} [inst : BEq α] (as bs : List α), (as.toArray == bs.toArray) = (as == bs)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfRoot_aeval : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S')
  (h₁ : (Polynomial.aeval pb.gen) (minpoly A pb'.gen) = 0) (h₂ : (Polynomial.aeval pb'.gen) (minpoly A pb.gen) = 0)
  (f : Polynomial A), (pb.equivOfRoot pb' h₁ h₂) ((Polynomial.aeval pb.gen) f) = (Polynomial.aeval pb'.gen) f
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.isEisensteinAt_iff : ∀ {R : Type u} [inst : CommSemiring R] (f : Polynomial R) (𝓟 : Ideal R),
  f.IsEisensteinAt 𝓟 ↔ f.leadingCoeff ∉ 𝓟 ∧ (∀ {n : ℕ}, n < f.natDegree → f.coeff n ∈ 𝓟) ∧ f.coeff 0 ∉ 𝓟 ^ 2
-- Init.Data.List.Attach
List.attach_cons : ∀ {α : Type u_1} {x : α} {xs : List α},
  (x :: xs).attach =
    ⟨x, ⋯⟩ ::
      List.map
        (fun x_1 =>
          match x_1 with
          | ⟨y, h⟩ => ⟨y, ⋯⟩)
        xs.attach
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
/-- A zero morphism `0 : X ⟶ X` is an isomorphism if and only if
the identity on `X` is zero.
 -/
CategoryTheory.Limits.isIsoZeroSelfEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (X : C) → CategoryTheory.IsIso 0 ≃ CategoryTheory.CategoryStruct.id X = 0
-- Std.Http.Internal.String
_private.Std.Http.Internal.String.0.Std.Http.Internal.UnquoteState.start.sizeOf_spec : sizeOf Std.Http.Internal.UnquoteState.start✝ = 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {fallback : α},
  ∅.maxKeyD fallback = fallback
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.ker_le_ker_of_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {S T : E →ₗ[𝕜] E}, S.IsSymmetric → T.IsSymmetric → S.range ≤ T.range → T.ker ≤ S.ker
-- Mathlib.GroupTheory.NoncommCoprod
/-- Coproduct of two `AddMonoidHom`s with the same codomain,
with a commutation assumption:
`f.noncommCoprod g (p : M × N) = f p.1 + g p.2`.
(Noncommutative case; in the commutative case, use `AddHom.coprod`.)  -/
AddMonoidHom.noncommCoprod : {M : Type u_1} →
  {N : Type u_2} →
    {P : Type u_3} →
      [inst : AddZeroClass M] →
        [inst_1 : AddZeroClass N] →
          [inst_2 : AddMonoid P] →
            (f : M →+ P) → (g : N →+ P) → (∀ (m : M) (n : N), AddCommute (f m) (g n)) → M × N →+ P
-- Mathlib.Order.CompleteBooleanAlgebra
CompletelyDistribLattice.toCompl : {α : Type u} → [self : CompletelyDistribLattice α] → Compl α
-- Mathlib.Analysis.Normed.Module.RieszLemma
/-- Riesz's lemma, which usually states that it is possible to find a
vector with norm 1 whose distance to a closed proper subspace is
arbitrarily close to 1. The statement here is in terms of multiples of
norms, since in general the existence of an element of norm exactly 1
is not guaranteed. For a variant giving an element with norm in `[1, R]`, see
`riesz_lemma_of_norm_lt`, and for a variant giving an element with norm
exactly one assuming stronger assumptions on the underlying field, see
`riesz_lemma_of_lt_one`.  -/
riesz_lemma : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {F : Subspace 𝕜 E}, IsClosed ↑F → (∃ x, x ∉ F) → ∀ {r : ℝ}, r < 1 → ∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- If given an orthogonal set of vectors, `gramSchmidt` fixes its input.  -/
InnerProductSpace.gramSchmidt_of_orthogonal : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E},
  (Pairwise fun x1 x2 => inner 𝕜 (f x1) (f x2) = 0) → InnerProductSpace.gramSchmidt 𝕜 f = f
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The degree of `v ∈ s` in `G` is at most the degree in `G.between s sᶜ` plus the excluded
vertices from `s`.  -/
SimpleGraph.degree_le_between_add : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} [inst : DecidableEq V] [inst_1 : Fintype V] {s : Finset V}
  [inst_2 : DecidableRel G.Adj], v ∈ s → G.degree v ≤ (SimpleGraph.between (↑s) (↑s)ᶜ G).degree v + s.card
-- Mathlib.Combinatorics.Graph.Basic
Graph.inc_eq_inc_iff_isLink_eq_isLink : ∀ {α : Type u_1} {β : Type u_2} {e f : β} {G₁ G₂ : Graph α β}, G₁.Inc e = G₂.Inc f ↔ G₁.IsLink e = G₂.IsLink f
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.single_le_iff : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, ((toDegLex fun₀ | b => 1) ≤ toDegLex fun₀ | a => 1) ↔ a ≤ b
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.map_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K₁ L₁ K₂ L₂ K₃ L₃ : CochainComplex C ℤ} (φ₁ : K₁ ⟶ L₁)
  (φ₂ : K₂ ⟶ L₂) (φ₃ : K₃ ⟶ L₃) (a : K₁ ⟶ K₂) (b : L₁ ⟶ L₂)
  (comm : CategoryTheory.CategoryStruct.comp φ₁ b = CategoryTheory.CategoryStruct.comp a φ₂) (a' : K₂ ⟶ K₃)
  (b' : L₂ ⟶ L₃) (comm' : CategoryTheory.CategoryStruct.comp φ₂ b' = CategoryTheory.CategoryStruct.comp a' φ₃),
  CochainComplex.mappingCone.map φ₁ φ₃ (CategoryTheory.CategoryStruct.comp a a')
      (CategoryTheory.CategoryStruct.comp b b') ⋯ =
    CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.map φ₁ φ₂ a b comm)
      (CochainComplex.mappingCone.map φ₂ φ₃ a' b' comm')
-- Mathlib.RingTheory.FiniteType
/-- If a set `S` generates an additive monoid `M`, then the image of `M` generates, as algebra,
`R[M]`.  -/
AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure : ∀ {R : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] [inst_1 : CommSemiring R] {S : Set M},
  AddSubmonoid.closure S = ⊤ → Function.Surjective ⇑(MvPolynomial.aeval fun s => AddMonoidAlgebra.of' R M ↑s)
-- Init.Prelude
/-- Pack a `Nat` encoding a valid codepoint into a `Char`.
This function is overridden with a native implementation.
 -/
Char.ofNatAux : (n : ℕ) → n.isValidChar → Char
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin
Fin.reduceMul : Lean.Meta.Simp.DSimproc
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.comp.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) [inst_5 : Algebra R T]
  [inst_6 : IsScalarTower R S T],
  Q.comp P =
    { toGenerators := Q.comp P.toGenerators,
      relation := Sum.elim (Q.compRelationAux P) fun rp => (MvPolynomial.rename Sum.inr) (P.relation rp),
      span_range_relation_eq_ker := ⋯ }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.toList_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {c : ℕ}, (Std.DHashMap.emptyWithCapacity c).toList = []
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
nullMeasurableSet_of_null_frontier : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α}, μ (frontier s) = 0 → MeasureTheory.NullMeasurableSet s μ
-- Mathlib.Algebra.Category.Grp.Limits
/-- The category of commutative groups has all limits.  -/
CommGrpCat.hasLimitsOfSize : ∀ [UnivLE.{v, u}], CategoryTheory.Limits.HasLimitsOfSize.{w, v, u, u + 1} CommGrpCat
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂)[k] = m₁[k]
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
CategoryTheory.Limits.hasLimit_of_domain_hasTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  [CategoryTheory.Limits.HasTerminal J] {F : CategoryTheory.Functor J C}
  [∀ (i j : J) (f : i ⟶ j), CategoryTheory.IsIso (F.map f)], CategoryTheory.Limits.HasLimit F
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.toImplicit.match_1.eq_2 : ∀ (motive : Lean.Expr → Sort u_1) (e : Lean.Expr)
  (h_1 :
    (binderName : Lean.Name) →
      (t b : Lean.Expr) →
        (binderName_1 : Lean.Name) →
          (binderType body : Lean.Expr) →
            (binderInfo : Lean.BinderInfo) →
              b = Lean.Expr.forallE binderName_1 binderType body binderInfo →
                (binderInfo_1 : Lean.BinderInfo) →
                  motive
                    (Lean.Expr.forallE binderName t (Lean.Expr.forallE binderName_1 binderType body binderInfo)
                      binderInfo_1))
  (h_2 : (e : Lean.Expr) → motive e),
  (∀ (binderName : Lean.Name) (t : Lean.Expr) (binderName_1 : Lean.Name) (binderType body : Lean.Expr)
      (binderInfo binderInfo_1 : Lean.BinderInfo),
      e = Lean.Expr.forallE binderName t (Lean.Expr.forallE binderName_1 binderType body binderInfo) binderInfo_1 →
        False) →
    (match e with
      | Lean.Expr.forallE binderName t (b@h:(Lean.Expr.forallE binderName_1 binderType body binderInfo)) binderInfo_1 =>
        h_1 binderName t b binderName_1 binderType body binderInfo h binderInfo_1
      | e => h_2 e) =
      h_2 e
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Preadditive
CategoryTheory.Localization.Preadditive.add'.congr_simp : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Preadditive C]
  {L : CategoryTheory.Functor C D} (W W_1 : CategoryTheory.MorphismProperty C) (e_W : W = W_1)
  [inst_3 : L.IsLocalization W] [inst_4 : W.HasLeftCalculusOfFractions] {X Y : C} (f₁ f₁_1 : L.obj X ⟶ L.obj Y),
  f₁ = f₁_1 →
    ∀ (f₂ f₂_1 : L.obj X ⟶ L.obj Y),
      f₂ = f₂_1 →
        CategoryTheory.Localization.Preadditive.add' W f₁ f₂ =
          CategoryTheory.Localization.Preadditive.add' W_1 f₁_1 f₂_1
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- there are unique morphisms from the object  -/
CategoryTheory.Limits.IsZero.unique_from : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C},
  CategoryTheory.Limits.IsZero X → ∀ (Y : C), Nonempty (Unique (Y ⟶ X))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_insertManyIfNewUnit_list_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List α}, (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).size ≤ t.size + l.length
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.instSemiring : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module A V] → (ρ : Representation A G V) → Semiring (ρ.IntertwiningMap ρ)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralAlgNorm.congr_simp : ∀ (K : Type u_2) [inst : NormedField K] (L : Type u_3) [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsUltrametricDist K] [h_alg : Algebra.IsAlgebraic K L], spectralAlgNorm K L = spectralAlgNorm K L
-- Mathlib.Algebra.WithConv
WithConv.ofConv_injective : ∀ {A : Type u_2}, Function.Injective WithConv.ofConv