mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.Bounded
/-- If `s ⊆ t`, then the diameter of `s` is bounded by that of `t`, provided `t` is bounded.  -/
Metric.diam_mono : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s t : Set α}, s ⊆ t → Bornology.IsBounded t → Metric.diam s ≤ Metric.diam t
-- Mathlib.Topology.Constructions.SumProd
isOpen_range_inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsOpen (Set.range Sum.inl)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get?_map : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w}
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) [LawfulBEq α] {f : α → β → γ} {k : α},
  (↑m).WF →
    Std.DHashMap.Internal.Raw₀.Const.get? (Std.DHashMap.Internal.Raw₀.map f m) k =
      Option.map (f k) (Std.DHashMap.Internal.Raw₀.Const.get? m k)
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weightOfEPs_cons : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : V → V → R) {a b c : V} (p : Quiver.Path a b)
  (e : b ⟶ c), Quiver.Path.weightOfEPs w (p.cons e) = Quiver.Path.weightOfEPs w p * w b c
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.gradedMul_def : ∀ (R : Type u_5) {ι : Type u_6} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_7) (ℬ : ι → Type u_8) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ],
  TensorProduct.gradedMul R 𝒜 ℬ =
    TensorProduct.curry
      (TensorProduct.map (LinearMap.mul' R (DirectSum ι fun i => 𝒜 i)) (LinearMap.mul' R (DirectSum ι fun i => ℬ i)) ∘ₗ
        ↑(TensorProduct.assoc R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => 𝒜 i)
                (TensorProduct R (DirectSum ι fun i => ℬ i) (DirectSum ι fun i => ℬ i))).symm ∘ₗ
          LinearMap.lTensor (DirectSum ι fun i => 𝒜 i)
              (↑(TensorProduct.assoc R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)
                    (DirectSum ι fun i => ℬ i)) ∘ₗ
                LinearMap.rTensor (DirectSum ι fun i => ℬ i) ↑(TensorProduct.gradedComm R ℬ 𝒜) ∘ₗ
                  ↑(TensorProduct.assoc R (DirectSum ι ℬ) (DirectSum ι 𝒜) (DirectSum ι ℬ)).symm) ∘ₗ
            ↑(TensorProduct.assoc R (DirectSum ι 𝒜) (DirectSum ι ℬ) (TensorProduct R (DirectSum ι 𝒜) (DirectSum ι ℬ))))
-- Mathlib.RingTheory.Congruence.Hom
/-- Given a function `f`, the smallest ring congruence relation containing the binary
relation on `f`'s image defined by '`x ≈ y` iff the elements of `f⁻¹(x)` are related to
the elements of `f⁻¹(y)` by a ring congruence relation `c`.'  -/
RingCon.mapGen : {M : Type u_1} →
  {N : Type u_2} → [inst : NonAssocSemiring M] → [inst_1 : NonAssocSemiring N] → {c : RingCon M} → (M → N) → RingCon N
-- Init.Tactics
/-- Searches environment for definitions or theorems that can be substituted in
for `exact?%` to solve the goal.
  -/
Lean.Parser.Syntax.exact? : Lean.ParserDescr
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_3.eq_3 : ∀ {n : ℕ} (motive : Option (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) → Sort u_1)
  (h_1 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some (some c)))
  (h_2 : Unit → motive (some none)) (h_3 : Unit → motive none),
  (match none with
    | some (some c) => h_1 c
    | some none => h_2 ()
    | none => h_3 ()) =
    h_3 ()
-- Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
MvPolynomial.esymmAlgHom_apply : ∀ {σ : Type u_1} {R : Type u_3} {n : ℕ} [inst : CommSemiring R] [inst_1 : Fintype σ] (p : MvPolynomial (Fin n) R),
  ↑((MvPolynomial.esymmAlgHom σ R n) p) = (MvPolynomial.aeval fun i => MvPolynomial.esymm σ R (↑i + 1)) p
