mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Submersion
_private.Mathlib.Geometry.Manifold.Submersion.0.Manifold.IsSubmersion.eq_1 : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {H : Type u_7} {G : Type u_9} {E : Type u} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : TopologicalSpace H] [inst_6 : TopologicalSpace G] (I : ModelWithCorners 𝕜 E H)
  (J : ModelWithCorners 𝕜 E'' G) {M : Type u_11} {N : Type u_13} [inst_7 : TopologicalSpace M]
  [inst_8 : ChartedSpace H M] [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] (n : WithTop ℕ∞) (f : M → N),
  Manifold.IsSubmersion I J n f = ∃ F x x_1, Manifold.IsSubmersionOfComplement F I J n f
-- Mathlib.Tactic.Ring.RingNF
/-- A cleanup routine, which simplifies normalized polynomials to a more human-friendly format.  -/
Mathlib.Tactic.RingNF.cleanup : Mathlib.Tactic.RingNF.Config → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Order.UpperLower.Basic
Set.antitone_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, (Antitone fun x => x ∈ s) ↔ IsLowerSet s
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.finrank_adjoin_eq_one_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E},
  Module.finrank F ↥(IntermediateField.adjoin F S) = 1 ↔ S ⊆ ↑⊥
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.lim.congr_simp : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasLimitsOfShape J C], CategoryTheory.Limits.lim = CategoryTheory.Limits.lim
-- Mathlib.Data.Rel
/-- A relation on `α` and `β`, aka a set-valued function, aka a partial multifunction.

We represent them as sets due to how relations are used in the context of uniform spaces.  -/
SetRel : Type u_6 → Type u_7 → Type (max u_7 u_6)
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_sup_le_or_aux_right : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  Filter.blimsup u f q ≤ Filter.blimsup u f fun x => p x ∨ q x
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.subNegZeroMonoid.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : Zero M₁] [inst_2 : SMul ℕ M₁] [inst_3 : Neg M₁]
  [inst_4 : Sub M₁] [inst_5 : SMul ℤ M₁] [inst_6 : SubNegZeroMonoid M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (one : f 0 = 0) (mul : ∀ (x y : M₁), f (x + y) = f x + f y) (inv : ∀ (x : M₁), f (-x) = -f x)
  (div : ∀ (x y : M₁), f (x - y) = f x - f y) (npow : ∀ (x : M₁) (n : ℕ), f (n • x) = n • f x)
  (zpow : ∀ (x : M₁) (n : ℤ), f (n • x) = n • f x),
  Function.Injective.subNegZeroMonoid f hf one mul inv div npow zpow =
    { toSubNegMonoid := Function.Injective.subNegMonoid f hf one mul inv div npow zpow, neg_zero := ⋯ }
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from additive commutative groups to additive commutative monoids
preserves all limits. (That is, the underlying additive commutative monoids could have been
computed instead as limits in the category of additive commutative monoids.)  -/
AddCommGrpCat.forget₂AddCommMon_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1}
    (CategoryTheory.forget₂ AddCommGrpCat AddCommMonCat)
-- Mathlib.Tactic.DepRewrite
Mathlib.Tactic.DepRewrite.dcongrArg : ∀ {α : Sort u} {a a' : α} {β : (a' : α) → a = a' → Sort v} (h : a = a') (f : (a' : α) → (h : a = a') → β a' h),
  f a ⋯ = ⋯ ▸ f a' h
-- Mathlib.GroupTheory.Solvable
Group.instIsSolvableQuotientSubgroup : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal] [Group.IsSolvable G], Group.IsSolvable (G ⧸ H)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
_private.Mathlib.CategoryTheory.Limits.Shapes.Reflexive.0.CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.match_3.eq_1 : ∀ (motive : (Y X : CategoryTheory.Limits.WalkingParallelPair) → (X ⟶ Y) → Sort u_1)
  (h_1 :
    Unit →
      motive CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero
        CategoryTheory.Limits.WalkingParallelPairHom.left)
  (h_2 :
    Unit →
      motive CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.WalkingParallelPair.zero
        CategoryTheory.Limits.WalkingParallelPairHom.right)
  (h_3 :
    (x : CategoryTheory.Limits.WalkingParallelPair) → motive x x (CategoryTheory.Limits.WalkingParallelPairHom.id x)),
  (match CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.WalkingParallelPair.zero,
      CategoryTheory.Limits.WalkingParallelPairHom.left with
    | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero),
      CategoryTheory.Limits.WalkingParallelPairHom.left => h_1 ()
    | .(CategoryTheory.Limits.WalkingParallelPair.one), .(CategoryTheory.Limits.WalkingParallelPair.zero),
      CategoryTheory.Limits.WalkingParallelPairHom.right => h_2 ()
    | x, .(x), CategoryTheory.Limits.WalkingParallelPairHom.id .(x) => h_3 x) =
    h_1 ()
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Icc_add_Icc_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [inst_2 : DecidableEq α] [AddLeftMono α] [AddRightMono α]
  [inst_5 : LocallyFiniteOrder α] (a b c d : α), Finset.Icc a b + Finset.Icc c d ⊆ Finset.Icc (a + c) (b + d)
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderLeftLeaningMinOpposite : ∀ {α : Type u_1} {il : LE α} {im : Min α} [Std.LawfulOrderLeftLeaningMin α], Std.LawfulOrderLeftLeaningMax α
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instPreservesOneHypercoversOverObjPostOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  (F : CategoryTheory.Functor C D) (X : C) [F.PreservesOneHypercovers J K],
  (CategoryTheory.Over.post F).PreservesOneHypercovers (J.over X) (K.over (F.obj X))
