mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a k : α} {v : β}, (t.insert k v)[a]? = if cmp k a = Ordering.eq then some v else t[a]?
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.op_inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P Q : CategoryTheory.ObjectProperty C),
  (P ⊓ Q).op = P.op ⊓ Q.op
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.eval₂_C_mul_T_n : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_3} [inst_1 : CommSemiring S] (f : R →+* S) (x : Sˣ) (r : R)
  (n : ℕ), (LaurentPolynomial.eval₂ f x) (LaurentPolynomial.C r * LaurentPolynomial.T ↑n) = f r * ↑x ^ n
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.hasLimit_cospan_forget_of_right' : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.HasLimit
    (CategoryTheory.Limits.cospan
      (((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inl)
      (((CategoryTheory.Limits.cospan g f).comp AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace).map
        CategoryTheory.Limits.WalkingCospan.Hom.inr))
-- Init.Data.String.Basic
String.Slice.rawEndPos_sliceFrom : ∀ {s : String.Slice} {pos : s.Pos}, (s.sliceFrom pos).rawEndPos = s.rawEndPos.unoffsetBy pos.offset
-- Batteries.Data.List.Lemmas
List.mem_union_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {x : α} {l₁ l₂ : List α}, x ∈ l₁ ∪ l₂ ↔ x ∈ l₁ ∨ x ∈ l₂
-- Mathlib.Order.BoundedOrder.Basic
/-- **Alias** of the forward direction of `isBot_iff_eq_bot`. -/
IsBot.eq_bot : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, IsBot a → a = ⊥
-- Mathlib.Order.Category.Preord
Preord.dualEquiv_functor : Preord.dualEquiv.functor = Preord.dual
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.map_id : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (s : AffineSubspace k P₁), AffineSubspace.map (AffineMap.id k P₁) s = s
-- Mathlib.Tactic.IntervalCases
/-- A `Bound` represents the result of analyzing a lower or upper bound expression.
If `e` is the scrutinee expression, then a lower bound expression like `3 < e`
is normalized to `¬e ≤ 3` and represented as `.lt 3`, and an upper bound expression
like `e ≤ 5` is represented as `.le 5`.
 -/
Mathlib.Tactic.IntervalCases.Bound : Type
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.category : {C : Type u} →
  [CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Category.{max w v, max (w + 1) u} (CategoryTheory.Limits.FormalCoproduct C)
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid_toFun : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : AddMonoid Y] (f : X → Y)
  (hf : f ∈ Function.locallyFinsuppWithin.addSubmonoid U) (a : X),
  (Function.locallyFinsuppWithin.mk_of_mem_addSubmonoid f hf) a = f a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
lt_add_of_pos_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddRightStrictMono α] (a : α) {b : α}, 0 < b → a < b + a
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
SimpleGraph.FarFromTriangleFree.nonpos : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  {ε : 𝕜} [inst_3 : Fintype α] [inst_4 : DecidableRel G.Adj] [Nonempty α],
  G.FarFromTriangleFree ε → G.CliqueFree 3 → ε ≤ 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.instInhabitedToIntInfo : Inhabited Lean.Meta.Grind.Arith.Cutsat.ToIntInfo
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.GoalState.mk : ℕ →
  (enodeMap : Lean.Meta.Grind.ENodeMap) →
    Lean.PArray Lean.Expr →
      Lean.Meta.Grind.ParentMap →
        Lean.Meta.Grind.CongrTable enodeMap →
          Lean.PHashMap Lean.HeadIndex (List Lean.Expr) →
            Lean.PHashSet Lean.HeadIndex →
              Array Lean.Meta.Grind.NewFact →
                Bool →
                  ℕ →
                    Std.Queue Lean.Meta.Grind.NewRawFact →
                      Lean.PArray Lean.Expr →
                        Lean.PHashMap Lean.Meta.Sym.ExprPtr (Array Lean.Meta.Ext.ExtTheorem) →
                          Lean.Meta.Grind.EMatch.State →
                            Lean.Meta.Grind.Injective.State →
                              Lean.Meta.Grind.Split.State →
                                Lean.Meta.Grind.Clean.State →
                                  Array Lean.Meta.Grind.SolverExtensionState → Lean.Meta.Grind.GoalState
-- Init.Data.Array.Attach
Array.getElem_attach : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i < xs.attach.size), xs.attach[i] = ⟨xs[i], ⋯⟩
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_inv : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W),
  cs.length w⁻¹ = cs.length w
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.one_le : ∀ {M : Type u_1} [inst : CommMonoid M] {a : Associates M}, 1 ≤ a
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.instIsSplitMonoBiprodComparison' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] [F.PreservesZeroMorphisms],
  CategoryTheory.IsSplitMono (F.biprodComparison' X Y)
-- Mathlib.LinearAlgebra.AffineSpace.Matrix
/-- Given an affine basis `p`, and a family of points `q : ι' → P`, this is the matrix whose
rows are the barycentric coordinates of `q` with respect to `p`.

It is an affine equivalent of `Basis.toMatrix`.  -/
AffineBasis.toMatrix : {ι : Type u₁} →
  {k : Type u₂} →
    {V : Type u₃} →
      {P : Type u₄} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] →
            [inst_2 : Ring k] → [inst_3 : Module k V] → AffineBasis ι k P → {ι' : Type u_1} → (ι' → P) → Matrix ι' ι k
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelZeroIsoTarget.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.Limits.cokernelZeroIsoTarget = CategoryTheory.Limits.coequalizer.isoTargetOfSelf 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {l : List (α × β)}, (Std.DTreeMap.Raw.Const.insertMany t l).isEmpty = (t.isEmpty && l.isEmpty)
-- Lean.DocString.DeferredCheck
Lean.Doc.DeferredCheckSite.decl.sizeOf_spec : ∀ (name : Lean.Name), sizeOf (Lean.Doc.DeferredCheckSite.decl name) = 1 + sizeOf name
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.unionProd.preimage_β_hom : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), (S.unionProd T).preimage (β_ Y X).hom = T.unionProd S
-- Mathlib.Tactic.FunProp.Types
/-- `RefinedDiscrTree` is lazy, so we store the partially evaluated tree.  -/
Mathlib.Meta.FunProp.State.transitionTheorems : Mathlib.Meta.FunProp.State → Mathlib.Meta.FunProp.GeneralTheorems
-- Init.Data.SInt.Lemmas
Int8.ofInt_int16ToInt : ∀ (x : Int16), Int8.ofInt x.toInt = x.toInt8
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_addOpposite : ∀ {α : Type u}, Cardinal.mk αᵃᵒᵖ = Cardinal.mk α
-- Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate
SSet.instIsSplitMonoChainComplexNatFromNormalizedChainComplex : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasCoproducts C]
  [inst_2 : CategoryTheory.Preadditive C] (X : SSet) (R : C),
  CategoryTheory.IsSplitMono (X.fromNormalizedChainComplex R)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Even
