mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.ComposableArrows
CategoryTheory.Localization.essSurj_mapComposableArrows_of_hasRightCalculusOfFractions : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W] [W.HasRightCalculusOfFractions] (n : ℕ),
  (L.mapComposableArrows n).EssSurj
-- Mathlib.SetTheory.Cardinal.Cofinality.Enum
Order.enum_univ : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : WellFoundedLT α] [inst_2 : IsRegularCardinalOrder α] (x : α),
  (Order.enum Set.univ ⋯) x = ⟨x, ⋯⟩
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_erase_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k : α} [inst_1 : Inhabited (β k)],
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.get! k = default
-- Mathlib.NumberTheory.PythagoreanTriples
PythagoreanTriple.isPrimitiveClassified_of_coprime_of_odd_of_pos : ∀ {x y z : ℤ} (h : PythagoreanTriple x y z), x.gcd y = 1 → y % 2 = 1 → 0 < z → h.IsPrimitiveClassified
-- Lean.Meta.Tactic.Grind.EMatchAction
_private.Lean.Meta.Tactic.Grind.EMatchAction.0.Lean.Meta.Grind.Action.CollectState : Type
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is any function and `g` is analytic without zero at `z₀`, then `f` is meromorphic in
normal form at `z₀` iff `g * f` is meromorphic in normal form at `z₀`.  -/
meromorphicNFAt_mul_iff_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {g : 𝕜 → 𝕜} {x : 𝕜} {f : 𝕜 → 𝕜},
  AnalyticAt 𝕜 g x → g x ≠ 0 → (MeromorphicNFAt (g * f) x ↔ MeromorphicNFAt f x)