-- Mathlib.CategoryTheory.Triangulated.TStructure.SpectralObject
CategoryTheory.Triangulated.TStructure.triangleω₁δ_obj_obj₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : CategoryTheory.IsTriangulated C] (a b c : EInt) (hab : a ≤ b)
  (hbc : b ≤ c) (j : C), ((t.triangleω₁δ a b c hab hbc).obj j).obj₁ = (t.eTruncGE.obj a).obj ((t.eTruncLT.obj b).obj j)
-- Mathlib.RingTheory.WittVector.Isocrystal
WittVector.instModuleFractionRingStandardOneDimIsocrystal : (p : ℕ) →
  [inst : Fact (Nat.Prime p)] →
    (k : Type u_1) →
      [inst_1 : CommRing k] →
        (_m : ℤ) → Module (FractionRing (WittVector p k)) (WittVector.StandardOneDimIsocrystal p k _m)
-- Std.Data.HashMap.Lemmas
_private.Std.Data.HashMap.Lemmas.0.GetElem?.match_1.eq_2 : ∀ (elem : outParam (Type u_1)) (motive : Option elem → Sort u_2) (h_1 : (e : elem) → motive (some e))
  (h_2 : Unit → motive none),
  (match none with
    | some e => h_1 e
    | none => h_2 ()) =
    h_2 ()
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_pointReflection : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (x y : P₁), (AffineEquiv.pointReflection k x) y = (Equiv.pointReflection x) y
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInv.eq_1 : ∀ {M : Type u_1} [inst : Monoid M] (S : Submonoid M),
  S.leftInv = { carrier := {x | ∃ y, x * ↑y = 1}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsSatisfiable.mono : ∀ {L : FirstOrder.Language} {T T' : L.Theory}, T'.IsSatisfiable → T ⊆ T' → T.IsSatisfiable
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.norm_iteratedFDeriv_le_seminorm : ∀ (𝕜 : Type u_2) {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 : NormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] (f : SchwartzMap E F) (n : ℕ) (x₀ : E),
  ‖iteratedFDeriv ℝ n (⇑f) x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 n) f
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.homOfPiHom_φ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) {J : Type w} (f : J → C) (φ : (j : J) → f j ⟶ X)
  (j : J), (CategoryTheory.Limits.FormalCoproduct.homOfPiHom X f φ).φ j = φ j
-- Init.Data.Vector.Lemmas
Vector.getElem?_pop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ}, xs.pop[i]? = if i < n - 1 then xs[i]? else none
-- Mathlib.Analysis.Complex.Exponential
/-- A finite initial segment of the exponential series, followed by an arbitrary tail.
For fixed `n` this is just a linear map w.r.t. `r`, and each map is a simple linear function
of the previous (see `expNear_succ`), with `expNear n x r ⟶ exp x` as `n ⟶ ∞`,
for any `r`.  -/
Real.expNear : ℕ → ℝ → ℝ → ℝ
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_dvdNotUnit_mk_iff : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {a b : M},
  DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