-- Mathlib.Data.Set.Prod
Set.graphOn.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α), Set.graphOn f s = (fun x => (x, f x)) '' s
-- Mathlib.GroupTheory.Abelianization.Finite
instFiniteAbelianization : ∀ {G : Type u_1} [inst : Group G] [Finite G], Finite (Abelianization G)
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.instMonadMCtxM : Lean.MonadMCtx Lean.Meta.SynthInstance.MkTableKey.M
-- Qq.Macro
Qq.Impl.addDollar : Lean.Name → Lean.Name
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.le_of_le_cert.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (k k_1 : ℤ) (v : Int.Internal.Linear.Var)
  (p : Int.Internal.Linear.Poly)
  (h_1 :
    (k : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k_2 : ℤ) → motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_2))
  (h_2 :
    (k k_2 : ℤ) →
      (v : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_2 v p))
  (h_3 : (c₁ c₂ : ℤ) → motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)),
  (match Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_1 v p with
    | Int.Internal.Linear.Poly.add k v p, Int.Internal.Linear.Poly.num k_2 => h_1 k v p k_2
    | Int.Internal.Linear.Poly.num k, Int.Internal.Linear.Poly.add k_2 v p => h_2 k k_2 v p
    | Int.Internal.Linear.Poly.num c₁, Int.Internal.Linear.Poly.num c₂ => h_3 c₁ c₂
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_2 k k_1 v p
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast.match_1.eq_1 : ∀ {α : Type u_2} {β : α → Type u_1} [inst : BEq α] (a : α)
  (motive : (x : Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Internal.AssocList.contains a x = true → Sort u_3)
  (k : α) (v : β k) (es : Std.DHashMap.Internal.AssocList α β)
  (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true)
  (h_1 :
    (k : α) →
      (v : β k) →
        (es : Std.DHashMap.Internal.AssocList α β) →
          (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true) →
            motive (Std.DHashMap.Internal.AssocList.cons k v es) h),
  (match Std.DHashMap.Internal.AssocList.cons k v es, h with
    | Std.DHashMap.Internal.AssocList.cons k v es, h => h_1 k v es h) =
    h_1 k v es h
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.hom_ext_iff : ∀ {R : Type u} [inst : CommRing R] {X Y : BialgCat R} {f g : X ⟶ Y},
  f = g ↔ BialgCat.Hom.toBialgHom f = BialgCat.Hom.toBialgHom g
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.union_insert_right_equiv_insert_union : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {p : (a : α) × β a}, (t₁ ∪ t₂.insert p.fst p.snd).Equiv ((t₁ ∪ t₂).insert p.fst p.snd)
-- Mathlib.Data.List.Permutation
List.permutationsAux2_snd_nil : ∀ {α : Type u_1} {β : Type u_2} (t : α) (ts : List α) (r : List β) (f : List α → β),
  (List.permutationsAux2 t ts r [] f).2 = r
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_filter_of_getKey?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  {f : α → β → Bool} {k k' : α} {fallback : β},
  t.WF →
    t.getKey? k = some k' →
      Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.filter f t) k fallback =
        (Option.filter (fun x => f k' x) (Std.DTreeMap.Raw.Const.get? t k)).getD fallback
-- Lean.LocalContext
/-- Low level API for adding a local declaration.
Do not use directly.  -/
Lean.LocalContext.addDecl : Lean.LocalContext → Lean.LocalDecl → Lean.LocalContext
-- Lean.Util.Recognizers
Lean.Expr.arrow? : Lean.Expr → Option (Lean.Expr × Lean.Expr)
-- Mathlib.Data.PFun
PFun.bind_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α →. β) (g : β → α →. γ) (a : α),
  f.bind g a = (f a).bind fun b => g b a
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_eq_asc_factorial_div_factorial' : ∀ (n k : ℕ), (n + k - 1).choose k = n.ascFactorial k / k.factorial
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.prependMap.eq_1 : ∀ {α : Type u} {β : α → Type v} (x : Std.DTreeMap.Internal.Zipper α β),
  Std.DTreeMap.Internal.Zipper.prependMap Std.DTreeMap.Internal.Impl.leaf x = x
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- The main non-trivial result: `h.Ω₀` is actually a terminal object.  -/
CategoryTheory.SubobjectRepresentableBy.isTerminalΩ₀ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
      {Ω : C} →
        (h : CategoryTheory.SubobjectRepresentableBy Ω) →
          CategoryTheory.Limits.IsTerminal (CategoryTheory.Subobject.underlying.obj h.Ω₀)
-- Mathlib.Algebra.Exact.Basic
Function.Exact.inr_fst : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N]
  [inst_3 : Module R M] [inst_4 : Module R N], Function.Exact ⇑(LinearMap.inr R M N) ⇑(LinearMap.fst R M N)
-- Mathlib.Topology.Defs.Induced
/-- The topology on the codomain is equal to the coinduced topology.  -/
Topology.IsCoinducing.eq_coinduced : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsCoinducing f → tY = TopologicalSpace.coinduced f tX
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_sdiff_eq_self : ∀ {α : Type u_2} {M : Matroid α} {X Y : Set α}, Y ⊆ M.closure (X \ Y) → M.closure (X \ Y) = M.closure X
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preBeth.eq_1 : ∀ (o : Ordinal.{u}), Cardinal.preBeth o = ⨆ a, 2 ^ Cardinal.preBeth ↑a
-- Mathlib.Order.Minimal
image_monotone_setOfPred_maximal_mem : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃y x : α⦄, y ∈ s → x ∈ s → (f y ≤ f x ↔ y ≤ x)) →
    f '' {x | Maximal (fun x => x ∈ s) x} = {x | Maximal (fun x => x ∈ f '' s) x}
-- Mathlib.Topology.Connected.LocallyPathConnected
/-- **Alias** of `Sum.locallyPathConnectedSpace`.

---

Disjoint unions of locally path-connected spaces are locally path-connected.  -/
Sum.locPathConnectedSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyPathConnectedSpace X]
  [LocallyPathConnectedSpace Y], LocallyPathConnectedSpace (X ⊕ Y)
