mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.CompactlyGenerated.Basic
/-- This property is sometimes referred to as `α` being upper continuous.  -/
DirectedOn.sSup_inf_eq : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {a : α} {s : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) s → sSup s ⊓ a = ⨆ b ∈ s, b ⊓ a
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.mk : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] →
          [inst_2 : AddGroup G] →
            {S : AddGroupExtension N E G} →
              (toAddMonoidHom : G →+ E) → Function.RightInverse (↑toAddMonoidHom).toFun ⇑S.rightHom → S.Splitting
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_modifyGet_StateT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ α : Type u}
  (f : σ → α × σ) (post : α → σ → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel (fun s => post (f s).1 (f s).2) (Std.Internal.Do.wp (MonadStateOf.modifyGet f) post epost)
-- Mathlib.Topology.Irreducible
preirreducibleSpace_iff : ∀ (X : Type u_3) [inst : TopologicalSpace X], PreirreducibleSpace X ↔ IsPreirreducible Set.univ
-- Init.SimpLemmas
Bool.not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b
-- Init.Core
instLawfulBEq : ∀ {α : Type u_1} [inst : DecidableEq α], LawfulBEq α
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.sphere_subset_box : ∀ {n d k : ℕ}, Behrend.sphere n d k ⊆ Behrend.box n d
-- Lean.ProjFns
Lean.AuxParentProjectionInfo.mk : ℕ → Bool → Lean.AuxParentProjectionInfo
-- Mathlib.Order.CountableSupClosed
subset_countableInfClosure : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α], s ⊆ countableInfClosure s
-- Lean.Expr
/-- Local instance binder annotation, e.g., `[Decidable α]`  -/
Lean.BinderInfo.instImplicit : Lean.BinderInfo
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.le_weightedOrder_map : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f : MvPowerSeries σ R} {S : Type u_3}
  [inst_1 : Semiring S] (φ : R →+* S),
  MvPowerSeries.weightedOrder w f ≤ MvPowerSeries.weightedOrder w ((MvPowerSeries.map φ) f)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The binary coproduct functor.  -/
CategoryTheory.Limits.coprod.functor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryCoproducts C] → CategoryTheory.Functor C (CategoryTheory.Functor C C)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.eq_1 : ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize✝ ByteArray.utf8DecodeChar?.FirstByte.invalid = 0
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorComm_inv_app_of_add_eq_zero : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (m n : A) (hmn : m + n = 0) (X : C),
  (CategoryTheory.shiftFunctorComm C m n).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C n m ⋯).hom.app X)
      ((CategoryTheory.shiftFunctorCompIsoId C m n hmn).inv.app X)
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The composition of the three left maps in the oplax associativity hexagon.
 -/
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPre F) →
                (CategoryTheory.MonoidalCategory.curriedTensorPostPost F ⟶
                  CategoryTheory.MonoidalCategory.curriedTensorPrePre' F)
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instDecidableLE : {n : ℕ} → DecidableLE (BitVec n)
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.normal_unop : ∀ {G : Type u_2} [inst : Group G] {H : Subgroup Gᵐᵒᵖ}, H.unop.Normal ↔ H.Normal
-- Init.Data.Int.Order
Int.add_le_add_iff_left : ∀ {b c : ℤ} (a : ℤ), a + b ≤ a + c ↔ b ≤ c
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.le_op_iff : ∀ {M : Type u_2} [inst : MulOneClass M] {S₁ : Submonoid Mᵐᵒᵖ} {S₂ : Submonoid M}, S₁ ≤ S₂.op ↔ S₁.unop ≤ S₂
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- Barycentric coordinates as an affine map.  -/
AffineBasis.coords : {ι : Type u_1} →
  {k : Type u_5} →
    {V : Type u_6} →
      {P : Type u_7} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] → [inst_2 : Ring k] → [inst_3 : Module k V] → AffineBasis ι k P → P →ᵃ[k] ι → k
-- Mathlib.Algebra.GroupWithZero.Subgroup
AddSubgroup.pointwise_smul_le_pointwise_smul_iff₀ : ∀ {G₀ : Type u_1} {A : Type u_4} [inst : GroupWithZero G₀] [inst_1 : AddGroup A] [inst_2 : DistribMulAction G₀ A]
  {S T : AddSubgroup A} {a : G₀}, a ≠ 0 → (a • S ≤ a • T ↔ S ≤ T)