-- Mathlib.Algebra.Field.Defs
/-- `a ^ 0 = 1`  -/
Semifield.zpow_zero' : ∀ {K : Type u_2} [self : Semifield K] (a : K), a ^ 0 = 1
-- Init.Data.String.Bootstrap
Substring.Raw.Internal.front : Substring.Raw → Char
-- Mathlib.Data.Nat.Fib.Basic
Nat.le_fib_self : ∀ {n : ℕ}, 5 ≤ n → n ≤ Nat.fib n
-- Init.Grind.Norm
Lean.Grind.exists_and_left : ∀ {α : Sort u} {p : α → Prop} {b : Prop}, (∃ x, b ∧ p x) = (b ∧ ∃ x, p x)
-- Mathlib.Algebra.Polynomial.Bivariate
/-- Two equivalent ways to express the evaluation of a bivariate polynomial over `R`
at a point in the affine plane over an `R`-algebra `S`.  -/
Polynomial.eval₂RingHom_eval₂RingHom : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S) (x y : S),
  Polynomial.eval₂RingHom (Polynomial.eval₂RingHom f x) y =
    (Polynomial.evalEvalRingHom x y).comp (Polynomial.mapRingHom (Polynomial.mapRingHom f))
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'Map_f_eq_cyclesMap : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i'] {i : ι} (hi : e.BoundaryLE i)
  {i' : ι'} (h : e.f i = i'),
  (HomologicalComplex.truncLE'Map φ e).f i =
    CategoryTheory.CategoryStruct.comp (K.truncLE'XIsoCycles e h hi).hom
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap φ i') (L.truncLE'XIsoCycles e h hi).inv)
-- Mathlib.Algebra.Polynomial.Eval.Degree
Polynomial.iterate_comp_eval₂ : ∀ {R : Type u} {S : Type v} [inst : Semiring R] {p q : Polynomial R} [inst_1 : CommSemiring S] (f : R →+* S) (k : ℕ)
  (t : S), Polynomial.eval₂ f t (p.comp^[k] q) = (fun x => Polynomial.eval₂ f x p)^[k] (Polynomial.eval₂ f t q)
-- Init.Data.List.Attach
List.unattach.eq_1 : ∀ {α : Type u_1} {p : α → Prop} (l : List { x // p x }), l.unattach = List.map (fun x => ↑x) l
-- Mathlib.Algebra.Module.Rat
map_nnrat_smul : ∀ {M : Type u_1} {M₂ : Type u_2} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] [_instM : Module ℚ≥0 M]
  [_instM₂ : Module ℚ≥0 M₂] {F : Type u_3} [inst_2 : FunLike F M M₂] [AddMonoidHomClass F M M₂] (f : F) (c : ℚ≥0)
  (x : M), f (c • x) = c • f x
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.mem_toList_iff_getElem?_eq_some : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t.WF → ∀ {k : α} {v : β}, (k, v) ∈ t.toList ↔ t[k]? = some v
-- Mathlib.Data.Finset.Max
Finset.min'_union : ∀ {α : Type u_2} [inst : LinearOrder α] {s₁ s₂ : Finset α} (h₁ : s₁.Nonempty) (h₂ : s₂.Nonempty),
  (s₁ ∪ s₂).min' ⋯ = min (s₁.min' h₁) (s₂.min' h₂)
-- Mathlib.FieldTheory.SeparableDegree
/-- If `E / F` is a separable extension, then its separable degree is equal to its degree.
When `E / F` is infinite, it means that `Field.Emb F E` has infinitely many elements.
(But the cardinality of `Field.Emb F E` is not equal to `Module.rank F E` in general!)  -/
Field.finSepDegree_eq_finrank_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [Algebra.IsSeparable F E],
  Field.finSepDegree F E = Module.finrank F E
-- Mathlib.Data.Nat.Fib.Basic
Nat.fib_mono : Monotone Nat.fib
-- Mathlib.NumberTheory.SmoothNumbers
/-- A number that divides an `s`-factored number is itself `s`-factored.  -/
Nat.mem_factoredNumbers_of_dvd : ∀ {s : Finset ℕ} {m k : ℕ}, m ∈ Nat.factoredNumbers s → k ∣ m → k ∈ Nat.factoredNumbers s
-- Mathlib.Analysis.Normed.Operator.Basic
ContinuousLinearMap.opNorm_nonneg : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F), 0 ≤ ‖f‖
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.tprod_div : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : CommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalGroup α] {f g : β → α} [T2Space α] [L.NeBot],
  Multipliable f L → Multipliable g L → ∏'[L] (b : β), f b / g b = (∏'[L] (b : β), f b) / ∏'[L] (b : β), g b
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f f_1 : X ⟶ Y)
  (e_f : f = f_1) [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f],
  AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f =
    AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f_1
-- Mathlib.Probability.Decision.Risk.Basic
/-- See `bayesRisk_le_iInf'` for a similar result when `P` is not a Markov kernel.  -/
ProbabilityTheory.bayesRisk_le_iInf : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal},
  Measurable (Function.uncurry ℓ) →
    ∀ (P : ProbabilityTheory.Kernel Θ 𝓧) [ProbabilityTheory.IsMarkovKernel P] (π : MeasureTheory.Measure Θ),
      ProbabilityTheory.bayesRisk ℓ P π ≤ ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂π
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
/-- The identity modification.  -/
CategoryTheory.Pseudofunctor.StrongTrans.Modification.id : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} →
          (η : F ⟶ G) → CategoryTheory.Pseudofunctor.StrongTrans.Modification η η
-- Mathlib.Tactic.ProxyType
/-- Generates a proxy type for the inductive type and an equivalence from the proxy type to the type.

If the declarations already exist, there is a check that they are correct.
 -/
Mathlib.ProxyType.ensureProxyEquiv : Mathlib.ProxyType.ProxyEquivConfig → Lean.InductiveVal → Lean.Elab.TermElabM Unit
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
Ideal.IsHomogeneous.inf : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {I J : Ideal A},
  Ideal.IsHomogeneous 𝒜 I → Ideal.IsHomogeneous 𝒜 J → Ideal.IsHomogeneous 𝒜 (I ⊓ J)
