mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.combine.match_1.eq_1 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) (p₂ : Lean.Grind.Linarith.Poly)
  (h_1 : (p₂ : Lean.Grind.Linarith.Poly) → motive Lean.Grind.Linarith.Poly.nil p₂)
  (h_2 : (p₁ : Lean.Grind.Linarith.Poly) → motive p₁ Lean.Grind.Linarith.Poly.nil)
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Lean.Grind.Linarith.Var) →
        (p₁ : Lean.Grind.Linarith.Poly) →
          (a₂ : ℤ) →
            (x₂ : Lean.Grind.Linarith.Var) →
              (p₂ : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a₁ x₁ p₁) (Lean.Grind.Linarith.Poly.add a₂ x₂ p₂)),
  (match Lean.Grind.Linarith.Poly.nil, p₂ with
    | Lean.Grind.Linarith.Poly.nil, p₂ => h_1 p₂
    | p₁, Lean.Grind.Linarith.Poly.nil => h_2 p₁
    | Lean.Grind.Linarith.Poly.add a₁ x₁ p₁, Lean.Grind.Linarith.Poly.add a₂ x₂ p₂ => h_3 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_1 p₂
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic.0.CategoryTheory.WithInitial.id.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → Sort u_2) (a : C)
  (h_1 : (a : C) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of a with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_1 a
-- Mathlib.Topology.Separation.Hausdorff
IsCompact.preimage_continuous : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [CompactSpace X] [T2Space Y]
  {f : X → Y} {s : Set Y}, IsCompact s → Continuous f → IsCompact (f ⁻¹' s)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.lift_unique : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (f : M →ₗ[R] A) (cond : ∀ (m : M), f m * f m = 0)
  (g : ExteriorAlgebra R M →ₐ[R] A), g.toLinearMap ∘ₗ ExteriorAlgebra.ι R = f ↔ g = (ExteriorAlgebra.lift R) ⟨f, cond⟩
-- Init.Data.Option.Basic
Option.map_none : ∀ {α : Type u_1} {β : Type u_2} (f : α → β), Option.map f none = none
-- Init.Data.Range.Polymorphic.PRange
Std.Rii.mk : {α : Type u} → Std.Rii α
-- Init.Data.String.Basic
String.Slice.startInclusive_slice : ∀ {s : String.Slice} {newStart newEnd : s.Pos} {h : newStart ≤ newEnd},
  (s.slice newStart newEnd h).startInclusive = newStart.str
-- Mathlib.Data.Bool.Count
List.IsChain.two_mul_count_bool_le_length_add_one : ∀ {l : List Bool}, List.IsChain (fun x1 x2 => x1 ≠ x2) l → ∀ (b : Bool), 2 * List.count b l ≤ l.length + 1
-- Init.Data.SInt.Lemmas
Int64.toInt_eq_toNatClampNeg : ∀ {a : Int64}, 0 ≤ a → a.toInt = ↑a.toNatClampNeg
-- Init.MetaTypes
/-- If true (default: true), descend into forall/lambda/let bodies when extracting. Only relevant when `descend` is true.  -/
Lean.Meta.ExtractLetsConfig.underBinder : Lean.Meta.ExtractLetsConfig → Bool
-- Mathlib.Data.Set.Card
Set.one_lt_ncard_iff_nontrivial : ∀ {α : Type u_1} {s : Set α} [Finite ↑s], 1 < s.ncard ↔ s.Nontrivial
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.fractionalIdealLatticeBasis.eq_1 : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K]
  (I : (FractionalIdeal (nonZeroDivisors (NumberField.RingOfIntegers K)) K)ˣ),
  NumberField.mixedEmbedding.fractionalIdealLatticeBasis K I =
    (have this := ⋯;
        Module.Basis.mk ⋯ ⋯).reindex
      (Fintype.equivOfCardEq ⋯)
-- Init.Data.Iterators.Basic
_private.Init.Data.Iterators.Basic.0.Std.IterStep.successor.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Std.IterStep α β → Sort u_3) (it : α) (out : β)
  (h_1 : (it : α) → (out : β) → motive (Std.IterStep.yield it out)) (h_2 : (it : α) → motive (Std.IterStep.skip it))
  (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.yield it out with
    | Std.IterStep.yield it out => h_1 it out
    | Std.IterStep.skip it => h_2 it
    | Std.IterStep.done => h_3 ()) =
    h_1 it out