-- Mathlib.LinearAlgebra.Dual.BaseChange
Module.Dual.congr_apply_apply : ∀ {R : Type u_1} [inst : CommSemiring R] {V : Type u_2} [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {W : Type u_3}
  [inst_3 : AddCommMonoid W] [inst_4 : Module R W] (e : V ≃ₗ[R] W) (a : V →ₗ[R] R) (x : W),
  ((Module.Dual.congr e) a) x = a (e.symm x)
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Projection
EuclideanGeometry.oangle_orthogonalProjection_self : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)] (p : P)
  {p' : P} {s : AffineSubspace ℝ P} [inst_5 : s.direction.HasOrthogonalProjection],
  p ∉ s →
    ∀ (h : p' ∈ s),
      p' ≠ ↑((EuclideanGeometry.orthogonalProjection s) p) →
        EuclideanGeometry.oangle p' (↑((EuclideanGeometry.orthogonalProjection s) p)) p = ↑(Real.pi / 2) ∨
          EuclideanGeometry.oangle p' (↑((EuclideanGeometry.orthogonalProjection s) p)) p = ↑(-Real.pi / 2)
-- Batteries.Data.List.Count
List.coe_sigmaCountToIdx : ∀ {α : Type u_1} [inst : BEq α] {xs : List α} {xc : (x : α) × Fin (List.count x xs)},
  ↑(xs.sigmaCountToIdx xc) = List.idxOfNth xc.fst xs ↑xc.snd
-- Mathlib.NumberTheory.MahlerMeasure
Polynomial.norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one : ∀ {p : Polynomial ℤ},
  (Polynomial.map (Int.castRingHom ℂ) p).mahlerMeasure = 1 → ‖(Polynomial.map (Int.castRingHom ℂ) p).leadingCoeff‖ = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
/-- If `c` is a cofork in `Cᵒᵖ`, then `c.unop.op` is isomorphic to `c`.  -/
CategoryTheory.Limits.Cofork.unopOpIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : Cᵒᵖ} → {f g : X ⟶ Y} → (c : CategoryTheory.Limits.Cofork f g) → c.unop.op ≅ c
-- Std.Internal.Do.WP.Basic
/-- `ExceptT`'s `WP` interpretation: lift the base interpretation by adding an exception
postcondition layer.  -/
Std.Internal.Do.ExceptT.wpInst : {m : Type u → Type z} →
  {EPred : Type u_1} →
    {ε α : Type u} →
      {Pred : Type v} →
        [inst : Std.Internal.Do.Assertion Pred] →
          [inst_1 : Std.Internal.Do.Assertion EPred] →
            [Std.Internal.Do.WP (m (Except ε α)) (Except ε α) Pred EPred] →
              Std.Internal.Do.WP (ExceptT ε m α) α Pred (EPost.Cons✝ (ε → Pred) EPred)
-- Batteries.Recycling.MonadSatisfying.Array
Array.SatisfiesM_mapIdxM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] [LawfulMonad m] {as : Array α}
  {f : ℕ → α → m β} {p : (i : ℕ) → β → i < as.size → Prop} {motive : ℕ → Prop},
  motive 0 →
    (∀ (i : ℕ) (h : i < as.size), motive i → SatisfiesM (fun x => p i x h ∧ motive (i + 1)) (f i as[i])) →
      SatisfiesM (fun arr => motive as.size ∧ ∃ (eq : arr.size = as.size), ∀ (i : ℕ) (h : i < as.size), p i arr[i] h)
        (Array.mapIdxM f as)