-- Mathlib.GroupTheory.SpecificGroups.Quaternion
QuaternionGroup.a_mul_a : ∀ {n : ℕ} (i j : ZMod (2 * n)), QuaternionGroup.a i * QuaternionGroup.a j = QuaternionGroup.a (i + j)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.MutualClosure.pushLocalDecl : Array Lean.FVarId →
  Lean.FVarId →
    Lean.Name →
      Lean.Expr →
        Lean.BinderInfo →
          Lean.LocalDeclKind →
            StateRefT' IO.RealWorld Lean.Elab.Term.MutualClosure.ClosureState Lean.Elab.TermElabM (Array Lean.FVarId)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.toUnder_map_right : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor D T)
  {Y X_1 : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit X) (F.comp (CategoryTheory.Functor.id T))}
  (f : Y ⟶ X_1), ((CategoryTheory.StructuredArrow.toUnder X F).map f).right = F.map f.right
-- Mathlib.Algebra.Group.Defs
/-- Multiplication is commutative in a commutative multiplicative magma.  -/
CommSemigroup.mul_comm : ∀ {G : Type u} [self : CommSemigroup G] (a b : G), a * b = b * a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_eq_of_mem : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α]
  [inst_3 : Inhabited α], m.WF → ∀ {k : α}, k ∈ m → m.getKey! k = k
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGE_iff_antitone_get`. -/
Antitone.sortedGE : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], Antitone l.get → l.SortedGE
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.count_eq_forIn : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] [inst_4 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  {it : Std.Iter β}, it.length = (forIn it 0 fun x acc => pure (ForInStep.yield (acc + 1))).run
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.of_le_norm_mul_star_self : ∀ {E : Type u_2} [inst : NonUnitalNormedRing E] [inst_1 : StarRing E],
  (∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * star x‖) → CStarRing E
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation_map : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℝ F]
  [hF : Fact (Module.finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x : F),
  ((Orientation.map (Fin 2) φ.toLinearEquiv) o).rightAngleRotation x = φ (o.rightAngleRotation (φ.symm x))
-- Init.Data.Array.Lemmas
Array.filterMap_empty : ∀ {α : Type u_1} {β : Type u_2} {f : α → Option β}, Array.filterMap f #[] = #[]
-- Mathlib.Algebra.Order.Group.Equiv
/-- `toLex` as a `MulEquiv`.  -/
toLexMulEquiv : (α : Type u_1) → [inst : Mul α] → α ≃* Lex α
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β a → Bool},
  Std.DHashMap.Internal.Raw.WFImp ↑m → Std.DHashMap.Internal.Raw.WFImp ↑(Std.DHashMap.Internal.Raw₀.filter f m)
-- Mathlib.Analysis.Normed.Algebra.QuaternionExponential
/-- Auxiliary result; if the power series corresponding to `Real.cos` and `Real.sin` evaluated
at `‖q‖` tend to `c` and `s`, then the exponential series tends to `c + (s / ‖q‖)`.  -/
Quaternion.hasSum_expSeries_of_imaginary : ∀ {q : Quaternion ℝ},
  q.re = 0 →
    ∀ {c s : ℝ},
      HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n) / ↑(2 * n).factorial) c →
        HasSum (fun n => (-1) ^ n * ‖q‖ ^ (2 * n + 1) / ↑(2 * n + 1).factorial) s →
          HasSum (fun n => (NormedSpace.expSeries ℝ (Quaternion ℝ) n) fun x => q) (↑c + (s / ‖q‖) • q)
-- Init.Prelude
List.toByteArray.loop : List UInt8 → ByteArray → ByteArray
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_submatrix_equiv : ∀ {α : Type u_1} {m : Type u_3} {n : Type u_4} [inst : Star α] {A : Matrix n n α} (e : m ≃ n),
  (A.submatrix ⇑e ⇑e).IsHermitian ↔ A.IsHermitian
-- Std.Http.Protocol.H1
/-- Consumes a zero-length fixed body and immediately marks body completion.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.parseFixedZeroBody : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Std.Http.Protocol.H1.Machine dir × Option Std.Http.Protocol.H1.PulledChunk × Bool
-- Mathlib.Algebra.Homology.HomologicalComplexAbelian
HomologicalComplex.instAbelian : {C : Type u_1} →
  {ι : Type u_2} →
    {c : ComplexShape ι} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.Abelian (HomologicalComplex C c)
-- Mathlib.Topology.Compactness.CountablyCompact
/-- For every countable open directed cover of a countably compact set, there exists a single
element of the cover which itself includes the set.  -/
IsCountablyCompact.elim_directed_cover : ∀ {ι : Type u_1} {E : Type u_2} [inst : TopologicalSpace E] {A : Set E} [Countable ι] [Nonempty ι],
  IsCountablyCompact A →
    ∀ (U : ι → Set E), (∀ (i : ι), IsOpen (U i)) → A ⊆ ⋃ i, U i → Directed (fun x1 x2 => x1 ⊆ x2) U → ∃ i, A ⊆ U i
-- Mathlib.Data.Fin.Basic
Fin.exists_eq_add_of_le : ∀ {n : ℕ} {a b : Fin n}, a ≤ b → ∃ k ≤ b, b = a + k
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
/-- Given an ordered family of vectors `i ↦ v i` ranging over `i ∈ I`, and indexes
`α₁, α₂, …, αₙ ∈ I` (not necessarily in order) the wedge product `v (α 1) ∧ ⋯ ∧ v (α n)` belongs to
the span of `n`-fold _ordered_ wedge products of elements of the `v i`.  -/
_private.Mathlib.LinearAlgebra.ExteriorPower.Basic.0.exteriorPower.ιMulti_family_span_fixedDegree_aux : ∀ (R : Type u) [inst : CommRing R] {n : ℕ} {M : Type u_1} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Type u_4}
  [inst_3 : LinearOrder I] (v : I → M) (α : Fin n → I),
  (ExteriorAlgebra.ιMulti R n) (v ∘ α) ∈ Submodule.span R (Set.range (ExteriorAlgebra.ιMulti_family R n v))
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_apply_zero : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : Field 𝕂] [inst_1 : Ring 𝔸] [inst_2 : Algebra 𝕂 𝔸] [inst_3 : TopologicalSpace 𝔸]
  [inst_4 : IsTopologicalRing 𝔸] (n : ℕ), ((NormedSpace.expSeries 𝕂 𝔸 n) fun x => 0) = Pi.single 0 1 n
-- Mathlib.Topology.Sheaves.Stalks
/-- A variant of `germ_res` with `op V ⟶ op U`
so that the LHS is more general and simp fires more easier.  -/
TopCat.Presheaf.germ_res'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) {U V : TopologicalSpace.Opens ↑X} (i : Opposite.op V ⟶ Opposite.op U) (x : ↑X) (hx : x ∈ U)
  {Z : C} (h : F.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map i) (CategoryTheory.CategoryStruct.comp (F.germ U x hx) h) =
    CategoryTheory.CategoryStruct.comp (F.germ V x ⋯) h
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageKind.notification : Lean.JsonRpc.MessageKind
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.linearIndependent_X : ∀ (σ : Type u) (R : Type v) [inst : CommSemiring R], LinearIndependent R MvPolynomial.X
-- Init.NotationExtra
/-- Similar to `first`, but succeeds only if one the given tactics solves the current goal.
 -/
Lean.solveTactic : Lean.ParserDescr
-- Mathlib.ModelTheory.Definability
Set.DefinableMap.eq_1 : ∀ {M : Type u_1} (L : FirstOrder.Language) [inst : L.Structure M] {α : Type u_2} {β : Type u_3} (A : Set M)
  (F : (α → M) → β → M), Set.DefinableMap L A F = ∀ (i : β), Set.DefinableFun L A fun x => F x i
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- A version of `UniformOnFun.hasBasis_uniformity_of_basis`
with weaker conclusion and weaker assumptions.

We make no assumptions about the set `𝔖`
but conclude only that the uniformity is equal to some indexed infimum.  -/
UniformOnFun.uniformity_eq_of_basis : ∀ {α : Type u_1} (β : Type u_2) [inst : UniformSpace β] (𝔖 : Set (Set α)) {ι : Sort u_5} {p : ι → Prop}
  {V : ι → Set (β × β)},
  (uniformity β).HasBasis p V →
    uniformity (UniformOnFun α β 𝔖) = ⨅ s ∈ 𝔖, ⨅ i, ⨅ (_ : p i), Filter.principal (UniformOnFun.gen 𝔖 s (V i))
-- Mathlib.Order.Filter.CountablyGenerated
Filter.IsCountableBasis.toIsBasis : ∀ {α : Type u_1} {ι : Type u_4} {p : ι → Prop} {s : ι → Set α}, Filter.IsCountableBasis p s → Filter.IsBasis p s
-- Init.Data.SInt.Bitwise
Int16.ne_not_self : ∀ {a : Int16}, a ≠ ~~~a
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_prodUnique : ∀ (R : Type u_8) (M : Type u_9) (N : Type u_10) [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid M] [inst_3 : TopologicalSpace N] [inst_4 : AddCommMonoid N] [inst_5 : Unique N]
  [inst_6 : Module R M] [inst_7 : Module R N],
  (↑(ContinuousLinearEquiv.prodUnique R M N)).toEquiv = Equiv.prodUnique M N
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
_private.Mathlib.RingTheory.MvPolynomial.Homogeneous.0.MvPolynomial.IsHomogeneous.exists_eval_ne_zero_of_totalDegree_le_card_aux : ∀ {R : Type u_5} [inst : CommRing R] [IsDomain R] {N : ℕ} {F : MvPolynomial (Fin N) R} {n : ℕ},
  F.IsHomogeneous n → F ≠ 0 → ↑n ≤ Cardinal.mk R → ∃ r, (MvPolynomial.eval r) F ≠ 0
-- Std.Async.Basic
_private.Std.Async.Basic.0.Std.Async.EAsync.forIn.loop : {ε β : Type} → (Unit → β → Std.Async.EAsync ε (ForInStep β)) → Task.Priority → IO.Promise (Except ε β) → β → BaseIO Unit
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- Auxiliary construction of a cone for `le_inf`.  -/
CategoryTheory.Subobject.leInfCone : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        {A : C} →
          (s : Set (CategoryTheory.Subobject A)) →
            (f : CategoryTheory.Subobject A) →
              (∀ g ∈ s, f ≤ g) → CategoryTheory.Limits.Cone (CategoryTheory.Subobject.wideCospan s)
-- Std.Async.System
/-- The home directory of the user.
 -/
Std.Async.System.SystemUser.homeDir : Std.Async.System.SystemUser → Option System.FilePath
-- Mathlib.Data.Sym.Basic
/-- Construct an element of the `n`th symmetric power from a multiset of cardinality `n`.
 -/
Sym.mk : {α : Type u_1} → {n : ℕ} → (m : Multiset α) → m.card = n → Sym α n
-- Init.Data.Vector.Range
Vector.mem_zipIdx : ∀ {α : Type u_1} {n : ℕ} {x : α} {i : ℕ} {xs : Vector α n} {k : ℕ} (h : (x, i) ∈ xs.zipIdx k),
  k ≤ i ∧ i < k + n ∧ x = xs[i - k]
-- Mathlib.Order.Heyting.Basic
sup_sdiff_distrib : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] (b c a : α), (b ⊔ c) \ a = b \ a ⊔ c \ a
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_prod : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] {S : NonUnitalSubalgebra R A}
  {S₁ : NonUnitalSubalgebra R B} {x : A × B}, x ∈ S.prod S₁ ↔ x.1 ∈ S ∧ x.2 ∈ S₁
-- Mathlib.CategoryTheory.Monoidal.Subcategory
/-- An inequality `P ≤ P'` between monoidal properties of objects induces
a monoidal functor between full monoidal subcategories.  -/
CategoryTheory.ObjectProperty.instMonoidalFullSubcategoryιOfLE : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {P : CategoryTheory.ObjectProperty C} →
        [inst_2 : P.IsMonoidal] →
          {P' : CategoryTheory.ObjectProperty C} →
            [inst_3 : P'.IsMonoidal] → (h : P ≤ P') → (CategoryTheory.ObjectProperty.ιOfLE h).Monoidal
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The underlying lean expression of a coherence isomorphism.  -/
Mathlib.Tactic.BicategoryLike.CoherenceHom.e : Mathlib.Tactic.BicategoryLike.CoherenceHom → Lean.Expr
-- Mathlib.LinearAlgebra.Contraction
lTensorHomEquivHomLTensor.congr_simp : ∀ (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] [inst_7 : Module.Projective R M] [inst_8 : Module.Finite R M],
  lTensorHomEquivHomLTensor R M P Q = lTensorHomEquivHomLTensor R M P Q
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLE'Map_f_eq : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c'} (φ : K ⟶ L) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i'] {i : ι} (hi : ¬e.BoundaryLE i)
  {i' : ι'} (h : e.f i = i'),
  (HomologicalComplex.truncLE'Map φ e).f i =
    CategoryTheory.CategoryStruct.comp (K.truncLE'XIso e h hi).hom
      (CategoryTheory.CategoryStruct.comp (φ.f i') (L.truncLE'XIso e h hi).inv)
-- Mathlib.CategoryTheory.Subobject.FactorThru
CategoryTheory.Subobject.factorThru_add : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C}
  {P : CategoryTheory.Subobject Y} (f g : X ⟶ Y) (w : P.Factors (f + g)) (wf : P.Factors f) (wg : P.Factors g),
  P.factorThru (f + g) w = P.factorThru f wf + P.factorThru g wg
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.endEquivSectionsFibers.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F],
  CategoryTheory.PreGaloisCategory.endEquivSectionsFibers F = CategoryTheory.PreGaloisCategory.endEquivSectionsFibers F
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.CompletionClientCapabilities.mk.sizeOf_spec : ∀ (completionItem? : Option Lean.Lsp.CompletionItemCapabilities),
  sizeOf { completionItem? := completionItem? } = 1 + sizeOf completionItem?
-- Mathlib.Algebra.GradedMonoid
SetLike.GradeZero.coe_submonoid : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} [inst : SetLike S R] [inst_1 : Monoid R] [inst_2 : AddMonoid ι]
  (A : ι → S) [inst_3 : SetLike.GradedMonoid A], ↑(SetLike.GradeZero.submonoid A) = ↑(A 0)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- `cospan f g` is the functor from the walking cospan hitting `f` and `g`.  -/