CliffordAlgebra.even.lift.aux_one : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_3} [inst_3 : Ring A] [inst_4 : Algebra R A] (f : CliffordAlgebra.EvenHom Q A),
  (CliffordAlgebra.even.lift.aux f) 1 = 1
-- Lean.Elab.Syntax
/-- We assume a new syntax can be treated as an atom when it starts and ends with a token.
Here are examples of atom-like syntax.
```
syntax "(" term ")" : term
syntax "[" (sepBy term ",") "]" : term
syntax "foo" : term
```
 -/
_private.Lean.Elab.Syntax.0.Lean.Elab.Command.isAtomLikeSyntax : Lean.Syntax → Bool
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Cases.brecOn.eq : ∀ {pu : Lean.Compiler.LCNF.Purity} {motive_1 : Lean.Compiler.LCNF.Alt pu → Sort u}
  {motive_2 : Lean.Compiler.LCNF.FunDecl pu → Sort u} {motive_3 : Lean.Compiler.LCNF.Cases pu → Sort u}
  {motive_4 : Lean.Compiler.LCNF.Code pu → Sort u} {motive_5 : Array (Lean.Compiler.LCNF.Alt pu) → Sort u}
  {motive_6 : List (Lean.Compiler.LCNF.Alt pu) → Sort u} (t : Lean.Compiler.LCNF.Cases pu)
  (F_1 : (t : Lean.Compiler.LCNF.Alt pu) → t.below → motive_1 t)
  (F_2 : (t : Lean.Compiler.LCNF.FunDecl pu) → t.below → motive_2 t)
  (F_3 : (t : Lean.Compiler.LCNF.Cases pu) → t.below → motive_3 t)
  (F_4 : (t : Lean.Compiler.LCNF.Code pu) → t.below → motive_4 t)
  (F_5 : (t : Array (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_1 t → motive_5 t)
  (F_6 : (t : List (Lean.Compiler.LCNF.Alt pu)) → Lean.Compiler.LCNF.Alt.below_2 t → motive_6 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 = F_3 t (Lean.Compiler.LCNF.Cases.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6).2
-- Mathlib.RepresentationTheory.Continuous.TopRep
_private.Mathlib.RepresentationTheory.Continuous.TopRep.0.TopRep.Hom.mk.injEq : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] {A : TopRep k G}
  {B : TopRep k G} (hom' hom'_1 : ContIntertwiningMap A.ρ B.ρ),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂] (e : M₁ ≃SL[σ₁₂] M₂) (b : M₁), ↑e b = e b
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.id.congr_simp : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.ContainsIdentities]
  [inst_4 : W.ContainsIdentities] (X : CategoryTheory.MorphismProperty.Comma L R P Q W), X.id = X.id
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.mkGeneralizedPatternEqProof.checkEqvToLhs? : Lean.Expr → Bool → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.instInsert : Insert ZFSet.{u_1} ZFSet.{u_1}
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStructTruncated
/-- Let `x₀`, `x₁`, `x₂` be `0`-simplices of a `2`-truncated simplicial set `X`,
`e₀₁` an edge from `x₀` to `x₁`, `e₁₂` an edge from `x₁` to `x₂`,
`e₀₂` an edge from `x₀` to `x₂`. This is the data of a `2`-simplex whose
faces are respectively `e₀₂`, `e₁₂` and `e₀₁`. Such structures shall provide
relations in the homotopy category of arbitrary (truncated) simplicial sets
(and specialized constructions for quasicategories and Kan complexes.).  -/
SSet.Truncated.Edge.CompStruct : {X : SSet.Truncated 2} →
  {x₀ x₁ x₂ : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge._proof_1 })} →
    SSet.Truncated.Edge x₀ x₁ → SSet.Truncated.Edge x₁ x₂ → SSet.Truncated.Edge x₀ x₂ → Type u
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
/-- A multiplicative action of a monoid on a monoid `β` gives a multiplicative action on `Set β`.  -/
Finset.mulDistribMulAction : {α : Type u_1} →
  {β : Type u_2} →
    [inst : DecidableEq β] →
      [inst_1 : Monoid α] → [inst_2 : Monoid β] → [MulDistribMulAction α β] → MulDistribMulAction α (Finset β)