-- Aesop.Forward.Substitution
/-- The level substitution implied by the premise substitution. If `e` is the
elaborated rule expression (with level params replaced by level mvars), and
`collectLevelMVars (← instantiateMVars e) = [?m₁, ..., ?mₙ]`, then `levels[i]`
is the level assigned to `?mᵢ`.  -/
Aesop.Substitution.levels : Aesop.Substitution → Array (Option Lean.Level)
-- Mathlib.Data.Rat.Cast.Order
NNRat.cast_lt_ofNat : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {p : ℚ≥0} {n : ℕ}
  [inst_3 : n.AtLeastTwo], ↑p < OfNat.ofNat n ↔ p < OfNat.ofNat n
-- Std.Data.TreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.get? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → Option β
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.neg_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} [inst_3 : CategoryTheory.Preadditive C] {a b c : M}
  (α : CategoryTheory.ShiftedHom X Y a) (β : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c),
  (-α).comp β h = -α.comp β h
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_subset_compl_diagSet : ∀ {α : Type u_1} {r : α → α → Prop} (hr : Std.Symm r), Sym2.fromRel hr ⊆ Sym2.diagSetᶜ ↔ Std.Irrefl r
-- Init.Data.SInt.Lemmas
Int8.le_iff_lt_or_eq : ∀ {a b : Int8}, a ≤ b ↔ a < b ∨ a = b
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : Add M] [inst_1 : SizeOf M] (toSetoid : Setoid M)
  (add' : ∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w + y) (x + z)),
  sizeOf { toSetoid := toSetoid, add' := add' } = 1 + sizeOf toSetoid
-- Mathlib.Order.Minimal
maximal_toDual : ∀ {α : Type u_2} {P : α → Prop} {x : α} [inst : LE α],
  Maximal (fun x => P (OrderDual.ofDual x)) (OrderDual.toDual x) ↔ Minimal P x
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryGE! : {α : Type u} → {β : Type v} → [Ord α] → [Inhabited (α × β)] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → α × β
-- Batteries.Data.DList.Basic
Batteries.DList.toList_mk : ∀ {α : Type u_1} {f : List α → List α} {h : ∀ (l : List α), f l = f [] ++ l},
  { apply := f, invariant := h }.toList = f []
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.startsWith_slice_of_isEmpty : ∀ {pat s : String.Slice}, pat.isEmpty = true → s.startsWith pat = true
-- Mathlib.Order.Directed
OrderDual.isDirected_le : ∀ {α : Type u_1} [inst : LE α] [IsCodirectedOrder α], IsDirectedOrder αᵒᵈ
-- Mathlib.Topology.Algebra.Module.ModuleTopology
IsModuleTopology.continuous_neg : ∀ (R : Type u_1) [τR : TopologicalSpace R] [inst : Semiring R] (C : Type u_6) [inst_1 : AddCommGroup C]
  [inst_2 : Module R C] [inst_3 : TopologicalSpace C] [IsModuleTopology R C], Continuous fun a => -a
-- Mathlib.Algebra.Order.Positive.Ring
Positive.addLeftReflectLT : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftStrictMono M] [AddLeftReflectLT M],
  AddLeftReflectLT { x // 0 < x }
-- Mathlib.Topology.UniformSpace.Closeds
UniformSpace.hausdorff.continuous_closure : ∀ {α : Type u_1} [inst : UniformSpace α], Continuous closure
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapRightIso_functor_obj_right : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  {R₁ R₂ : CategoryTheory.Functor B T} (i : R₁ ≅ R₂) (X : CategoryTheory.Comma L R₁),
  ((CategoryTheory.Comma.mapRightIso L i).functor.obj X).right = X.right
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.zeroLocus_eq_basicOpen_of_mul_add : ∀ {R : Type u} [inst : CommSemiring R] (e f : R),
  e * f = 0 → e + f = 1 → PrimeSpectrum.zeroLocus {e} = ↑(PrimeSpectrum.basicOpen f)
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold.injEq : ∀ (declName unfold declName_1 unfold_1 : Lean.Name),
  (Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold declName unfold =
      Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold declName_1 unfold_1) =
    (declName = declName_1 ∧ unfold = unfold_1)
-- Init.Data.Vector.Basic
/-- Computes the product of the elements of a vector.

Examples:
* `#v[a, b, c].prod = a * (b * (c * 1))`
* `#v[1, 2, 5].prod = 10`
 -/
Vector.prod : {α : Type u_1} → {n : ℕ} → [Mul α] → [One α] → Vector α n → α
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.YonedaCollection.map₂_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} {X Y : C}
  (f : X ⟶ Y) (p : CategoryTheory.OverPresheafAux.YonedaCollection F Y),
  (CategoryTheory.OverPresheafAux.YonedaCollection.map₂ F f p).fst =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.yoneda.map f) p.fst
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.le_mul_left : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : Associates M}, a ≤ b * a
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.injective_lift_iff : ∀ {R : Type u} {S : Type v} [inst : Ring R] [inst_1 : Semiring S] {I : Ideal R} [inst_2 : I.IsTwoSided] {f : R →+* S}
  (H : ∀ a ∈ I, f a = 0), Function.Injective ⇑(Ideal.Quotient.lift I f H) ↔ RingHom.ker f = I
