mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Closed
/-- If being a sheaf for `J₁` is equivalent to being a sheaf for `J₂`, then `J₁ = J₂`.  -/
CategoryTheory.topology_eq_iff_same_sheaves : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J₁ J₂ : CategoryTheory.GrothendieckTopology C},
  J₁ = J₂ ↔
    ∀ (P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))),
      CategoryTheory.Presieve.IsSheaf J₁ P ↔ CategoryTheory.Presieve.IsSheaf J₂ P
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeKnowsType : Lean.Options → Bool
-- Lean.Compiler.IR.Basic
Lean.IR.flattenAux : Lean.IR.FnBody → Array Lean.IR.FnBody → Array Lean.IR.FnBody × Lean.IR.FnBody
-- Lean.Meta.Basic
/-- Given `e` of the form `fun (p₁ : P₁) … (p₁ : P₁) => t[p_1,…,p_n]` and `arg₁ : P₁, …, argₙ : Pₙ`, returns
* the names `p₁, …, pₙ`,
* the binder infos,
* the binder types `P₁, P₂[arg₁], …, P[arg₁,…,argₙ₋₁]`, and
* the term `t[arg₁,…,argₙ]`.

It uses `whnf` to reduce `e` if it is not a lambda.

See also `Lean.Meta.instantiateLambda`.
 -/
Lean.Meta.instantiateLambdaWithParamInfos : Lean.Expr → Array Lean.Expr → optParam Bool false → Lean.MetaM (Array Lean.Meta.ExprParamInfo × Lean.Expr)
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
/-- One direction of the **Borel-Cantelli lemma**
(sometimes called the "*first* Borel-Cantelli lemma"):
if `(s i)` is a sequence of sets such that `∑' i, μ (s i)` is finite,
then the limit superior of the `s i` along the `atTop` filter is a null set.

Note: for the *second* Borel-Cantelli lemma (applying to independent sets in a probability space),
see `ProbabilityTheory.measure_limsup_eq_one`.  -/
MeasureTheory.measure_limsup_atTop_eq_zero : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s : ℕ → Set α}, ∑' (i : ℕ), μ (s i) ≠ ⊤ → μ (Filter.limsup s Filter.atTop) = 0
-- Std.Data.ExtTreeSet.Basic
/-- Given a proof that such an element exists, retrieves the largest element that is
less than or equal to the given element.
 -/
Std.ExtTreeSet.getLE : {α : Type u} →
  {cmp : α → α → Ordering} →
    [inst : Std.TransCmp cmp] → (t : Std.ExtTreeSet α cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.isComplex_mk_iff : ∀ {K : Type u_1} [inst : Field K] {φ : K →+* ℂ},
  (NumberField.InfinitePlace.mk φ).IsComplex ↔ ¬NumberField.ComplexEmbedding.IsReal φ
-- Lean.Meta.Basic
Lean.Meta.withNewBinderInfos : {n : Type → Type u_1} →
  [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Array (Lean.FVarId × Lean.BinderInfo) → n α → n α
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.ComposableArrows.fourδ₁Toδ₀.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ f₁_1 : i₀ ⟶ i₁)
  (e_f₁ : f₁ = f₁_1) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₁₂ : i₀ ⟶ i₂)
  (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂),
  CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₁ f₂ f₃ f₄ f₁₂ h₁₂ =
    CategoryTheory.ComposableArrows.fourδ₁Toδ₀ f₁_1 f₂ f₃ f₄ f₁₂ ⋯
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.range_arg : Set.range Complex.arg = Set.Ioc (-Real.pi) Real.pi
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.drop.aux.eq_1 : ∀ {α : Type u}, Stream'.WSeq.drop.aux 0 = Computation.pure
-- Mathlib.Data.List.Lattice
List.inter_nil : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), [] ∩ l = []
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.isEmpty_pullback_iff : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S},
  IsEmpty ↥(CategoryTheory.Limits.pullback f g) ↔ Disjoint (Set.range ⇑f) (Set.range ⇑g)
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.mem_factors_iff_dvd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] {a p : α},
  a ≠ 0 → Irreducible p → (Associates.mk p ∈ (Associates.mk a).factors ↔ p ∣ a)
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_sup : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (S T : Submonoid M) (f : F),
  Submonoid.map f (S ⊔ T) = Submonoid.map f S ⊔ Submonoid.map f T
