mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_unop2 : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : Bᵒᵖ} {f g : a ⟶ b} (η : f ⟶ g),
  Bicategory.Opposite.op2 η.unop2 = η
-- Mathlib.MeasureTheory.Function.L2Space
_private.Mathlib.MeasureTheory.Function.L2Space.0.MeasureTheory.«term⟪_,_⟫_1» : Lean.ParserDescr
-- Lean.Widget.UserWidget
_private.Lean.Widget.UserWidget.0.Lean.Widget.evalWidgetInstanceUnsafe : Lean.Expr → Lean.MetaM Lean.Widget.WidgetInstance
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.step_flatMapM : ∀ {α β α₂ γ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : MonadAttach m] [inst_2 : LawfulMonad m]
  [inst_3 : WeaklyLawfulMonadAttach m] [inst_4 : Std.Iterator α Id β] [inst_5 : Std.Iterator α₂ m γ]
  {f : β → m (Std.IterM m γ)} {it₁ : Std.Iter β},
  (Std.Iter.flatMapM f it₁).step =
    match it₁.step with
    | ⟨Std.IterStep.yield it₁' b, h⟩ => do
      let fx ← MonadAttach.attach (f b)
      pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.flatMapAfterM f it₁' (some ↑fx)) ⋯))
    | ⟨Std.IterStep.skip it₁', h⟩ =>
      pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (Std.Iter.flatMapAfterM f it₁' none) ⋯))
    | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Icc : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a b c : G₀},
  0 ≤ a → b ≤ c → (fun x => a * x) '' Set.Icc b c = Set.Icc (a * b) (a * c)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Non-dependent recursion principle for localizations: given elements `f x y : p`