_private.Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc.0.CategoryTheory.Limits.termG₄ : Lean.ParserDescr
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- `p.sum f` is `∑ n ∈ p.support, f n (p.coeff n)`, i.e., one sums the values of functions applied
to coefficients of the polynomial `p`.  -/
SkewPolynomial.sum : {R : Type u_1} → [inst : Semiring R] → {S : Type u_5} → [AddCommMonoid S] → SkewPolynomial R → (ℕ → R → S) → S
-- Mathlib.AlgebraicGeometry.Modules.Tilde
_private.Mathlib.AlgebraicGeometry.Modules.Tilde.0.AlgebraicGeometry.QuasicoherentTilde.Aux.of_le : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {V : (AlgebraicGeometry.Spec R).Opens} (g : ↑R),
  PrimeSpectrum.basicOpen g ≤ V →
    AlgebraicGeometry.QuasicoherentTilde.Aux✝ M V →
      AlgebraicGeometry.QuasicoherentTilde.Aux✝ M (PrimeSpectrum.basicOpen g)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_op_inv : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] (s : Finset α),
  Finset.image MulOpposite.op s⁻¹ = (Finset.image MulOpposite.op s)⁻¹
-- Mathlib.Order.Filter.AtTopBot.Tendsto
/-- **Alias** of `Filter.tendsto_atTop_atTop_of_monotone`. -/
Monotone.tendsto_atTop_atTop : ∀ {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → (∀ (b : β), ∃ a, b ≤ f a) → Filter.Tendsto f Filter.atTop Filter.atTop
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.measure_compl_aeSeqSet_eq_zero : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} [Countable ι] (hf : ∀ (i : ι), AEMeasurable (f i) μ),
  (∀ᵐ (x : α) ∂μ, p x fun n => f n x) → μ (aeSeqSet hf p)ᶜ = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
/-- To check whether a morphism is coequalized by the maps of a pushout cocone, it suffices to check
it for `inl t` and `inr t`  -/
CategoryTheory.Limits.PushoutCocone.coequalizer_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z}
  (t : CategoryTheory.Limits.PushoutCocone f g) {W : C} {k l : t.pt ⟶ W},
  CategoryTheory.CategoryStruct.comp t.inl k = CategoryTheory.CategoryStruct.comp t.inl l →
    CategoryTheory.CategoryStruct.comp t.inr k = CategoryTheory.CategoryStruct.comp t.inr l →
      ∀ (j : CategoryTheory.Limits.WalkingSpan),
        CategoryTheory.CategoryStruct.comp (t.ι.app j) k = CategoryTheory.CategoryStruct.comp (t.ι.app j) l
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.instIsIsoFunctorHoCatAdjCounit' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  CategoryTheory.IsIso HomotopicalAlgebra.CofibrantObject.HoCat.adjCounit'
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.ball_eq_preimage : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] (x : E)
  (r : ℝ), Euclidean.ball x r = ⇑toEuclidean ⁻¹' Metric.ball (toEuclidean x) r
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.fst_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {ρ : MeasureTheory.Measure (α × β)}, ρ.fst Set.univ = ρ Set.univ
-- Init.Data.Vector.Lemmas
/-- Use this as `induction ass using vector₃_induction` on a hypothesis of the form `ass : Vector (Vector (Vector α n) m) k`.
The hypothesis `ass` will be replaced with a hypothesis `ass : Array (Array (Array α))`
along with additional hypotheses `h₁ : ass.size = k`, `h₂ : ∀ xs ∈ ass, xs.size = m`,
and `h₃ : ∀ xs ∈ ass, ∀ x ∈ xs, x.size = n`.
Appearances of the original `ass` in the goal will be replaced with
`Vector.mk (xss.attach.map (fun ⟨xs, m⟩ => Vector.mk (xs.attach.map (fun ⟨x, m'⟩ => Vector.mk x ⋯)) ⋯)) ⋯`.
 -/