-- Lean.Parser.Command
Lean.Parser.Command.computedFields.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.Int.Cast.Defs
AddGroupWithOne.neg_add_cancel : ∀ {R : Type u} [self : AddGroupWithOne R] (a : R), -a + a = 0
-- Mathlib.Analysis.Convex.Cone.Extension
/-- M. **Riesz extension theorem**: given a convex cone `s` in a vector space `E`, a submodule `p`,
and a linear `f : p → ℝ`, assume that `f` is nonnegative on `p ∩ s` and `p + s = E`. Then
there exists a globally defined linear function `g : E → ℝ` that agrees with `f` on `p`,
and is nonnegative on `s`.  -/
riesz_extension : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] (s : PointedCone ℝ E) (f : E →ₗ.[ℝ] ℝ),
  (∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x) →
    (∀ (y : E), ∃ x, ↑x + y ∈ s) → ∃ g, (∀ (x : ↥f.domain), g ↑x = ↑f x) ∧ ∀ x ∈ s, 0 ≤ g x
-- Mathlib.Data.Matrix.Mul
dotProduct_diagonal' : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonUnitalNonAssocSemiring α]
  (v w : m → α) (i : m), (v ⬝ᵥ fun j => Matrix.diagonal w j i) = v i * w i
-- Mathlib.Computability.TuringMachine.StackTuringMachine
/-- The set of subtree statements in a statement.  -/
Turing.TM2.stmts₁ : {K : Type u_1} →
  {Γ : K → Type u_2} → {Λ : Type u_3} → {σ : Type u_4} → Turing.TM2.Stmt Γ Λ σ → Finset (Turing.TM2.Stmt Γ Λ σ)