-- Mathlib.RingTheory.Ideal.Prime
Ideal.bot_prime : ∀ {α : Type u} [inst : Semiring α] [Nontrivial α] [NoZeroDivisors α], ⊥.IsPrime
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- The stability axiom in 'arrow' form: If `S` covers `f` then `S` covers `g ≫ f` for any `g`.  -/
CategoryTheory.GrothendieckTopology.arrow_stable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (J : CategoryTheory.GrothendieckTopology C)
  (f : Y ⟶ X) (S : CategoryTheory.Sieve X),
  J.Covers S f → ∀ {Z : C} (g : Z ⟶ Y), J.Covers S (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.ι_mapMap_assoc : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X Y : CategoryTheory.GradedObject I C} (φ : X ⟶ Y) (p : I → J) [inst_1 : X.HasMap p] [inst_2 : Y.HasMap p] (i : I)
  (j : J) (hij : p i = j) {Z : C} (h : Y.mapObj p j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapMap φ p j) h) =
    CategoryTheory.CategoryStruct.comp (φ i) (CategoryTheory.CategoryStruct.comp (Y.ιMapObj p i j hij) h)
-- Mathlib.Order.RelClasses
/-- Set notation form of `LT.lt.trans_le` -/
LT.lt.trans_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊂ b → b ⊆ c → a ⊂ c
-- Init.Data.BitVec.Lemmas
BitVec.toInt_mul : ∀ {w : ℕ} (x y : BitVec w), (x * y).toInt = (x.toInt * y.toInt).bmod (2 ^ w)
-- Mathlib.Algebra.Module.NatInt
AddCommMonoid.toNatModule : {M : Type u_3} → [inst : AddCommMonoid M] → Module ℕ M
-- Mathlib.Tactic.Abel
Mathlib.Tactic.Abel.term_smul : ∀ {α : Type u_1} [inst : AddCommMonoid α] (c n : ℕ) (x a : α) (n' : ℕ) (a' : α),
  c * n = n' →
    Mathlib.Tactic.Abel.smul c a = a' →
      Mathlib.Tactic.Abel.smul c (Mathlib.Tactic.Abel.term n x a) = Mathlib.Tactic.Abel.term n' x a'
-- Mathlib.Algebra.Category.Grp.Biproducts
/-- Construct limit data for a binary product in `AddCommGrpCat`, using
`AddCommGrpCat.of (G × H)`.
 -/