Vector.vector₃_induction : ∀ {α : Type u_1} {n m k : ℕ} (P : Vector (Vector (Vector α n) m) k → Prop),
  (∀ (xss : Array (Array (Array α))) (h₁ : xss.size = k) (h₂ : ∀ xs ∈ xss, xs.size = m)
      (h₃ : ∀ xs ∈ xss, ∀ as ∈ xs, as.size = n),
      P
        (Vector.mk
          (Array.map
            (fun x =>
              match x with
              | ⟨xs, m_1⟩ =>
                Vector.mk
                  (Array.map
                    (fun x =>
                      match x with
                      | ⟨as, m'⟩ => Vector.mk as ⋯)
                    xs.attach)
                  ⋯)
            xss.attach)
          ⋯)) →
    ∀ (xss : Vector (Vector (Vector α n) m) k), P xss
-- Lean.Meta.LitValues
/-- Return `some c` if `e` is a `Char.ofNat`-application that encodes the character `c`.  -/
Lean.Meta.getCharValue? : Lean.Expr → Lean.MetaM (Option Char)
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.equiv.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [inst_2 : L.IsLocalization W] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y],
  CategoryTheory.Localization.SmallHom.equiv W L = CategoryTheory.Localization.SmallHom.equiv W L
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryLT_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (hto : t.Ordered) {k : α} (he : ∃ a ∈ t, compare a k = Ordering.lt),
  Std.DTreeMap.Internal.Impl.Const.getEntryLT k t hto he =
    ((Std.DTreeMap.Internal.Impl.getEntryLT k t hto he).fst, (Std.DTreeMap.Internal.Impl.getEntryLT k t hto he).snd)
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.minpolyX_eq_zero_iff : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K), f.minpolyX ↥K⟮f⟯ = 0 ↔ ∃ c, f = RatFunc.C c
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Sums of harmonic functions are harmonic.
 -/
InnerProductSpace.HarmonicAt.add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E},
  InnerProductSpace.HarmonicAt f₁ x → InnerProductSpace.HarmonicAt f₂ x → InnerProductSpace.HarmonicAt (f₁ + f₂) x
-- Init.Data.BitVec.Lemmas
/-- rotateRight is invariant under `mod` by the bitwidth.  -/
BitVec.rotateRight_mod_eq_rotateRight : ∀ {w : ℕ} {x : BitVec w} {r : ℕ}, x.rotateRight (r % w) = x.rotateRight r
-- Mathlib.Data.List.Sigma
List.lookup_ext : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {l₀ l₁ : List (Sigma β)},
  l₀.NodupKeys → l₁.NodupKeys → (∀ (x : α) (y : β x), y ∈ List.dlookup x l₀ ↔ y ∈ List.dlookup x l₁) → l₀.Perm l₁
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wSameSide_of_left_mem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x : P} (y : P), x ∈ s → s.WSameSide x y
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.unitOfList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.DTreeMap.Const.unitOfList [] cmp = ∅
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
/-- The upper half plane as a subset of `ℂ`.
This is convenient for taking derivatives of functions on the upper half plane.  -/
UpperHalfPlane.upperHalfPlaneSet : Set ℂ
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.mul_assoc : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x y z : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation F ((x.mul y).mul z) (x.mul (y.mul z))
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.IsCovering.star_bijective : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] {φ : U ⥤q V},
  φ.IsCovering → ∀ (u : U), Function.Bijective (φ.star u)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.range_toSubgraph : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β},
  Set.range SimpleGraph.Copy.toSubgraph = {B' | Nonempty (A ≃g B'.coe)}
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.fold_eq_foldl_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w} {f : δ → α → δ}
  {init : δ}, Std.DHashMap.fold (fun d a x => f d a) init m = Array.foldl f init m.keysArray
-- Mathlib.Tactic.Ring.Compare
Mathlib.Tactic.Ring.add_lt_add_left : ∀ {α : Type u_1} [inst : CommSemiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {b c : α},
  b < c → ∀ (a : α), b + a < c + a
-- Lean.LocalContext
/-- Sort the given `FVarId`s by the order in which they appear in `lctx`. If any of
the `FVarId`s do not appear in `lctx`, the result is unspecified.
 -/
Lean.LocalContext.sortFVarsByContextOrder : Lean.LocalContext → Array Lean.FVarId → Array Lean.FVarId
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.instMonoAbelianImageToKernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.Mono S.abelianImageToKernel
-- Mathlib.GroupTheory.IsSubnormal
/-- A characterisation of satisfying `IsSubnormal` in terms of chains of subgroups, each normal in
the following one.

The sequence stabilises once it reaches `⊤`, which is guaranteed at the asserted `n`.
 -/
Subgroup.IsSubnormal.isSubnormal_iff : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G},
  H.IsSubnormal ↔ ∃ n f, Monotone f ∧ (∀ (i : ℕ), ((f i).subgroupOf (f (i + 1))).Normal) ∧ f 0 = H ∧ f n = ⊤