-- Mathlib.Data.Semiquot
/-- Assertion of non-emptiness via `Trunc`  -/
Semiquot.val : {α : Type u_1} → (self : Semiquot α) → Trunc ↑self.s
-- Mathlib.Computability.TuringDegree
TuringEquivalent.equivalence : Equivalence TuringEquivalent
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.mk.inj : ∀ {date : Std.Time.PlainDate} {time : Std.Time.PlainTime} {date_1 : Std.Time.PlainDate} {time_1 : Std.Time.PlainTime},
  { date := date, time := time } = { date := date_1, time := time_1 } → date = date_1 ∧ time = time_1
-- Init.Data.String.Lemmas.Pattern.Basic
/-- Type class for the condition that the empty string is not a match. This is necessary for the theory to
work out as there is just no reasonable notion of searching that works for the empty string that is
still specific enough to yield reasonably strong correctness results for operations based on
searching.
 -/
String.Slice.Pattern.Model.StrictPatternModel : {ρ : Type} → (pat : ρ) → [String.Slice.Pattern.Model.PatternModel pat] → Prop
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.IterM.toListRev_uLift : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [inst : Std.Iterator α m β]
  [inst_1 : Monad m] [inst_2 : Monad n] {it : Std.IterM m β} [inst_3 : MonadLiftT m (Std.Iterators.ULiftT n)]
  [Std.Iterators.Finite α m] [LawfulMonad m] [LawfulMonad n] [LawfulMonadLiftT m (Std.Iterators.ULiftT n)],
  (it.uLift n).toListRev = (fun l => List.map ULift.up l.down) <$> (monadLift it.toListRev).run
-- Mathlib.Algebra.Module.Injective
Module.Baer.ExtensionOf.mk.injEq : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q] {M : Type u_1}
  {N : Type u_2} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module R N]
  {i : M →ₗ[R] N} {f : M →ₗ[R] Q} (toLinearPMap : N →ₗ.[R] Q) (le : i.range ≤ toLinearPMap.domain)
  (is_extension : ∀ (m : M), f m = ↑toLinearPMap ⟨i m, ⋯⟩) (toLinearPMap_1 : N →ₗ.[R] Q)
  (le_1 : i.range ≤ toLinearPMap_1.domain) (is_extension_1 : ∀ (m : M), f m = ↑toLinearPMap_1 ⟨i m, ⋯⟩),
  ({ toLinearPMap := toLinearPMap, le := le, is_extension := is_extension } =
      { toLinearPMap := toLinearPMap_1, le := le_1, is_extension := is_extension_1 }) =
    (toLinearPMap = toLinearPMap_1)