-- Mathlib.Logic.Equiv.Defs
Equiv.max_def : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) [inst : Max β] (a b : α), a ⊔ b = e.symm (e a ⊔ e b)
-- Mathlib.Data.FunLike.IsApply
FunLike.natCast_eq_nsmul_one : ∀ {F' : Type u_4} {α : Type u_5} [inst : FunLike F' α α] [inst_1 : NatCast F'] [inst_2 : One F'] [inst_3 : SMul ℕ α]
  [inst_4 : SMul ℕ F'] [IsSMulApply ℕ F' α α] [IsNatCastApply F' α] [IsOneApplyEqSelf F' α] (n : ℕ), ↑n = n • 1
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatCastInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.Convex.Segment
Nonneg.segment_eq_uIcc : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜] {x y : { t // 0 ≤ t }},
  segment { t // 0 ≤ t } x y = Set.uIcc x y
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctor.map₂_inv_hom : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g : a ⟶ b} (η : f ≅ g),
  CategoryTheory.CategoryStruct.comp (F.map₂ η.inv) (F.map₂ η.hom) = CategoryTheory.CategoryStruct.id (F.map g)
-- Mathlib.FieldTheory.PurelyInseparable.Basic
/-- A field extension `E / F` of exponential characteristic `q` is purely inseparable
if and only if for every element `x` of `E`, the minimal polynomial of `x` over `F` is of form
`X ^ (q ^ n) - y` for some natural number `n` and some element `y` of `F`.  -/
isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C : ∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q : ℕ) [hF : ExpChar F q],
  IsPurelyInseparable F E ↔ ∀ (x : E), ∃ n y, minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y
-- Mathlib.Order.Antisymmetrization
toAntisymmetrization_ofAntisymmetrization : ∀ {α : Type u_1} (r : α → α → Prop) [inst : IsPreorder α r] (a : Antisymmetrization α r),
  toAntisymmetrization r (ofAntisymmetrization r a) = a
-- Mathlib.NumberTheory.WellApproximable
mem_wellApproximable_iff : ∀ {A : Type u_1} [inst : SeminormedGroup A] {δ : ℕ → ℝ} {a : A},
  a ∈ wellApproximable A δ ↔ a ∈ Filter.blimsup (fun n => approxOrderOf A n (δ n)) Filter.atTop fun n => 0 < n
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_const_const : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {l : Filter α} {c₁ : E''} {c₂ : F''}, c₁ ≠ 0 → c₂ ≠ 0 → (fun x => c₁) =Θ[l] fun x => c₂
-- Mathlib.Tactic.NormNum.NatLog
/-- Given the natural number literals `eb` and `en`, returns `Nat.log eb en`
as a natural number literal and an equality proof.
Panics if `ex` or `en` aren't natural number literals.
 -/
Mathlib.Meta.NormNum.proveNatLog : (eb en : Q(ℕ)) → (ek : Q(ℕ)) × Q(Nat.log «$eb» «$en» = «$ek»)
-- Mathlib.Data.Set.Sigma
Set.biInter_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} (s : Set ι) (t : (i : ι) → Set (α i)) (f : Sigma α → Set β),
  ⋂ ij ∈ s.sigma t, f ij = ⋂ i ∈ s, ⋂ j ∈ t i, f ⟨i, j⟩