-- Mathlib.Topology.Connected.TotallyDisconnected
Continuous.connectedComponentsMap.congr_simp : ∀ {α : Type u} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {f f_1 : α → β} (e_f : f = f_1)
  (h : Continuous f) (a a_1 : ConnectedComponents α),
  a = a_1 → h.connectedComponentsMap a = ⋯.connectedComponentsMap a_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k : α}, k ∈ m.insertMany l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ \ t₂).get? k = none
-- Mathlib.Order.RelSeries
RelSeries.length_pos : ∀ {α : Type u_1} {r : SetRel α α} {s : RelSeries r} [r.IsIrrefl], 0 < s.length ↔ {x | x ∈ s}.Nontrivial
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.Hom.mk.sizeOf_spec : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] {Y Z : ContinuousGeneratedByCat X}
  [inst_1 : SizeOf ι] [inst_2 : (a : ι) → SizeOf (X a)] (hom : Topology.ContinuousMapGeneratedBy X ↑Y ↑Z),
  sizeOf { hom := hom } = 1 + sizeOf hom
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.buildTable.eq_1 : ∀ (pat : String.Slice),
  String.Slice.Pattern.ForwardSliceSearcher.buildTable pat =
    if h : pat.utf8ByteSize = 0 then Vector.cast ⋯ #v[]
    else
      let arr := Array.emptyWithCapacity pat.utf8ByteSize;
      let arr' := arr.push 0;
      String.Slice.Pattern.ForwardSliceSearcher.buildTable.go✝ pat arr' ⋯ ⋯ ⋯
-- Init.Data.Option.Lemmas
Option.guard_beq_none : ∀ {α : Type u_1} [inst : BEq α] {x : α} {p : α → Bool}, (Option.guard p x == none) = !p x
-- Mathlib.Data.Ordmap.Ordset
Ordnode.Valid'.mk : ∀ {α : Type u_1} [inst : Preorder α] {lo : WithBot α} {t : Ordnode α} {hi : WithTop α},
  t.Bounded lo hi → t.Sized → t.Balanced → Ordnode.Valid' lo t hi
-- Mathlib.Order.Filter.Map
/-- The analog of `Set.kernImage` for filters.
A set `s` belongs to `Filter.kernMap m f` if either of the following equivalent conditions hold.

1. There exists a set `t ∈ f` such that `s = Set.kernImage m t`. This is used as a definition.
2. There exists a set `t` such that `tᶜ ∈ f` and `sᶜ = m '' t`, see `Filter.mem_kernMap_iff_compl`
   and `Filter.compl_mem_kernMap`.

This definition is useful because it gives a right adjoint to `Filter.comap`, and because it has a
nice interpretation when working with `co-` filters (`Filter.cocompact`, `Filter.cofinite`, ...).
For example, `kernMap m (cocompact α)` is the filter generated by the complements of the sets
`m '' K` where `K` is a compact subset of `α`.  -/
Filter.kernMap : {α : Type u_1} → {β : Type u_2} → (α → β) → Filter α → Filter β
-- Init.Data.SInt.Bitwise
Int8.or_not_self : ∀ {a : Int8}, a ||| ~~~a = -1
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instIsEquivalenceRestrictScalarsToRingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (e : R ≃+* S),
  (AlgCat.restrictScalars e.toRingHom).IsEquivalence
-- Mathlib.Topology.NhdsWithin
dense_pi : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (α i)] {s : (i : ι) → Set (α i)} (I : Set ι),
  (∀ i ∈ I, Dense (s i)) → Dense (I.pi s)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C)
  (X Y : CategoryTheory.Discrete PUnit.{u_1 + 1}),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A) X
      Y =
    CategoryTheory.MonObj.mul
-- Mathlib.Order.Filter.Cofinite
Set.Finite.cofinite_inf_principal_compl : ∀ {α : Type u_2} {s : Set α}, s.Finite → Filter.cofinite ⊓ Filter.principal sᶜ = Filter.cofinite
-- Mathlib.CategoryTheory.Sigma.Basic
/-- The identity morphism on an object.  -/
CategoryTheory.Sigma.SigmaHom.id : {I : Type w₁} →
  {C : I → Type u₁} →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] → (X : (i : I) × C i) → CategoryTheory.Sigma.SigmaHom X X
-- Mathlib.Algebra.Group.Shrink
Shrink.instCommSemigroup.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : CommSemigroup α],
  Shrink.instCommSemigroup = (equivShrink α).symm.commSemigroup