for all `x` and `y`, such that `r S x x'` and `r S y y'` implies `f x y = f x' y'`,
then `f` is defined on the whole `Localization S`.  -/
AddLocalization.liftOn₂ : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} →
      {p : Sort u} →
        AddLocalization S →
          AddLocalization S →
            (f : M → ↥S → M → ↥S → p) →
              (∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
                  (AddLocalization.r S) (a, b) (a', b') →
                    (AddLocalization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') →
                p
-- Mathlib.Order.BooleanSubalgebra
/-- BooleanSubalgebras of a lattice form a complete lattice.  -/
BooleanSubalgebra.instCompleteLattice : {α : Type u_2} → [inst : BooleanAlgebra α] → CompleteLattice (BooleanSubalgebra α)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the spans of two vectors are equal, twice angles with those vectors on the right are
equal.  -/
Orientation.two_zsmul_oangle_right_of_span_eq : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) {y z : V}, ℝ ∙ y = ℝ ∙ z → 2 • o.oangle x y = 2 • o.oangle x z
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
PreQuasiregular.instOne : {R : Type u_1} → [NonUnitalSemiring R] → One (PreQuasiregular R)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.irreducible_iff_natDegree' : ∀ {R : Type u} [inst : CommSemiring R] [NoZeroDivisors R] {p : Polynomial R},
  p.Monic →
    (Irreducible p ↔
      p ≠ 1 ∧ ∀ (f g : Polynomial R), f.Monic → g.Monic → f * g = p → g.natDegree ∉ Finset.Ioc 0 (p.natDegree / 2))
-- Lean.Elab.Binders
Lean.Elab.Term.elabForall : Lean.Elab.Term.TermElab
-- Mathlib.NumberTheory.LSeries.PrimesInAP
_private.Mathlib.NumberTheory.LSeries.PrimesInAP.0.ArithmeticFunction.vonMangoldt.F''_le : ∀ (p : Nat.Primes) (k : ℕ), ArithmeticFunction.vonMangoldt.F''✝ (p, k) ≤ 2 * (↑↑p)⁻¹ ^ (↑k + 3 / 2)
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.mkIso_hom_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S S' : CategoryTheory.Span Wₗ Wᵣ c c'} (e : S.apex ≅ S'.apex)
  (hₗ : autoParam (CategoryTheory.CategoryStruct.comp e.hom S'.l = S.l) CategoryTheory.Span.mkIso._auto_1)
  (hᵣ : autoParam (CategoryTheory.CategoryStruct.comp e.hom S'.r = S.r) CategoryTheory.Span.mkIso._auto_3),
  (CategoryTheory.Span.mkIso e hₗ hᵣ).hom.hom = e.hom
-- Lean.Data.Lsp.Basic
Lean.Lsp.RenameFile : Type
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_map : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (f : BoundedLatticeHom α β)
  (L : BooleanSubalgebra α), ↑(BooleanSubalgebra.map f L) = ⇑f '' ↑L
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `F` reflects isomorphisms, then `Cocones.functoriality F` reflects isomorphisms
as well.
 -/
CategoryTheory.Limits.Cocone.reflects_cocone_isomorphism : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] (F : CategoryTheory.Functor C D) [F.ReflectsIsomorphisms]
  (K : CategoryTheory.Functor J C), (CategoryTheory.Limits.Cocone.functoriality K F).ReflectsIsomorphisms
-- Mathlib.Topology.Perfect
PerfectSpace.mk : ∀ {α : Type u_1} [inst : TopologicalSpace α], Preperfect Set.univ → PerfectSpace α
-- Mathlib.Topology.Algebra.InfiniteSum.Group
hasProd_ite_div_hasProd : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f : β → α} {a : α} [L.LeAtTop] [inst_4 : DecidableEq β],
  HasProd f a L → ∀ (b : β), HasProd (fun n => if n = b then 1 else f n) (a / f b) L
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ≅ Y), f.unop.inv = f.inv.unop
-- Init.Data.Array.Lemmas
/-- Two arrays of arrays are equal iff their flattens coincide, as well as the sizes of the
arrays.  -/
Array.eq_iff_flatten_eq : ∀ {α : Type u_1} {xss₁ xss₂ : Array (Array α)},
  xss₁ = xss₂ ↔ xss₁.flatten = xss₂.flatten ∧ Array.map Array.size xss₁ = Array.map Array.size xss₂
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_zero : ∀ (R : Type u_3) (M : Type u_4) {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N], LinearMap.BilinMap.toQuadraticMap 0 = 0
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsNonloop.exists_mem_isBase : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsNonloop e → ∃ B, M.IsBase B ∧ e ∈ B
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasFilteredColimitsInd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.HasFilteredColimits (CategoryTheory.Ind C)
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.hom_inv_id_apply : ∀ {X Y : TopCat} (f : X ≅ Y) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom f.inv) ((CategoryTheory.ConcreteCategory.hom f.hom) x) = x
-- Mathlib.CategoryTheory.Sums.Basic
/-- `sum C D` gives the direct sum of two categories.
 -/
CategoryTheory.sum : (C : Type u₁) →
  [CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) → [CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Category.{max v₁ v₂, max u₂ u₁} (C ⊕ D)
-- Mathlib.Data.Set.Finite.Lattice
Set.map_finite_biSup : ∀ {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : FunLike F α β] [SupBotHomClass F α β] {s : Set ι},
  s.Finite → ∀ (f : F) (g : ι → α), f (⨆ x ∈ s, g x) = ⨆ x ∈ s, f (g x)
-- Mathlib.Algebra.Ring.Aut
RingAut.coe_one : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Add R], ⇑1 = id
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.ofOrderIso_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {X Y : C} {f : X ⟶ Y} [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  (c : CategoryTheory.TransfiniteCompositionOfShape J f) {J' : Type w'} [inst_5 : LinearOrder J'] [inst_6 : OrderBot J']
  [inst_7 : SuccOrder J'] [inst_8 : WellFoundedLT J'] (e : J' ≃o J), (c.ofOrderIso e).F = e.equivalence.functor.comp c.F
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- `Covariant` is useful to formulate succinctly statements about the interactions between an
action of a Type on another one and a relation on the acted-upon Type.

See the `CovariantClass` doc-string for its meaning.  -/
Covariant : (M : Type u_1) → (N : Type u_2) → (M → N → N) → (N → N → Prop) → Prop
-- Mathlib.Topology.Constructions
continuous_map_sInf : ∀ {α : Type u_5} [inst : TopologicalSpace α] {S : Set (Setoid α)} {s : Setoid α} (h : s ∈ S),
  Continuous (Setoid.map_sInf h)
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instNonUnitalRing : {R : Type u_1} → [NonUnitalRing R] → NonUnitalRing Rᵐᵒᵖ
-- Mathlib.Data.Sym.Sym2
/-- Map an unordered pair to a finite set.  -/
Sym2.toFinset : {α : Type u_1} → [DecidableEq α] → Sym2 α → Finset α
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.conjugate_self : ∀ {R : Type u_1} [inst : Semigroup R] [inst_1 : StarMul R] {x : R},
  IsSelfAdjoint x → ∀ {z : R}, IsSelfAdjoint z → IsSelfAdjoint (z * x * z)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHint.toInlayHintInfo : Lean.Elab.InlayHint → Lean.Elab.InlayHintInfo
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.homMk₁.match_1.eq_1 : ∀ (motive : Fin (1 + 1) → Sort u_1) (isLt : 0 < 1 + 1) (h_1 : (isLt : 0 < 1 + 1) → motive ⟨0, isLt⟩)
  (h_2 : (isLt : 1 < 1 + 1) → motive ⟨1, isLt⟩),
  (match ⟨0, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨1, isLt⟩ => h_2 isLt) =
    h_1 isLt
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffOn_snd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_9} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {s : Set (M × N)},
  ContMDiffOn (I.prod J) J n Prod.snd s
-- Mathlib.GroupTheory.Perm.Finite
Equiv.Perm.perm_symm_on_of_perm_on_finite : ∀ {α : Type u} {f : Equiv.Perm α} {p : α → Prop} [Finite { x // p x }],
  (∀ (x : α), p x → p (f x)) → ∀ {x : α}, p x → p ((Equiv.symm f) x)
-- Mathlib.Analysis.Calculus.Deriv.Mul
derivWithin_fun_const_smul : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} {R : Type u_2} [inst_3 : Monoid R]
  [inst_4 : DistribMulAction R F] [SMulCommClass 𝕜 R F] [ContinuousConstSMul R F] (c : R),
  DifferentiableWithinAt 𝕜 f s x → derivWithin (fun y => c • f y) s x = c • derivWithin f s x
-- Mathlib.Order.CompleteLattice.MulticoequalizerDiagram
_private.Mathlib.Order.CompleteLattice.MulticoequalizerDiagram.0.CompleteLattice.MulticoequalizerDiagram.multispanIndex.match_1.eq_1 : ∀ {ι : Type u_1} (motive : (CategoryTheory.Limits.MultispanShape.prod ι).L → Sort u_2) (i j : ι)
  (h_1 : (i j : ι) → motive (i, j)),
  (match (i, j) with
    | (i, j) => h_1 i j) =
    h_1 i j
-- Mathlib.Analysis.Calculus.TangentCone.Basic
uniqueDiffWithinAt_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : DivisionSemiring 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : TopologicalSpace 𝕜] [(nhdsWithin 0 {0}ᶜ).NeBot] [ContinuousSMul 𝕜 E] {x : E},
  UniqueDiffWithinAt 𝕜 Set.univ x
-- Mathlib.Topology.Category.Stonean.Basic
/-- The morphism from `presentation X` to `X` is an epimorphism.  -/
Profinite.presentation.epi_π : ∀ (X : Profinite), CategoryTheory.Epi (Profinite.presentation.π X)
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- In a compact space, the set of finite measures with mass at most `C` is compact.  -/
isCompact_setOfPred_finiteMeasure_le_of_compactSpace : ∀ (E : Type u_1) [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  [CompactSpace E] (C : NNReal), IsCompact {μ | μ.mass ≤ C}
-- Init.Data.List.SplitOn.Basic
_private.Init.Data.List.SplitOn.Basic.0.List.splitOnPTR.go : {α : Type u_1} → (α → Bool) → List α → Array α → Array (List α) → List (List α)
-- Mathlib.Control.Monad.Writer
WriterT.run_throw : ∀ {α ω : Type u} {M : Type u → Type u_2} {ε : Type u_1} [inst : MonadExceptOf ε M] (e : ε), (throw e).run = throw e
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.wideEqualizer.lift_ι : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)}
  [inst_1 : CategoryTheory.Limits.HasWideEqualizer f] [inst_2 : Nonempty J] {W : C} (k : W ⟶ X)
  (h : ∀ (j₁ j₂ : J), CategoryTheory.CategoryStruct.comp k (f j₁) = CategoryTheory.CategoryStruct.comp k (f j₂)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.wideEqualizer.lift k h)
      (CategoryTheory.Limits.wideEqualizer.ι f) =
    k
-- Init.Data.Vector.Lemmas
Vector.findSome?_mk : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Array α} (h : xs.size = n) (f : α → Option β),
  Vector.findSome? f (Vector.mk xs h) = Array.findSome? f xs
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instContinuousNeg : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : ContinuousNeg G],
  ContinuousNeg (SeparationQuotient G)