-- Mathlib.Algebra.DirectSum.Idempotents
/-- If a semiring can be decomposed into direct sum of finite left ideals `Vᵢ`
where `1 = e₁ + ... + eₙ` and `eᵢ ∈ Vᵢ`, then `eᵢ` is a family of complete
orthogonal idempotents.  -/
DirectSum.completeOrthogonalIdempotents_idempotent : ∀ {R : Type u_1} {I : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq I] (V : I → Ideal R)
  [inst_2 : DirectSum.Decomposition V] [inst_3 : Fintype I], CompleteOrthogonalIdempotents (DirectSum.idempotent V)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.denote_norm : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (e : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Poly.denote ctx e.norm = Lean.Grind.Linarith.Expr.denote ctx e
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithBot.WithTop.completeLinearOrder : {α : Type u_5} → [ConditionallyCompleteLinearOrder α] → CompleteLinearOrder (WithBot (WithTop α))
-- Mathlib.Topology.Subpath
/-- Given a path `γ` and a sequence `t` of `n + 1` points in `[0, 1]`, there is a natural homotopy
between the concatenation of paths `γ.subpath (t k) (t (k + 1))`, and `γ.subpath (t 0) (t n)`.  -/
Path.Homotopy.concatSubpath : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {a b : X} →
      {n : ℕ} →
        (γ : Path a b) →
          (t : Fin (n + 1) → ↑unitInterval) →
            (Path.concat (⇑γ ∘ t) fun k => γ.subpath (t k.castSucc) (t k.succ)).Homotopy
              (γ.subpath (t 0) (t (Fin.last n)))
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Creates a matrix from a list of elements in the form `(i, j, mat[i, j])`.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm.ofValues : {α : ℕ → ℕ → Type} →
  [self : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm α] → {n m : ℕ} → List (ℕ × ℕ × ℚ) → α n m
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.natDegree_optionEquivLeft : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial (Option σ) R),
  ((MvPolynomial.optionEquivLeft R σ) p).natDegree = MvPolynomial.degreeOf none p