AddCommGrpCat.binaryProductLimitCone : (G H : AddCommGrpCat) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair G H)
-- Lean.Parser.Term
Lean.Parser.Command.commentBody.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.ringHom_eval₂_intCastRingHom : ∀ {R : Type u_3} {S : Type u_4} [inst : Ring R] [inst_1 : Ring S] (p : Polynomial ℤ) (f : R →+* S) (r : R),
  f (Polynomial.eval₂ (Int.castRingHom R) r p) = Polynomial.eval₂ (Int.castRingHom S) (f r) p
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_subset_sdiff : ∀ {α : Type u_1} [inst : DecidableEq α] {s t u v : Finset α}, s ⊆ t → v ⊆ u → s \ u ⊆ t \ v
-- Mathlib.Data.Fintype.Card
Finset.card_compl : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (s : Finset α), sᶜ.card = Fintype.card α - s.card
-- Mathlib.Analysis.Calculus.Deriv.Prod
hasStrictDerivAt_pi : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_1} {E' : ι → Type u_2}
  [inst_1 : (i : ι) → NormedAddCommGroup (E' i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E' i)] {φ : 𝕜 → (i : ι) → E' i}
  {φ' : (i : ι) → E' i}, HasStrictDerivAt φ φ' x ↔ ∀ (i : ι), HasStrictDerivAt (fun x => φ x i) (φ' i) x
-- Mathlib.Algebra.Notation.Pi.Basic
Pi.single_eq_of_ne : ∀ {ι : Type u_1} {M : ι → Type u_6} [inst : (i : ι) → Zero (M i)] [inst_1 : DecidableEq ι] {i i' : ι},
  i' ≠ i → ∀ (x : M i), Pi.single i x i' = 0
-- Init.Data.Nat.Fold
/-- Checks whether there is some number less that the given bound for which `f` returns `true`.

Examples:
* `Nat.any 4 (fun i _ => i < 5) = true`
* `Nat.any 7 (fun i _ => i < 5) = true`
* `Nat.any 7 (fun i _ => i % 2 = 0) = true`
* `Nat.any 1 (fun i _ => i % 2 = 1) = false`
 -/
Nat.any : (n : ℕ) → ((i : ℕ) → i < n → Bool) → Bool
-- Lean.Declaration
/-- Declaration object that can be sent to the kernel.  -/
Lean.Declaration : Type
-- Mathlib.Topology.MetricSpace.PiNat
/-- Given a closed nonempty subset `s` of `Π (n : ℕ), E n`, there exists a retraction onto this
set, i.e., a continuous map with range equal to `s`, equal to the identity on `s`.  -/
PiNat.exists_retraction_of_isClosed : ∀ {E : ℕ → Type u_1} [inst : (n : ℕ) → TopologicalSpace (E n)] [∀ (n : ℕ), DiscreteTopology (E n)]
  {s : Set ((n : ℕ) → E n)}, IsClosed s → s.Nonempty → ∃ f, (∀ x ∈ s, f x = x) ∧ Set.range f = s ∧ Continuous f
-- Mathlib.Order.PartialSups
partialSups_iff_forall : ∀ {α : Type u_1} {ι : Type u_3} [inst : SemilatticeSup α] [inst_1 : Preorder ι] [inst_2 : LocallyFiniteOrderBot ι]
  {f : ι → α} (p : α → Prop), (∀ {a b : α}, p (a ⊔ b) ↔ p a ∧ p b) → ∀ {i : ι}, p ((partialSups f) i) ↔ ∀ j ≤ i, p (f j)
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.throwLevelNameMismatch : {m : Type → Type} →
  {α : Type} → [Monad m] → [Lean.MonadError m] → List Lean.Name → List Lean.Name → Lean.Name → Lean.Name → m α
-- Mathlib.Geometry.Manifold.ContMDiff.Atlas
OpenPartialHomeomorph.contMDiffAt_extend : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {e : OpenPartialHomeomorph M H} {x : M},
  e ∈ IsManifold.maximalAtlas I n M → x ∈ e.source → ContMDiffAt I (modelWithCornersSelf 𝕜 E) n (↑(e.extend I)) x
-- Mathlib.Geometry.Euclidean.Projection
EuclideanGeometry.reflection.eq_1 : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection],
  EuclideanGeometry.reflection s =
    ((AffineIsometryEquiv.vaddConst 𝕜 ↑(Classical.arbitrary ↥s)).symm.trans
          s.direction.reflection.toAffineIsometryEquiv).trans
      (AffineIsometryEquiv.vaddConst 𝕜 ↑(Classical.arbitrary ↥s))
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.comp_apply : ∀ {E : Type u_3} {F : Type u_4} [inst : Group E] [inst_1 : Group F] (p : GroupSeminorm E) (f : F →* E) (x : F),
  (p.comp f) x = p (f x)
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.add.match_1.eq_2 : ∀ (motive : ONote → ONote → Sort u_1) (e : ONote) (n : ℕ+) (a o : ONote) (h_1 : (o : ONote) → motive ONote.zero o)
  (h_2 : (e : ONote) → (n : ℕ+) → (a o : ONote) → motive (e.oadd n a) o),
  (match e.oadd n a, o with
    | ONote.zero, o => h_1 o
    | e.oadd n a, o => h_2 e n a o) =
    h_2 e n a o
-- Mathlib.Algebra.SkewMonoidAlgebra.Support
SkewMonoidAlgebra.support_single_mul_eq_image : ∀ {k : Type u_1} {G : Type u_2} [inst : Monoid G] [inst_1 : Semiring k] [inst_2 : MulSemiringAction G k]
  (f : SkewMonoidAlgebra k G) [inst_3 : DecidableEq G] {r : k} {x : G},
  IsLeftRegular x →
    (∀ (y : k), r * x • y = 0 ↔ y = 0) →
      (SkewMonoidAlgebra.single x r * f).support = Finset.image (fun x_1 => x * x_1) f.support
-- Mathlib.RingTheory.Congruence.Defs
/-- The natural homomorphism from a ring to its quotient by a ring congruence relation.  -/
RingCon.mk' : {R : Type u_1} → [inst : NonAssocSemiring R] → (c : RingCon R) → R →+* c.Quotient
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.prod_source : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (e : PartialEquiv α β) (e' : PartialEquiv γ δ),
  (e.prod e').source = e.source ×ˢ e'.source
-- Mathlib.Probability.Kernel.MeasurableLIntegral
ProbabilityTheory.Kernel.measurable_kernel_prodMk_left' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {η : ProbabilityTheory.Kernel (α × β) γ} [ProbabilityTheory.IsSFiniteKernel η]
  {s : Set (β × γ)}, MeasurableSet s → ∀ (a : α), Measurable fun b => (η (a, b)) (Prod.mk b ⁻¹' s)
-- Mathlib.Analysis.SpecificLimits.Normed
tsum_choose_mul_geometric_of_norm_lt_one' : ∀ {R : Type u_4} [inst : NormedRing R] [HasSummableGeomSeries R] (k : ℕ) {r : R},
  ‖r‖ < 1 → ∑' (n : ℕ), ↑((n + k).choose k) * r ^ n = Ring.inverse (1 - r) ^ (k + 1)
-- Mathlib.Data.Set.Function
Set.eqOn_singleton : ∀ {α : Type u_1} {β : Type u_2} {f₁ f₂ : α → β} {a : α}, Set.EqOn f₁ f₂ {a} ↔ f₁ a = f₂ a
-- Init.Data.Int.Order
Int.nonneg_of_mul_nonneg_right : ∀ {a b : ℤ}, 0 ≤ a * b → 0 < a → 0 ≤ b
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_const_const : ∀ {α : Type u_1} {E : Type u_3} {F'' : Type u_10} [inst : Norm E] [inst_1 : NormedAddCommGroup F''] (c : E) {c' : F''},
  c' ≠ 0 → ∀ (l : Filter α), (fun _x => c) =O[l] fun _x => c'
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
MvPolynomial.trdeg_of_isDomain : ∀ {ι : Type u} {S : Type v} [inst : CommRing S] [IsDomain S],
  Algebra.trdeg S (MvPolynomial ι S) = Cardinal.lift.{v, u} (Cardinal.mk ι)
-- Mathlib.Data.Fin.SuccPred
Fin.lt_castPred_succ_iff : ∀ {n : ℕ} {a b : Fin (n + 1)} (ha : a.succ ≠ Fin.last (n + 1)), b < a.succ.castPred ha ↔ b ≤ a
-- Lean.Server.Requests
Lean.Server.SerializedLspResponse.isComplete : Lean.Server.SerializedLspResponse → Bool
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_eq_self_iff : ∀ {α : Type u_1} {M : Matroid α} {C : Set α}, M.contract C = M ↔ Disjoint C M.E
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.div_left_inj : ∀ {α : Type u} [inst : DivisionMonoid α] {a b c : α}, IsUnit c → (a / c = b / c ↔ a = b)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw.foldRev_cons : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Raw α β} {acc : List ((a : α) × β a)},
  Std.DHashMap.Raw.Internal.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc l =
    Std.DHashMap.Internal.toListModel l.buckets ++ acc
-- Init.Data.UInt.Lemmas
UInt8.toUSize_toUInt32 : ∀ (n : UInt8), n.toUInt32.toUSize = n.toUSize
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- An additive group extension is equivalent to itself.  -/
AddGroupExtension.Equiv.refl : {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) → S.Equiv S
-- Mathlib.Order.Hom.Basic
OrderIso.isMin_apply : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] (f : α ≃o β) {x : α}, IsMin (f x) ↔ IsMin x
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
/-- Lax left unity.  -/
CategoryTheory.LaxFunctor.map₂_leftUnitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.LaxFunctor B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.leftUnitor f).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.map f)).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (self.mapId a) (self.map f))
        (self.mapComp (CategoryTheory.CategoryStruct.id a) f))