-- Mathlib.Data.Nat.Bitwise
Nat.bitwise_bit : ∀ {f : Bool → Bool → Bool},
  autoParam (f false false = false) Nat.bitwise_bit._auto_1 →
    ∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ),
      Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)
-- Mathlib.RingTheory.Finiteness.Subalgebra
Submodule.fg_unit : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (I : (Submodule R A)ˣ), (↑I).FG
-- Lean.DocString.Parser
/-- Parses one or more blocks.
 -/
Lean.Doc.Parser.blocks1 : Lean.Doc.Parser.BlockCtxt → Lean.Parser.ParserFn
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.implicitDeriv.eq_1 : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] (v : Polynomial A),
  Differential.implicitDeriv v = Differential.mapCoeffs + v • Derivation.restrictScalars ℤ Polynomial.derivative'
-- Mathlib.Data.List.Duplicate
List.Duplicate.elim_singleton : ∀ {α : Type u_1} {x y : α}, List.Duplicate x [y] → False
-- Mathlib.Data.List.Destutter
List.destutter'_cons_pos : ∀ {α : Type u_1} (l : List α) {R : α → α → Prop} [inst : DecidableRel R] {a b : α},
  R b a → List.destutter' R b (a :: l) = b :: List.destutter' R a l
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel.parts.sizeOf_spec : ∀ (p : Array Lean.Lsp.InlayHintLabelPart), sizeOf (Lean.Lsp.InlayHintLabel.parts p) = 1 + sizeOf p
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.inl_comp_binaryCoproductIso_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C (Type w)) (a : C)
  (x : F.obj a),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryCoproductIso F G).hom.app a))
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.coprod.inl.app a)) x) =
    Sum.inl x