-- Mathlib.RingTheory.AdjoinRoot
/-- The elements `1, root g, ..., root g ^ (d - 1)` form a basis for `AdjoinRoot g`,
where `g` is a monic polynomial of degree `d`.  -/
AdjoinRoot.powerBasisAux' : {R : Type u_1} → [inst : CommRing R] → {g : Polynomial R} → g.Monic → Module.Basis (Fin g.natDegree) R (AdjoinRoot g)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapGrp_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal], e.mapGrp.inverse = e.inverse.mapGrp
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.uniformity_basis_dist_le_inv_nat_pos : ∀ {α : Type u} [inst : PseudoMetricSpace α],
  (uniformity α).HasBasis (fun n => 0 < n) fun n => {p | dist p.1 p.2 ≤ 1 / ↑n}
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- A category `C` is said to have exact colimits of shape `J` provided that colimits of shape `J`
exist and are exact (in the sense that they preserve finite limits).
 -/
CategoryTheory.HasExactColimitsOfShape : (J : Type u') →
  [inst : CategoryTheory.Category.{v', u'} J] →
    (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasColimitsOfShape J C] → Prop
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated
AlgebraicGeometry.quasiCompact_iff_compactSpace : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [QuasiSeparatedSpace ↥Y] [CompactSpace ↥Y],
  AlgebraicGeometry.QuasiCompact f ↔ CompactSpace ↥X
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_maxKey?_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α} {v : β k}
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → (Std.Internal.List.maxKey? (Std.Internal.List.insertEntry k v l)).isSome = true
-- Mathlib.GroupTheory.Congruence.Defs
/-- Coercion from a type with an addition to its quotient by an additive congruence
relation  -/
AddCon.instCoeTCQuotient : {M : Type u_1} → [inst : Add M] → (c : AddCon M) → CoeTC M c.Quotient
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.hausdorffEDist_closure`.

---

The Hausdorff edistance between sets or their closures is the same.  -/
EMetric.hausdorffEdist_closure : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {s t : Set α},
  Metric.hausdorffEDist (closure s) (closure t) = Metric.hausdorffEDist s t
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} (K : CategoryTheory.Limits.Multifork I) (b : J.R),
  K.π.app (CategoryTheory.Limits.WalkingMulticospan.right b) =
    CategoryTheory.CategoryStruct.comp (K.ι (J.fst b)) (I.fst b)
-- Mathlib.Algebra.WithConv
WithConv.toEquiv_addEquiv : ∀ {A : Type u_2} [inst : AddMonoid A], ↑(WithConv.addEquiv A) = WithConv.equiv A
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.sdiv_eq.match_1.eq_2 : ∀ (motive : Bool → Bool → Sort u_1) (h_1 : Unit → motive false false) (h_2 : Unit → motive false true)
  (h_3 : Unit → motive true false) (h_4 : Unit → motive true true),
  (match false, true with
    | false, false => h_1 ()
    | false, true => h_2 ()
    | true, false => h_3 ()
    | true, true => h_4 ()) =
    h_2 ()
-- Mathlib.NumberTheory.Chebyshev
_private.Mathlib.NumberTheory.Chebyshev.0.Chebyshev.psi_pow_eq_sum_b : ∀ (x : ℝ) (n : ℕ), 0 ≤ x → ∃ M, ∀ N ≥ M, Chebyshev.psi (x ^ (↑n)⁻¹) = ∑ k ∈ Finset.Icc 1 N, Chebyshev.b✝ x (n * k)
-- Mathlib.Algebra.Algebra.Prod
AlgEquiv.uniqueProd_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Unique B] (x : A), AlgEquiv.uniqueProd.symm x = (0, x)
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.natDegree_X_pow : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R] (n : ℕ), (Polynomial.X ^ n).natDegree = n
-- Mathlib.Order.Heyting.Hom
/-- Copy of a `CoheytingHom` with a new `toFun` equal to the old one. Useful to fix definitional
equalities.  -/
CoheytingHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : CoheytingAlgebra α] →
      [inst_1 : CoheytingAlgebra β] → (f : CoheytingHom α β) → (f' : α → β) → f' = ⇑f → CoheytingHom α β
-- Mathlib.RingTheory.MvPowerSeries.Order
MvPowerSeries.weightedOrder_one : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) [Nontrivial R], MvPowerSeries.weightedOrder w 1 = 0
-- Init.Data.List.Erase
List.erase_replicate_self : ∀ {α : Type u_1} [inst : BEq α] {n : ℕ} [LawfulBEq α] {a : α}, (List.replicate n a).erase a = List.replicate (n - 1) a
-- Mathlib.CategoryTheory.Subfunctor.SubmonoidFunctor
/-- A submonoid of `M.obj U` for all `U : C`.  -/
CategoryTheory.SubmonoidFunctor.obj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {M : CategoryTheory.Functor C MonCat} → CategoryTheory.SubmonoidFunctor M → (U : C) → Submonoid ↑(M.obj U)
-- Mathlib.RingTheory.Noetherian.Defs
/-- **Alias** of `Ideal.fg_of_isNoetherianRing`. -/
Ideal.FG.of_isNoetherianRing : ∀ {R : Type u_1} [inst : Semiring R] [IsNoetherianRing R] (I : Ideal R), I.FG
-- Mathlib.RingTheory.Localization.Integral
IsLocalization.integerNormalization_map_to_map : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (p : Polynomial S),
  ∃ b, Polynomial.map (algebraMap R S) (IsLocalization.integerNormalization M p) = ↑b • p
-- Mathlib.Algebra.Star.Module
star_inv_natCast_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : DivisionSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : StarAddMonoid M] (n : ℕ) (x : M), star ((↑n)⁻¹ • x) = (↑n)⁻¹ • star x
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.SearchStep.cast_rejected : ∀ {s t : String.Slice} {hst : s.copy = t.copy} {startPos endPos : s.Pos},
  String.Slice.Pattern.SearchStep.cast hst (String.Slice.Pattern.SearchStep.rejected startPos endPos) =
    String.Slice.Pattern.SearchStep.rejected (startPos.cast hst) (endPos.cast hst)
-- Mathlib.Algebra.Group.Irreducible.Defs
Irreducible.ne_one : ∀ {M : Type u_1} [inst : Monoid M] {p : M}, Irreducible p → p ≠ 1
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.restrictScalars_id : ∀ (R : Type u_1) {S : Type u_5} {M : Type u_8} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : Module S M] [inst_5 : LinearMap.CompatibleSMul M M R S],
  ↑R LinearMap.id = LinearMap.id
-- Mathlib.Algebra.FreeAlgebra
/-- Scalar multiplication defined as multiplication by the image of elements from `R`.
Note: Used for notation only.
 -/
FreeAlgebra.Pre.hasSMul : (R : Type u_1) → (X : Type u_2) → SMul R (FreeAlgebra.Pre R X)
-- Init.Data.BitVec.Bitblast
/-- An initial value with both `q, r = 0`.  -/
BitVec.DivModState.init : (w : ℕ) → BitVec.DivModState w
-- Mathlib.Order.OrderDual
/-- Transfer `Bot` across an `Equiv`.  -/
Equiv.bot : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Bot β] → Bot α
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.small_closure : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {s : Set M} [Small.{u, w} ↑s],
  Small.{u, w} ↥((FirstOrder.Language.Substructure.closure L).toFun s)
-- Mathlib.Data.Nat.Choose.Central
Nat.centralBinom.eq_1 : ∀ (n : ℕ), n.centralBinom = (2 * n).choose n
-- Mathlib.RingTheory.Trace.Basic
Algebra.embeddingsMatrixReindex.eq_1 : ∀ {κ : Type w} (A : Type u) {B : Type v} (C : Type z) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B]
  [inst_3 : CommRing C] [inst_4 : Algebra A C] (b : κ → B) (e : κ ≃ (B →ₐ[A] C)),
  Algebra.embeddingsMatrixReindex A C b e = (Matrix.reindex (Equiv.refl κ) e.symm) (Algebra.embeddingsMatrix A C b)
-- Mathlib.GroupTheory.Torsion
/-- The group exponent exists for any bounded torsion group.  -/
IsMulTorsion.exponentExists : ∀ {G : Type u_1} [inst : Group G], IsMulTorsion G → (Set.range fun g => orderOf g).Finite → Monoid.ExponentExists G
-- Init.Data.Array.Lemmas
Array.size_filterMap_le : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β} {xs : Array α}, (Array.filterMap f xs).size ≤ xs.size
-- Mathlib.Algebra.Group.Prod
/-- Canonical homomorphism of additive monoids from `AddUnits α` into `α × αᵃᵒᵖ`.
Used mainly to define the natural topology of `AddUnits α`.  -/
AddUnits.embedProduct : (α : Type u_6) → [inst : AddMonoid α] → AddUnits α →+ α × αᵃᵒᵖ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Structures detected.
We expect to find a small number of `IntModule`s in a given goal. Thus, using `Array` is fine here.
 -/
Lean.Meta.Grind.Arith.Linear.State.structs : Lean.Meta.Grind.Arith.Linear.State → Array Lean.Meta.Grind.Arith.Linear.Struct
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.homCategory_comp : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] (𝒳 : CategoryTheory.BasedCategory 𝒮)
  (𝒴 : CategoryTheory.BasedCategory 𝒮) {X Y Z : CategoryTheory.BasedFunctor 𝒳 𝒴} (α : CategoryTheory.BasedNatTrans X Y)
  (β : CategoryTheory.BasedNatTrans Y Z), CategoryTheory.CategoryStruct.comp α β = α.comp β
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.preimage_ceil_of_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {n : ℕ},
  n ≠ 0 → Nat.ceil ⁻¹' {n} = Set.Ioc ↑(n - 1) ↑n
-- Init.Core
thunkCoe : {α : Type u_1} → CoeTail α (Thunk α)
-- Mathlib.Lean.Meta.RefinedDiscrTree.Encode
/-- Encode `e` as a sequence of keys, computing only the first `Key`.  -/
Lean.Meta.RefinedDiscrTree.initializeLazyEntryWithEta : Lean.Expr →
  optParam Bool true → Lean.MetaM (List (Lean.Meta.RefinedDiscrTree.Key × Lean.Meta.RefinedDiscrTree.LazyEntry))
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm'_le_eLpNorm'_mul_rpow_measure_univ : ∀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ε}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {p q : ℝ},
  0 < p →
    p ≤ q →
      MeasureTheory.AEStronglyMeasurable f μ →
        MeasureTheory.eLpNorm' f p μ ≤ MeasureTheory.eLpNorm' f q μ * μ Set.univ ^ (1 / p - 1 / q)
-- Mathlib.Data.QPF.Multivariate.Basic
MvQPF.repr : {n : ℕ} → {F : TypeVec.{u} n → Type u_1} → [self : MvQPF F] → {α : TypeVec.{u} n} → F α → ↑(MvQPF.P F) α
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.bodyInterest.inj : ∀ {β : Type} {x x_1 : Bool},
  Std.Http.Server.Connection.Recv.bodyInterest✝ x = Std.Http.Server.Connection.Recv.bodyInterest✝ x_1 → x = x_1
-- Mathlib.Topology.Inseparable
specializes_iff_mem_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, x ⤳ y ↔ y ∈ closure {x}
-- Init.Data.Int.Order
Int.neg_lt_sub_left_of_lt_add : ∀ {a b c : ℤ}, c < a + b → -a < b - c
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.integral_comp_polarCoord_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℝ E] (f : NumberField.mixedEmbedding.mixedSpace K → E),
  ∫ (x : NumberField.mixedEmbedding.realMixedSpace K) in (NumberField.mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(NumberField.mixedEmbedding.polarCoord K).symm x) =
    ∫ (x : NumberField.mixedEmbedding.mixedSpace K), f x
-- Mathlib.RingTheory.Localization.Cardinality
Localization.cardinalMk : ∀ {R : Type u} [inst : CommRing R] {S : Submonoid R},
  S ≤ nonZeroDivisors R → Cardinal.mk (Localization S) = Cardinal.mk R
-- Mathlib.NumberTheory.LSeries.ZMod
/-- Relation between the completed L-function and the usual one (odd case).
We state it this way around so it holds at the poles of the gamma factor as well.
 -/
ZMod.LFunction_eq_completed_div_gammaFactor_odd : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Odd Φ → ∀ (s : ℂ), ZMod.LFunction Φ s = ZMod.completedLFunction Φ s / (s + 1).Gammaℝ
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.ofCoeff_sum : ∀ {k : Type u_1} {G : Type u_2} [inst : AddCommMonoid k] {k' : Type u_3} {G' : Type u_4} [inst_1 : AddCommMonoid k']
  (f : G →₀ k) (g : G → k → G' →₀ k'), { coeff := f.sum g } = { coeff := f }.sum fun x1 x2 => { coeff := g x1 x2 }
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.extInv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cone F} (φ : c.pt ≅ c'.pt)
  (w : ∀ (j : J), CategoryTheory.CategoryStruct.comp φ.inv (c.π.app j) = c'.π.app j),
  CategoryTheory.Limits.Cone.extInv φ w = CategoryTheory.Limits.Cone.ext φ ⋯
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.mk_right_as : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : L.comp F' ⟶ F), (CategoryTheory.Functor.RightExtension.mk F' α).right.as = PUnit.unit
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.completeMultipartiteGraph.topEmbedding_apply_snd : ∀ {ι : Type u_3} (V : ι → Type u_4) (f : (i : ι) → V i) (i : ι),
  ((SimpleGraph.completeMultipartiteGraph.topEmbedding V f) i).snd = f i
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.instCoeNormalExprExpr : Coe Mathlib.Tactic.Abel.NormalExpr Lean.Expr
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Clear.clear : ∀ {σs : List (Type u)} {P P' A Q : Std.Do.SPred σs}, (P ⊣⊢ₛ P' ∧ A) → (P' ⊢ₛ Q) → P ⊢ₛ Q
-- Mathlib.Data.Seq.Defs
_private.Mathlib.Data.Seq.Defs.0.Stream'.Seq.omap.match_1.eq_2 : ∀ {α : Type u_2} {β : Type u_1} (motive : Option (α × β) → Sort u_3) (a : α) (b : β) (h_1 : Unit → motive none)
  (h_2 : (a : α) → (b : β) → motive (some (a, b))),
  (match some (a, b) with
    | none => h_1 ()
    | some (a, b) => h_2 a b) =
    h_2 a b
-- Std.Internal.Parsec.String
/-- Run a `Parser` on a `String`, returns either the result or an error string with offset.
 -/
Std.Internal.Parsec.String.Parser.run : {α : Type} → Std.Internal.Parsec.String.Parser α → String → Except String α
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.addSubgroupOfEquivOfLe_apply_coe : ∀ {G : Type u_7} [inst : AddGroup G] {H K : AddSubgroup G} (h : H ≤ K) (g : ↥(H.addSubgroupOf K)),
  ↑((AddSubgroup.addSubgroupOfEquivOfLe h) g) = ↑↑g
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.ret.eq_1 : ∀ {α : Type u} (a : α), Stream'.WSeq.ret a = ↑[a]
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
Quiver.FreeGroupoid.instGroupoid : {V : Type u} → [inst : Quiver V] → CategoryTheory.Groupoid (Quiver.FreeGroupoid V)
-- Init.Data.ByteArray.Basic
/-- Retrieves the byte at the indicated index. Callers must prove that the index is in bounds.

Use `uget` for a more efficient alternative or `get!` for a variant that panics if the
index is out of bounds.
 -/
ByteArray.get : (a : ByteArray) → (i : ℕ) → autoParam (i < a.size) ByteArray.get._auto_1 → UInt8
-- Mathlib.Geometry.Convex.Cone.Basic
/-- `hs.toCone s` is the least cone that includes `s`.  -/
Convex.toCone_isLeast : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] {s : Set M} (hs : Convex 𝕜 s),
  IsLeast {t | s ⊆ ↑t} (Convex.toCone s hs)
-- Aesop.RuleSet.Member
Aesop.instInhabitedGlobalRuleSetMember.default : Aesop.GlobalRuleSetMember
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuous_parametric_primitive_of_continuous : ∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : TopologicalSpace X]
  {μ : MeasureTheory.Measure ℝ} [MeasureTheory.NullSingletonClass μ] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {f : X → ℝ → E} {a₀ : ℝ}, Continuous (Function.uncurry f) → Continuous fun p => ∫ (t : ℝ) in a₀..p.2, f p.1 t ∂μ
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
/-- We can partition a finite family into `partition_card ε` sets, such that the remainders
in each set are close together.  -/
AbsoluteValue.exists_partition_int : ∀ (n : ℕ) {ε : ℝ},
  0 < ε → ∀ {b : ℤ}, b ≠ 0 → ∀ (A : Fin n → ℤ), ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
-- Mathlib.Algebra.Group.Subgroup.Order
mabs_mem_iff : ∀ {S : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : LinearOrder G] {x : SetLike S G} [InvMemClass S G] {H : S}
  {x_1 : G}, |x_1|ₘ ∈ H ↔ x_1 ∈ H
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionList : Type
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.mem_addFiber : ∀ {M : Type u_1} [inst : AddMonoid M] {x : M} {ab : M × M}, ab ∈ DiscreteConvolution.addFiber x ↔ ab.1 + ab.2 = x
-- Mathlib.Analysis.Calculus.Deriv.Polynomial
Polynomial.hasFDerivWithinAt_aeval : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {s : Set 𝕜} {R : Type u_1} [inst_1 : CommSemiring R]
  [inst_2 : Algebra R 𝕜] (q : Polynomial R) (x : 𝕜),
  HasFDerivWithinAt (fun x => (Polynomial.aeval x) q)
    (ContinuousLinearMap.smulRight 1 ((Polynomial.aeval x) (Polynomial.derivative q))) s x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
MulOpposite.comap_op_leftUniformSpace : ∀ (G : Type u_1) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G],
  UniformSpace.comap MulOpposite.op (IsTopologicalGroup.leftUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.rightUniformSpace G
-- Aesop.Search.SearchM
Aesop.SearchM.Context.mk.inj : ∀ {ruleSet : Aesop.LocalRuleSet} {normSimpContext : Aesop.NormSimpContext} {options : Aesop.Options'}
  {ruleSet_1 : Aesop.LocalRuleSet} {normSimpContext_1 : Aesop.NormSimpContext} {options_1 : Aesop.Options'},
  { ruleSet := ruleSet, normSimpContext := normSimpContext, options := options } =
      { ruleSet := ruleSet_1, normSimpContext := normSimpContext_1, options := options_1 } →
    ruleSet = ruleSet_1 ∧ normSimpContext = normSimpContext_1 ∧ options = options_1
-- Init.GetElem
List.getElem?_eq_none : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.length ≤ i → l[i]? = none
-- Init.Data.Float.Model.Float32
Float32.Model.mk : (toBits : UInt32) → Float.Model.Format.binary32.Valid toBits.toBitVec → Float32.Model
-- Mathlib.Algebra.Free
FreeAddMagma.lift_comp_of' : ∀ {α : Type u} {β : Type v} [inst : Add β] (f : FreeAddMagma α →ₙ+ β), FreeAddMagma.lift (⇑f ∘ FreeAddMagma.of) = f
-- Mathlib.Logic.Equiv.Defs
Equiv.Perm.sigmaCongrRight_trans : ∀ {α : Type u_1} {β : α → Type u_2} (F G : (a : α) → Equiv.Perm (β a)),
  Equiv.trans (Equiv.Perm.sigmaCongrRight F) (Equiv.Perm.sigmaCongrRight G) =
    Equiv.Perm.sigmaCongrRight fun a => Equiv.trans (F a) (G a)
-- Mathlib.Topology.Algebra.Monoid
Subsemigroup.topologicalClosure_minimal : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Semigroup M] [inst_2 : SeparatelyContinuousMul M]
  (s : Subsemigroup M) {t : Subsemigroup M}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.LinearAlgebra.Isomorphisms
LinearMap.quotKerEquivRange_apply_mk : ∀ {R : Type u_1} {M : Type u_2} {M₂ : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M →ₗ[R] M₂) (x : M),
  ↑(f.quotKerEquivRange (Submodule.Quotient.mk x)) = f x
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.lTensorAlgEquiv_symm_single : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : AddCommMonoid M] (m : M) (a : A)
  (b : B),
  (AddMonoidAlgebra.lTensorAlgEquiv R A B).symm (AddMonoidAlgebra.single m (a ⊗ₜ[R] b)) =
    AddMonoidAlgebra.single m a ⊗ₜ[R] b