-- Mathlib.ModelTheory.Algebra.Field.CharP
FirstOrder.Language.Theory.fieldOfChar.eq_1 : ∀ (p : ℕ),
  FirstOrder.Language.Theory.fieldOfChar p =
    FirstOrder.Language.Theory.field ∪
      if p = 0 then (fun q => FirstOrder.Language.BoundedFormula.not (FirstOrder.Field.eqZero q)) '' {q | Nat.Prime q}
      else if Nat.Prime p then {FirstOrder.Field.eqZero p} else {⊥}
-- Mathlib.Topology.Order
closure_discrete : ∀ {α : Type u_1} [inst : TopologicalSpace α] [DiscreteTopology α] (s : Set α), closure s = s
-- Mathlib.ModelTheory.Algebra.Field.IsAlgClosed
/-- The Theory `Theory.ACF p` is `κ`-categorical whenever `κ` is an uncountable cardinal.  -/
FirstOrder.Field.ACF_categorical : ∀ {p : ℕ} (κ : Cardinal.{u_2}), Cardinal.aleph0 < κ → κ.Categorical (FirstOrder.Language.Theory.ACF p)
-- Mathlib.Data.Fin.Basic
Fin.max_val : ∀ {n : ℕ} {a : Fin n}, max (↑a) n = n
-- Mathlib.Analysis.Convex.BetweenList
List.wbtw_singleton : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (p₁ : P), List.Wbtw R [p₁]
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.apply_coe_mem_map : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {p : Submodule R M} (r : ↥p), f ↑r ∈ Submodule.map f p
-- Init.Data.Ord.UInt
UInt16.instTransOrd : Std.TransOrd UInt16
-- Mathlib.Order.Filter.IsBounded
Filter.IsBounded.isBoundedUnder : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {f : Filter α} {q : β → β → Prop} {u : α → β},
  (∀ (a₀ a₁ : α), r a₀ a₁ → q (u a₀) (u a₁)) → Filter.IsBounded r f → Filter.IsBoundedUnder q f u