-- Batteries.Data.Fin.Coding
/-- Decode `Unit` from `Fin 1`.  -/
Fin.decodeUnit : Fin 1 → Unit
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopEquiv_unitIso : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C],
  (CategoryTheory.MonoidalOpposite.mopEquiv C).unitIso = CategoryTheory.Iso.refl (CategoryTheory.Functor.id C)
-- Mathlib.Combinatorics.Matroid.Map
Matroid.mapEmbedding_isBasis_iff : ∀ {α : Type u_1} {β : Type u_2} {M : Matroid α} {f : α ↪ β} {I X : Set β},
  (M.mapEmbedding f).IsBasis I X ↔ M.IsBasis (⇑f ⁻¹' I) (⇑f ⁻¹' X) ∧ I ⊆ X ∧ X ⊆ Set.range ⇑f
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.instReprHeap.repr : {α : Type u_1} → [Repr α] → Batteries.BinomialHeap.Imp.Heap α → ℕ → Std.Format
-- Mathlib.Data.Seq.Defs
Stream'.Seq.terminates_nil : ∀ {α : Type u}, Stream'.Seq.nil.Terminates
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
isAssociatedPrime_iff_exists_injective_linearMap : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsNoetherianRing R], IsAssociatedPrime I M ↔ I.IsPrime ∧ ∃ f, Function.Injective ⇑f
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.of_field : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : Field K] [inst_2 : Algebra R K] [FaithfulSMul R K],
  (∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y) → IsFractionRing R K