-- Mathlib.Algebra.Algebra.Opposite
AlgHom.op_symm_apply_apply : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : Aᵐᵒᵖ →ₐ[R] Bᵐᵒᵖ) (a : A),
  (AlgHom.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.shuffleIt.go : {α : Type u} → Array α → StdGen → ℕ → Array α × StdGen
-- Mathlib.Data.Nat.Init
/-- A natural number `m` divides the sum `m + n` if and only if `m` divides `n`.  -/
Nat.dvd_add_self_left : ∀ {m n : ℕ}, m ∣ m + n ↔ m ∣ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_Ψ₃ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.Ψ₃.coeff 4 = 3
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseFraction : (Std.Time.Fraction → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {fallback : α} {he : Std.DTreeMap.Internal.Impl.contains (t.maxKeyD fallback) t = true},
      t.getKey (t.maxKeyD fallback) he = t.maxKeyD fallback
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Sorted.below : {motive :
    {basis : Tactic.ComputeAsymptotics.Basis} →
      (a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis) → a.Sorted → Prop} →
  {basis : Tactic.ComputeAsymptotics.Basis} →
    {a : Tactic.ComputeAsymptotics.MultiseriesExpansion basis} → a.Sorted → Prop
-- Mathlib.Topology.Algebra.Ring.Ideal
/-- The closure of an ideal in a topological ring as an ideal.  -/
Ideal.closure : {R : Type u_1} → [inst : TopologicalSpace R] → [inst_1 : Ring R] → [IsTopologicalRing R] → Ideal R → Ideal R
-- Init.Data.Bool
Bool.and_self_left : ∀ (a b : Bool), (a && (a && b)) = (a && b)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.finitary_iff : ∀ {α : Type u_1} (M : Matroid α), M.Finitary ↔ ∀ (I : Set α), (∀ J ⊆ I, J.Finite → M.Indep J) → M.Indep I
-- Mathlib.RepresentationTheory.Subrepresentation
/-- A subrepresentation of `ρ` can be thought of as an `A[G]` submodule of `ρ.asModule`.
 -/
Subrepresentation.asSubmodule : {A : Type u_1} →
  {G : Type u_2} →
    {W : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid W] →
            [inst_3 : Module A W] →
              {ρ : Representation A G W} → Subrepresentation ρ → Submodule (MonoidAlgebra A G) ρ.asModule
-- Mathlib.Data.Finset.Image
Finset.map_cons : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (a : α) (s : Finset α) (ha : a ∉ s),
  Finset.map f (Finset.cons a s ha) = Finset.cons (f a) (Finset.map f s) ⋯
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_refl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D}, CategoryTheory.NatIso.op (CategoryTheory.Iso.refl F) = CategoryTheory.Iso.refl F.op
-- Mathlib.RingTheory.Flat.Basic
Algebra.TensorProduct.includeLeft_injective : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CommSemiring S] [inst_6 : Algebra S A]
  [inst_7 : SMulCommClass R S A] [Module.Flat R A],
  Function.Injective ⇑(algebraMap R B) → Function.Injective ⇑Algebra.TensorProduct.includeLeft
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.prod : ∀ {R : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] {x : X}
  {s : Set X} {t : Set Y} {y : Y},
  Convexity.IsStarConvexSet R x s → Convexity.IsStarConvexSet R y t → Convexity.IsStarConvexSet R (x, y) (s ×ˢ t)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
/-- Cover-dense functors induce an equivalence of categories of sheaves.

This is known as the comparison lemma. It requires that the sites are small and the value category
is complete.
 -/
CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        (G : CategoryTheory.Functor C D) →
          (K : CategoryTheory.GrothendieckTopology D) →
            (A : Type v) →
              [inst_2 : CategoryTheory.Category.{u, v} A] →
                [G.LocallyCoverDense K] →
                  [G.IsLocallyFull K] →
                    [G.IsLocallyFaithful K] →
                      [G.IsCoverDense K] →
                        [∀ (X : Dᵒᵖ),
                              CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X G.op) A] →
                          CategoryTheory.Sheaf (G.inducedTopology K) A ≌ CategoryTheory.Sheaf K A
-- Lean.Meta.Tactic.Grind.AC.Seq
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.Seq.superposeAC?.mkResult : Option Lean.Grind.AC.Seq →
  Option Lean.Grind.AC.Seq →
    Option Lean.Grind.AC.Seq → Option (Lean.Grind.AC.Seq × Lean.Grind.AC.Seq × Lean.Grind.AC.Seq)
-- Lean.Elab.Level
Lean.Elab.Level.Context.mk.sizeOf_spec : ∀ (options : Lean.Options) (ref : Lean.Syntax) (autoBoundImplicit : Bool),
  sizeOf { options := options, ref := ref, autoBoundImplicit := autoBoundImplicit } =
    1 + sizeOf options + sizeOf ref + sizeOf autoBoundImplicit
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- The map from `M` to `Γ(M, U)`. This is a localization map when `U = D(f)`.  -/
AlgebraicGeometry.tilde.toOpen : {R : CommRingCat} →
  (M : ModuleCat ↑R) →
    (U : (AlgebraicGeometry.Spec R).Opens) →
      M ⟶ (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).presheaf.obj (Opposite.op U)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapComp_assoc_right_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X)
      ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X)) =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.associator f g h).inv).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X)))
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.measure_subtype_coe_le_comap : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ →
    ∀ (t : Set ↑s), μ (Subtype.val '' t) ≤ (MeasureTheory.Measure.comap Subtype.val μ) t