-- Init.Grind.Ring.Basic
/-- A ring `α` has characteristic `p` if `OfNat.ofNat x = 0` iff `x % p = 0`.

Note that for `p = 0`, we have `x % p = x`, so this says that `OfNat.ofNat` is injective from `Nat` to `α`.

In the case of a semiring, we take the stronger condition that
`OfNat.ofNat x = OfNat.ofNat y` iff `x % p = y % p`.
 -/
Lean.Grind.IsCharP : (α : Type u) → [Lean.Grind.Semiring α] → outParam ℕ → Prop
-- Mathlib.Topology.Compactness.Lindelof
Set.Countable.isLindelof : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s.Countable → IsLindelof s
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.universallyClosed_isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.UniversallyClosed
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_ofClass : ∀ {S : Type u_1} {R : Type u_2} [inst : NonAssocRing R] [inst_1 : SetLike S R] [inst_2 : SubringClass S R] (s : S),
  ↑(Subring.ofClass s) = ↑s
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_eq_getD_default : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β],
  m.WF → ∀ {a : α}, Std.DHashMap.Raw.Const.get! m a = Std.DHashMap.Raw.Const.getD m a default
-- Mathlib.Control.Functor.Multivariate
_private.Mathlib.Control.Functor.Multivariate.0.TypeVec.append1.match_1.eq_1 : ∀ {n : ℕ} (motive : Fin2 (n + 1) → Sort u_1) (i : Fin2 n) (h_1 : (i : Fin2 n) → motive i.fs)
  (h_2 : Unit → motive Fin2.fz),
  (match i.fs with
    | i.fs => h_1 i
    | Fin2.fz => h_2 ()) =
    h_1 i
-- Init.Grind.Order
Lean.Grind.Order.lt_unsat_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a : α} {k : ℤ}, k.ble' 0 = true → a < a + ↑k → False
-- Mathlib.Topology.Path
Path.refl_reparam : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X} {f : ↑unitInterval → ↑unitInterval} (hfcont : Continuous f)
  (hf₀ : f 0 = 0) (hf₁ : f 1 = 1), (Path.refl x).reparam f hfcont hf₀ hf₁ = Path.refl x
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.Nonsingular.of_rightRegular : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n]
  {A : Matrix n n R}, IsRightRegular A → A.Nonsingular