-- Init.Data.UInt.Lemmas
USize.instIsLinearOrder : Std.IsLinearOrder USize
-- Mathlib.Data.Set.Sups
Set.singleton_infs : ∀ {α : Type u_2} [inst : SemilatticeInf α] {t : Set α} {a : α}, {a} ⊼ t = (fun b => a ⊓ b) '' t
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.mk.injEq : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (toPresentation : Algebra.Presentation R S ι σ) (map : σ → ι) (map_inj : Function.Injective map)
  (toPresentation_1 : Algebra.Presentation R S ι σ) (map_1 : σ → ι) (map_inj_1 : Function.Injective map_1),
  ({ toPresentation := toPresentation, map := map, map_inj := map_inj } =
      { toPresentation := toPresentation_1, map := map_1, map_inj := map_inj_1 }) =
    (toPresentation = toPresentation_1 ∧ map = map_1)
-- Init.Data.Int.Order
Int.sign_mul_natAbs : ∀ (a : ℤ), a.sign * ↑a.natAbs = a
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.isUniformInducing_toLp : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [Finite ι]
  [inst : (i : ι) → PseudoEMetricSpace (β i)], IsUniformInducing (WithLp.toLp p)
-- Init.Data.Range.Polymorphic.PRange
Std.Ric.instMembershipOfLE : {α : Type u} → [LE α] → Membership α (Std.Ric α)
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
/-- The functor `DerivedCategory.Plus.Qh : HomotopyCategory.Plus C ⥤ DerivedCategory.Plus C`
is induced by `DerivedCategory.Qh : HomotopyCategory C (.up ℤ) ⥤ DerivedCategory C`.  -/
DerivedCategory.Plus.QhCompιIsoιCompQh : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        DerivedCategory.Plus.Qh.comp DerivedCategory.Plus.ι ≅ (HomotopyCategory.Plus.ι C).comp DerivedCategory.Qh
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- Converts `PostconditionT m α` to `HetT m α`, preserving the postcondition property.
 -/
Std.Iterators.HetT.ofPostconditionT : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → Std.Iterators.PostconditionT m α → Std.Iterators.HetT m α
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
/-- A distinguished polynomial `g` induces a natural isomorphism `A[X] / (g) ≃ₐ[A] A⟦X⟧ / (g)`.  -/
Polynomial.IsDistinguishedAt.algEquivQuotient : {A : Type u_1} →
  [inst : CommRing A] →
    {g : Polynomial A} →
      {I : Ideal A} →
        g.IsDistinguishedAt I →
          [IsAdicComplete I A] → (Polynomial A ⧸ Ideal.span {g}) ≃ₐ[A] PowerSeries A ⧸ Ideal.span {↑g}
-- Std.Time.Format.Basic
/-- The part of a formatting string. A string is just a text and a modifier is in the format described in
the `Modifier` type.
 -/