-- Init.Data.UInt.Bitwise
UInt32.toFin_xor : ∀ (a b : UInt32), (a ^^^ b).toFin = a.toFin ^^^ b.toFin
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_addConstC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p : Lean.Grind.CommRing.Poly) (k : ℤ),
  Lean.Grind.CommRing.Poly.denote ctx (p.addConstC k c) = Lean.Grind.CommRing.Poly.denote ctx p + ↑k
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
nndist_toMul : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] (a b : Additive X),
  nndist (Additive.toMul a) (Additive.toMul b) = nndist a b
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.insertₘ : {α : Type u} →
  {β : α → Type v} →
    [BEq α] → [Hashable α] → Std.DHashMap.Internal.Raw₀ α β → (a : α) → β a → Std.DHashMap.Internal.Raw₀ α β
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrangeRestrict.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M] {N : Type u_5} [inst_1 : AddZeroClass N] (f : M →+ N),
  f.mrangeRestrict = f.codRestrict (AddMonoidHom.mrange f) ⋯
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.le_cof_map_of_isNormal : ∀ {f : Ordinal.{u_1} → Ordinal.{u_1}}, Order.IsNormal f → ∀ (a : Ordinal.{u_1}), a.cof ≤ (f a).cof
-- Mathlib.AlgebraicGeometry.Sites.EtalePoint
AlgebraicGeometry.Scheme.isConservativeFamilyOfPoints_pointSmallEtale' : ∀ (S : AlgebraicGeometry.Scheme),
  (CategoryTheory.ObjectProperty.ofObj fun s =>
      AlgebraicGeometry.Scheme.pointSmallEtale
        ((AlgebraicGeometry.Scheme.SpecToEquivOfField (SeparableClosure ↑(S.residueField s)) S).invFun
          ⟨s,
            CommRingCat.ofHom
              (algebraMap (↑(S.residueField s)) (SeparableClosure ↑(S.residueField s)))⟩)).IsConservativeFamilyOfPoints
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.indepFun_iff_indepSet_preimage : ∀ {α : Type u_1} {Ω : Type u_2} {β : Type u_4} {β' : Type u_5} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {f : Ω → β} {g : Ω → β'} {mβ : MeasurableSpace β}
  {mβ' : MeasurableSpace β'} [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  Measurable f →
    Measurable g →
      (ProbabilityTheory.Kernel.IndepFun f g κ μ ↔
        ∀ (s : Set β) (t : Set β'),
          MeasurableSet s → MeasurableSet t → ProbabilityTheory.Kernel.IndepSet (f ⁻¹' s) (g ⁻¹' t) κ μ)
-- Mathlib.Geometry.Euclidean.Congruence
EuclideanGeometry.triangle_congruent_iff_dist_eq : ∀ {P₁ : Type u_4} {P₂ : Type u_5} [inst : MetricSpace P₁] [inst_1 : MetricSpace P₂] {t₁ : Fin 3 → P₁} {t₂ : Fin 3 → P₂},
  Congruent t₁ t₂ ↔ ∀ (i j : Fin 3), dist (t₁ i) (t₁ j) = dist (t₂ i) (t₂ j)
-- Mathlib.Logic.Equiv.Defs
Equiv.self_trans_symm : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.trans e.symm = Equiv.refl α
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.foldrTR.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → β → β) (init : β) (l : List α),
  List.foldrTR f init l = Array.foldr f init l.toArray
-- Mathlib.Algebra.Category.GrpWithZero
GrpWithZero.Iso.mk_hom : ∀ {α β : GrpWithZero} (e : α.carrier ≃* β.carrier),
  (GrpWithZero.Iso.mk e).hom = GrpWithZero.ofHom (MonoidWithZeroHom.ofClass e)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instIsOverTower_2 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C)
  [inst_1 : CategoryTheory.CanonicallyOverClass X Y] [inst_2 : CategoryTheory.OverClass Y S],
  CategoryTheory.IsOverTower X Y S
-- Init.Data.Order.Lemmas
Std.le_antisymm : ∀ {α : Type u} [inst : LE α] [Std.Antisymm fun x1 x2 => x1 ≤ x2] {a b : α}, a ≤ b → b ≤ a → a = b
-- Mathlib.LinearAlgebra.QuadraticForm.Basis
QuadraticMap.toBilinHom_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : LinearOrder ι] [inst_1 : CommRing R]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N] (S : Type u_5)
  [inst_6 : CommSemiring S] [inst_7 : Algebra S R] [inst_8 : Module S N] [inst_9 : IsScalarTower S R N]
  (bm : Module.Basis ι R M) (Q : QuadraticMap R M N), (QuadraticMap.toBilinHom S bm) Q = Q.toBilin bm
-- Std.Async.UDP
/-- Enables or disables multicast loopback for the UDP socket.
 -/
Std.Async.UDP.Socket.setMulticastLoop : Std.Async.UDP.Socket → Bool → IO Unit
-- Mathlib.Analysis.SpecificLimits.Basic
/-- For any positive `ε`, define on an encodable type a positive sequence with sum less than `ε`  -/
posSumOfEncodable : {ε : ℝ} → 0 < ε → (ι : Type u_4) → [Encodable ι] → { ε' // (∀ (i : ι), 0 < ε' i) ∧ ∃ c, HasSum ε' c ∧ c ≤ ε }
-- Mathlib.Algebra.GroupWithZero.Opposite
AddOpposite.instMulZeroClass : {α : Type u_1} → [MulZeroClass α] → MulZeroClass αᵃᵒᵖ
-- Mathlib.Order.Max
isMax_ofDual_iff : ∀ {α : Type u_1} [inst : LE α] {a : αᵒᵈ}, IsMax (OrderDual.ofDual a) ↔ IsMin a
-- Init.Meta.Defs
Lean.instQuoteNameMkStr1 : Lean.Quote Lean.Name
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.instAlgebraExtension : (k : Type u_1) →
  [inst : Field k] →
    [Finite k] →
      (p : ℕ) →
        [inst_2 : Fact (Nat.Prime p)] →
          [inst_3 : CharP k p] → (n : ℕ) → [NeZero n] → Algebra k (FiniteField.Extension k p n)