-- Mathlib.Topology.Constructions.SumProd
/-- Precomposing `f` with `Prod.fst` is continuous  -/
Continuous.fst' : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Z}, Continuous f → Continuous fun x => f x.1
-- Mathlib.NumberTheory.NumberField.House
/-- There exists a "small" non-zero algebraic integral solution of an
non-trivial underdetermined system of linear equations with algebraic integer coefficients.  -/
NumberField.house.exists_ne_zero_int_vec_house_le : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] {α : Type u_2} {β : Type u_3}
  (a : Matrix α β (NumberField.RingOfIntegers K)),
  a ≠ 0 →
    ∀ {p q : ℕ},
      0 < p →
        p < q →
          ∀ [inst_2 : Fintype β],
            Fintype.card β = q →
              ∀ {A : ℝ},
                (∀ (k : α) (l : β), NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) (a k l)) ≤ A) →
                  ∀ [inst_3 : DecidableEq (K →+* ℂ)] [inst_4 : Fintype α],
                    Fintype.card α = p →
                      ∃ ξ,
                        ξ ≠ 0 ∧
                          a.mulVec ξ = 0 ∧
                            ∀ (l : β),
                              NumberField.house ↑(ξ l) ≤
                                NumberField.house.c₁✝ K * (NumberField.house.c₁✝ K * ↑q * A) ^ (↑p / (↑q - ↑p))
-- Mathlib.NumberTheory.NumberField.Units.Basic
/-- The group of roots of unity of order dividing `torsionOrder` is equal to the torsion
group.  -/
NumberField.Units.rootsOfUnity_eq_torsion : ∀ (K : Type u_1) [inst : Field K] [NumberField K],
  rootsOfUnity (NumberField.Units.torsionOrder K) (NumberField.RingOfIntegers K) = NumberField.Units.torsion K
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- Faces are nonempty and downward closed: a non-empty subset of its spanning vertices spans
another face.  -/
PreAbstractSimplicialComplex.isRelLowerSet_faces : ∀ {ι : Type u_1} (self : PreAbstractSimplicialComplex ι), IsRelLowerSet self.faces Finset.Nonempty
-- Mathlib.Data.List.ReduceOption
List.reduceOption_replicate_none : ∀ {α : Type u_1} {n : ℕ}, (List.replicate n none).reduceOption = []
-- Mathlib.Analysis.Convex.EGauge
egauge_zero_zero : ∀ (𝕜 : Type u_1) [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E],
  egauge 𝕜 0 0 = 0
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.orOver_of_exists : ∀ {n : ℕ} {p : ℕ → Prop}, (∃ k < n, p k) → Int.Internal.Linear.OrOver n p
-- Std.Data.HashMap.Raw
/-- Returns `true` if there is a mapping for the given key. There is also a `Prop`-valued version
of this: `a ∈ m` is equivalent to `m.contains a = true`.

Observe that this is different behavior than for lists: for lists, `∈` uses `=` and `contains` uses
`==` for comparisons, while for hash maps, both use `==`.
 -/
Std.HashMap.Raw.contains : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → Bool
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.containsThenInsert!.size.eq_1 : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.containsThenInsert!.size Std.DTreeMap.Internal.Impl.leaf = 0
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.erase!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (t : Std.DTreeMap.Internal.Impl α β),
  Std.DTreeMap.Internal.Impl.erase! k t =
    match t with
    | Std.DTreeMap.Internal.Impl.leaf => Std.DTreeMap.Internal.Impl.leaf
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r =>
      match compare k k' with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.balanceR! k' v' (Std.DTreeMap.Internal.Impl.erase! k l) r
      | Ordering.gt => Std.DTreeMap.Internal.Impl.balanceL! k' v' l (Std.DTreeMap.Internal.Impl.erase! k r)
      | Ordering.eq => l.glue! r
-- Lean.Elab.Do.Basic
/-- Create a `DoElemCont` returning the result using `pure`.  -/
Lean.Elab.Do.DoElemCont.mkPure : Lean.Expr → Lean.Elab.TermElabM Lean.Elab.Do.DoElemCont
-- Init.Data.Array.Erase
Array.mem_of_mem_erase : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {xs : Array α}, a ∈ xs.erase b → a ∈ xs
-- Std.Time.Date.Unit.Week
/-- Convert `Hour.Offset` into `Week.Offset`.
 -/
Std.Time.Week.Offset.ofHours : Std.Time.Hour.Offset → Std.Time.Week.Offset
-- Mathlib.Data.Finset.Empty
Finset.bot_eq_empty : ∀ {α : Type u_1}, ⊥ = ∅
-- Init.Data.SInt.Bitwise
ISize.zero_shiftRight : ∀ {a : ISize}, 0 >>> a = 0