Std.Time.FormatPart : Type
-- Init.GrindInstances.ToInt
Lean.Grind.instMulISizeSintNumBits : Lean.Grind.ToInt.Mul ISize (Lean.Grind.IntInterval.sint System.Platform.numBits)
-- Mathlib.Analysis.Complex.ReImTopology
TendstoUniformly.im : ∀ {α : Type u_1} {ι : Type u_2} {f : ι → α → ℂ} {p : Filter ι} {g : α → ℂ},
  TendstoUniformly f g p → TendstoUniformly (fun n x => (f n x).im) (fun y => (g y).im) p
-- Mathlib.CategoryTheory.ObjectProperty.Kernels
CategoryTheory.ObjectProperty.preservesCokernels_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.Limits.HasCokernels C] [P.IsClosedUnderCokernels]
  ⦃X Y : P.FullSubcategory⦄ (f : X ⟶ Y),
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) P.ι
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.id_apply : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} (f : U ⟶ U) (x : ↥U), f x = x
-- Mathlib.Topology.MetricSpace.Isometry
IsometryClass.ediam_image : ∀ {F : Type u_1} {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : FunLike F α β] [IsometryClass F α β] (f : F) (s : Set α), Metric.ediam (⇑f '' s) = Metric.ediam s
-- Lean.Elab.BuiltinNotation
Lean.Elab.Term.elabNoindex : Lean.Elab.Term.TermElab
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_ofList_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.HashMap.Raw.ofList l).getKey? k' = some k
-- Mathlib.Order.PartialSups
partialSups.eq_1 : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  (f : ι → α), partialSups f = { toFun := fun i => (Finset.Iic i).sup' ⋯ f, monotone' := ⋯ }
-- Mathlib.Algebra.Category.ModuleCat.Basic
ModuleCat.instLinear : {S : Type u} → [inst : CommRing S] → CategoryTheory.Linear S (ModuleCat S)
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernelRelations_relation : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (x : pres₂.R ⊕ ι),
  (pres₂.cokernelRelations data).relation x =
    match x with
    | Sum.inl r => pres₂.relation r
    | Sum.inr i => data.lift i
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_ofPred : ∀ {α : Type u_3} (p : α → Prop), {a | p a}ᶜ = {a | ¬p a}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldRev_eq_foldr_keys : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {f : δ → α → δ} {init : δ},
  Std.DHashMap.Raw.Internal.foldRev (fun d a x => f d a) init ↑m = List.foldr (fun a b => f b a) init (↑m).keys
-- Mathlib.Data.Setoid.Partition
Setoid.sUnion_classes : ∀ {α : Type u_1} (r : Setoid α), ⋃₀ r.classes = Set.univ
-- Mathlib.Data.Part
Part.inv_def : ∀ {α : Type u_1} [inst : Inv α] (a : Part α), a⁻¹ = Part.map (fun x => x⁻¹) a
-- Mathlib.FieldTheory.PurelyInseparable.Basic
IsPurelyInseparable.injective_restrictDomain : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [IsPurelyInseparable F E]
  (R : Type u_1) (L : Type u_2) [inst_4 : CommSemiring R] [inst_5 : Algebra R F] [inst_6 : Algebra R E]
  [inst_7 : CommRing L] [IsReduced L] [inst_9 : Algebra R L] [inst_10 : IsScalarTower R F E],
  Function.Injective (AlgHom.domRestrict F)
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.quotientPathsTo_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C]
  {X Y : CategoryTheory.Quotient (CategoryTheory.pathsHomRel C)} (hf : X ⟶ Y),
  (CategoryTheory.quotientPathsTo C).map hf = Quot.liftOn hf (fun f => CategoryTheory.composePath f) ⋯
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.toCompleteSpace : ∀ {A : Type u_1} [self : NonUnitalCStarAlgebra A], CompleteSpace A
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- Construct an isomorphism in the over category given isomorphisms of the objects whose forward
direction gives a commutative triangle.
 -/
CategoryTheory.Over.isoMk : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} →
      {f g : CategoryTheory.Over X} →
        (hl : f.left ≅ g.left) →
          autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) CategoryTheory.Over.isoMk._auto_1 →
            (f ≅ g)