-- Lean.Meta.Tactic.AuxLemma
Lean.Meta.AuxLemmas.mk.inj : ∀ {lemmas lemmas_1 : Lean.PHashMap Lean.Meta.AuxLemmaKey (Lean.Name × List Lean.Name)},
  { lemmas := lemmas } = { lemmas := lemmas_1 } → lemmas = lemmas_1
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.contSupp.match_1.eq_3 : ∀ (motive : Turing.PartrecToTM2.Cont' → Sort u_1) (f : Turing.ToPartrec.Code) (k : Turing.PartrecToTM2.Cont')
  (h_1 : (fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.cons₁ fs k))
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive k.cons₂)
  (h_3 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.comp f k))
  (h_4 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (Turing.PartrecToTM2.Cont'.fix f k))
  (h_5 : Unit → motive Turing.PartrecToTM2.Cont'.halt),
  (match Turing.PartrecToTM2.Cont'.comp f k with
    | Turing.PartrecToTM2.Cont'.cons₁ fs k => h_1 fs k
    | k.cons₂ => h_2 k
    | Turing.PartrecToTM2.Cont'.comp f k => h_3 f k
    | Turing.PartrecToTM2.Cont'.fix f k => h_4 f k
    | Turing.PartrecToTM2.Cont'.halt => h_5 ()) =
    h_3 f k
-- Mathlib.Topology.Order.ScottTopology
/-- The Scott topology.

It is defined as the join of the topology of upper sets and the Scott-Hausdorff topology.  -/
Topology.scott : (α : Type u_3) → Set (Set α) → [Preorder α] → TopologicalSpace α
-- Mathlib.Tactic.Linter.TextBased
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.ErrorContext.mk.injEq : ∀ (error : Mathlib.Linter.TextBased.StyleError✝) (lineNumber : ℕ) (path : System.FilePath)
  (error_1 : Mathlib.Linter.TextBased.StyleError✝) (lineNumber_1 : ℕ) (path_1 : System.FilePath),
  ({ error := error, lineNumber := lineNumber, path := path } =
      { error := error_1, lineNumber := lineNumber_1, path := path_1 }) =
    (error = error_1 ∧ lineNumber = lineNumber_1 ∧ path = path_1)
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.inter_compl : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), s ∩ sᶜ = ∅
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.map_den : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] {𝒜 : ι → σ} {B : Type u_4} {τ : Type u_5} [inst_3 : CommRing B] [inst_4 : SetLike τ B]
  [inst_5 : AddSubgroupClass τ B] {ℬ : ι → τ} (f : 𝒜 →+*ᵍ ℬ) {W₁ : Submonoid A} {W₂ : Submonoid B}
  (hw : W₁ ≤ Submonoid.comap f W₂) (c : HomogeneousLocalization.NumDenSameDeg 𝒜 W₁),
  (HomogeneousLocalization.NumDenSameDeg.map f hw c).den = (f.gradedAddHom c.deg) c.den
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Make `ArchimedeanClass.subsemigroup` a subgroup by assigning
s = ⊤ with a junk value ⊥.  -/
ArchimedeanClass.addSubgroup : {M : Type u_1} →
  [inst : AddCommGroup M] →
    [inst_1 : LinearOrder M] → [inst_2 : IsOrderedAddMonoid M] → UpperSet (ArchimedeanClass M) → AddSubgroup M
-- Init.Data.String.Lemmas.Order
String.Slice.Pos.slice_le_slice_iff : ∀ {s : String.Slice} {p₀ p₁ q r : s.Pos} {h₁ : p₀ ≤ q} {h₁' : p₀ ≤ r} {h₂ : q ≤ p₁} {h₂' : r ≤ p₁},
  q.slice p₀ p₁ h₁ h₂ ≤ r.slice p₀ p₁ h₁' h₂' ↔ q ≤ r
-- Mathlib.Order.OmegaCompletePartialOrder
/-- The identity as a continuous function.  -/
OmegaCompletePartialOrder.ContinuousHom.id : {α : Type u_2} → [inst : OmegaCompletePartialOrder α] → α →𝒄 α
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.isClique_empty : ∀ {α : Type u_1} {G : SimpleGraph α}, G.IsClique ∅
-- Mathlib.Data.List.Infix
List.tails_append : ∀ {α : Type u_1} (s t : List α), (s ++ t).tails = List.map (fun l => l ++ t) s.tails ++ t.tails.tail
-- Init.Data.UInt.BasicAux
/-- Converts a natural number to a 64-bit unsigned integer, wrapping on overflow.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Nat.toUInt64 5 = 5`
* `Nat.toUInt64 65539 = 65539`
* `Nat.toUInt64 4_294_967_299 = 4_294_967_299`
* `Nat.toUInt64 18_446_744_073_709_551_620 = 4`
 -/
Nat.toUInt64 : ℕ → UInt64
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Presieve.Arrows.FirstObj.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {I : Type t}
  [inst_1 : Small.{w, t} I] (X : I → C) (z₁ z₂ : CategoryTheory.Equalizer.Presieve.Arrows.FirstObj P X),
  (∀ (i : I),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i)) z₁ =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π (fun i => P.obj (Opposite.op (X i))) i)) z₂) →
    z₁ = z₂
-- Mathlib.Data.Int.Bitwise
_private.Mathlib.Data.Int.Bitwise.0.Int.div2.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.ofNat n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_1 n
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Pre.ofScalar.inj : ∀ {R : Type u_1} {X : Type u_2} {a a_1 : R}, FreeAlgebra.Pre.ofScalar a = FreeAlgebra.Pre.ofScalar a_1 → a = a_1
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
/-- `SimplexCategoryGenRel.mk` is the main constructor for objects of `SimplexCategoryGenRel`.  -/
SimplexCategoryGenRel.mk : ℕ → SimplexCategoryGenRel
-- Mathlib.Analysis.Normed.Ring.Basic
norm_commutator_units_sub_one_le : ∀ {α : Type u_2} [inst : SeminormedRing α] (a b : αˣ),
  ‖↑(a * b * a⁻¹ * b⁻¹) - 1‖ ≤ 2 * ‖↑a⁻¹‖ * ‖↑b⁻¹‖ * ‖↑a - 1‖ * ‖↑b - 1‖
-- Mathlib.RingTheory.IntegralDomain
Finset.exists_eq_pow_of_mul_eq_pow_of_coprime : ∀ {ι : Type u_2} {R : Type u_3} [inst : CommSemiring R] [GCDMonoid R] [Subsingleton Rˣ] {n : ℕ} {c : R} {s : Finset ι}
  {f : ι → R}, (∀ i ∈ s, ∀ j ∈ s, i ≠ j → IsCoprime (f i) (f j)) → ∏ i ∈ s, f i = c ^ n → ∀ i ∈ s, ∃ d, f i = d ^ n
-- Mathlib.RepresentationTheory.Equiv
Representation.leftRegularMapEquiv_symm_single : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {k : Type u} [inst_2 : CommSemiring k]
  [inst_3 : Module k V] (σ : Representation k G V) (g : G) (v : V),
  (σ.leftRegularMapEquiv.symm v) (MonoidAlgebra.single g 1) = (σ g) v
-- Init.Data.Int.DivMod.Bootstrap
Int.emod_self : ∀ {a : ℤ}, a % a = 0
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If `x` is not in the closure of `s`, then `f` has any derivative at `x` within `s`,
as this statement is empty.  -/
HasFDerivWithinAt.of_notMem_closure : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E},
  x ∉ closure s → HasFDerivWithinAt f f' s x
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeleton_zero : ∀ (X : SSet), X.skeleton 0 = ⊥
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.mul_mul_div : ∀ {α : Type u} [inst : DivisionMonoid α] {b : α} (a : α), IsUnit b → a * b * (1 / b) = a
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.bestLabelForDecl? : Lean.Elab.ContextInfo → Lean.Name → Lean.Name → Bool → Lean.Server.Completion.M✝ (Option Lean.Name)
-- Mathlib.Lean.Elab.InfoTree
/-- Gets the local context, and the expected type of the `Info`.
Handles `TacticInfo`s (looking at the first goal), `TermInfo`s, and `PartialTermInfo`s.
Does not get the metavariable context; assumes that the caller has accumulated an ambient
`ContextInfo` at this point which is sufficient.  -/
Lean.Elab.Info.getLCtx? : Lean.Elab.Info → Option (Lean.LocalContext × Option Lean.Expr)
-- Mathlib.Algebra.Category.BoolRing
/-- Turn a morphism in `BoolRing` back into a `RingHom`.  -/
BoolRing.Hom.hom : {X Y : BoolRing} → X.Hom Y → ↑X →+* ↑Y
-- Mathlib.Algebra.Category.Grp.EpiMono
AddCommGrpCat.mono_iff_ker_eq_bot : ∀ {A B : AddCommGrpCat} (f : A ⟶ B), CategoryTheory.Mono f ↔ (AddCommGrpCat.Hom.hom f).ker = ⊥
-- Mathlib.MeasureTheory.Covering.VitaliFamily
/-- **Alias** of `VitaliFamily.FineSubfamilyOn.measure_sdiff_biUnion`. -/
VitaliFamily.FineSubfamilyOn.measure_diff_biUnion : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  {v : VitaliFamily μ} {f : X → Set (Set X)} {s : Set X} (h : v.FineSubfamilyOn f s),
  μ (s \ ⋃ p ∈ h.index, h.covering p) = 0
-- Mathlib.Order.Bounds.Image
BddAbove.bddAbove_image2_of_bddBelow : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → BddAbove s → BddBelow t → BddAbove (Set.image2 f s t)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instRespectsIsoColimitsOfShape : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type u_1)
  [inst_1 : CategoryTheory.Category.{v_1, u_1} J], (W.colimitsOfShape J).RespectsIso
-- Mathlib.Data.Finsupp.AList
Finsupp.toAList.eq_1 : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (f : α →₀ M),
  f.toAList = { entries := List.map Prod.toSigma f.graph.toList, nodupKeys := ⋯ }
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_toAddSubgroup : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), ↑s.toAddSubgroup = ↑s
-- Mathlib.Order.Filter.Germ.OrderedMonoid
Filter.Germ.instCanonicallyOrderedAdd : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} [inst : Add β] [inst_1 : LE β] [CanonicallyOrderedAdd β],
  CanonicallyOrderedAdd (l.Germ β)
-- Lean.Environment
_private.Lean.Environment.0.Lean.finalizeImport.unsafe_11 : Lean.Environment → NonScalar
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.convs.eq_1 : ∀ {K : Type u_2} [inst : DivisionRing K] (g : GenContFract K) (n : ℕ), g.convs n = g.nums n / g.dens n
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.mapRingHom.congr_simp : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {R' : Type u_6} {S' : Type u_7} {T' : Type u_8} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring T] [inst_3 : Algebra R S] [inst_4 : Algebra R T]
  [inst_5 : CommSemiring R'] [inst_6 : CommSemiring S'] [inst_7 : CommSemiring T'] [inst_8 : Algebra R' S']
  [inst_9 : Algebra R' T'] (fR fR_1 : R →+* R') (e_fR : fR = fR_1) (fS fS_1 : S →+* S') (e_fS : fS = fS_1)
  (fT fT_1 : T →+* T') (e_fT : fT = fT_1) (HS : fS.comp (algebraMap R S) = (algebraMap R' S').comp fR)
  (HT : fT.comp (algebraMap R T) = (algebraMap R' T').comp fR),
  Algebra.TensorProduct.mapRingHom fR fS fT HS HT = Algebra.TensorProduct.mapRingHom fR_1 fS_1 fT_1 ⋯ ⋯
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_of_getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {a a' : α}, (↑m).WF → m.getKey? a = some a' → m.contains a' = true
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- A factorisation of a morphism `f = e ≫ m`, with `m` monic.  -/
CategoryTheory.Limits.MonoFactorisation.I : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Limits.MonoFactorisation f → C
-- Mathlib.Data.List.MinMax
List.minimum_eq_top : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLT α] {l : List α}, l.minimum = ⊤ ↔ l = []