CategoryTheory.Limits.cospan : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y Z : C} → (X ⟶ Z) → (Y ⟶ Z) → CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C
-- Mathlib.Data.Finsupp.Single
Finsupp.zipWith_single_single : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_7} {P : Type u_8} [inst : Zero M] [inst_1 : Zero N] [inst_2 : Zero P]
  (f : M → N → P) (hf : f 0 0 = 0) (a : α) (m : M) (n : N),
  (Finsupp.zipWith f hf (fun₀ | a => m) fun₀ | a => n) = fun₀ | a => f m n
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec.eq_1 : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  (M : Matrix m n α) (v : n → α) (x : m), M.mulVec v x = (fun j => M x j) ⬝ᵥ v
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.coe_neg : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {M : Type u_8} {N₂ : Type u_12} [inst : Semiring R₁] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommGroup N₂] [inst_4 : Module R₁ M] [inst_5 : Module R₂ N₂] {σ₁₂ : R₁ →+* R₂}
  (f : M →ₛₗ[σ₁₂] N₂), ⇑(-f) = -⇑f
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mul_le_mul_of_nonneg : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c d : α} [PosMulMono α] [MulPosMono α],
  a ≤ b → c ≤ d → 0 ≤ a → 0 ≤ d → a * c ≤ b * d
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_X_pow_le : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).degree ≤ ↑n