-- Mathlib.Logic.Function.CompTypeclasses
CompTriple.comp_apply : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} {φ : M → N} {ψ : N → P} {χ : M → P},
  CompTriple φ ψ χ → ∀ (x : M), ψ (φ x) = χ x
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.hasLevelMVarAtCurrDepth : Lean.Expr → Lean.MetaM Bool
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.EqnInfo.type : Lean.Elab.WF.EqnInfo → Lean.Expr
-- Mathlib.Algebra.Ring.Defs
neg_mul_eq_neg_mul : ∀ {α : Type u} [inst : Mul α] [inst_1 : HasDistribNeg α] (a b : α), -(a * b) = -a * b
-- Mathlib.Data.Matrix.Reflection
/-- This can be used to prove
```lean
example (P : Matrix (Fin 2) (Fin 3) α → Prop) :
  (∀ x, P x) ↔ ∀ a b c d e f, P !![a, b, c; d, e, f] :=
(forall_iff _).symm
```
 -/
Matrix.forall_iff : ∀ {α : Type u_1} {m n : ℕ} (P : Matrix (Fin m) (Fin n) α → Prop),
  Matrix.Forall P ↔ ∀ (x : Matrix (Fin m) (Fin n) α), P x
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.Integrable.integral_smul : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {R : Type u_6} [inst_2 : NormedRing R] [inst_3 : Module R G] [IsBoundedSMul R G]
  [SMulCommClass ℝ R G] (c : R) {f : α → G},
  MeasureTheory.Integrable f μ → ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The cokernel of `f.op` is the opposite of `kernel f`.  -/
CategoryTheory.cokernelOpUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → Opposite.unop (CategoryTheory.Limits.cokernel f.op) ≅ CategoryTheory.Limits.kernel f
-- Lean.Data.AssocList
Lean.AssocList.findEntry? : {α : Type u} → {β : Type v} → [BEq α] → α → Lean.AssocList α β → Option (α × β)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKey!_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false →
        (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKey! =
          if compare t.minKey! k = Ordering.eq then k else t.minKey!
-- Mathlib.Topology.Irreducible
image_mem_irreducibleComponents_of_isPreirreducible_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  Continuous f →
    IsOpenMap f →
      (∀ (x : Y), IsPreirreducible (f ⁻¹' {x})) →
        Function.Surjective f → ∀ {V : Set X}, V ∈ irreducibleComponents X → f '' V ∈ irreducibleComponents Y