mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.tan_sub_pi : ∀ (x : ℂ), Complex.tan (x - ↑Real.pi) = Complex.tan x
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_mul' : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R},
  p.leadingCoeff * q.leadingCoeff ≠ 0 → (p * q).degree = p.degree + q.degree
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Two equal maps on scalars give rise to an equivariant map for identity  -/
MulActionHom.ofEq : {M : Type u_2} →
  {N : Type u_3} →
    {φ : M → N} →
      {X : Type u_5} →
        [inst : SMul M X] → {Y : Type u_6} → [inst_1 : SMul N Y] → {φ' : M → N} → φ = φ' → (X →ₑ[φ] Y) → X →ₑ[φ'] Y
-- Mathlib.Combinatorics.SimpleGraph.Paths
/-- **Alias** of `SimpleGraph.Walk.edges_cycleBypass_subset_edges`. -/
SimpleGraph.Walk.edges_cycleBypass_subset : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (w : G.Walk v v), w.cycleBypass.edges ⊆ w.edges
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.sumPiLpEquivProdLpPiLp_symm_apply_ofLp : ∀ {𝕜 : Type u_1} [inst : Semiring 𝕜] {ι : Type u_5} {κ : Type u_6} (p : ENNReal) (α : ι ⊕ κ → Type u_7)
  [inst_1 : Fintype ι] [inst_2 : Fintype κ] [inst_3 : Fact (1 ≤ p)]
  [inst_4 : (i : ι ⊕ κ) → SeminormedAddCommGroup (α i)] [inst_5 : (i : ι ⊕ κ) → Module 𝕜 (α i)]
  (a : WithLp p (WithLp p ((i : ι) → α (Sum.inl i)) × WithLp p ((i : κ) → α (Sum.inr i)))) (i : ι ⊕ κ),
  ((PiLp.sumPiLpEquivProdLpPiLp p α).symm a).ofLp i = Sum.rec a.fst.ofLp a.snd.ofLp i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- the second inclusion  -/
CategoryTheory.Functor.PushoutObjObj.inr : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} →
              {X₁ Y₁ : C₁} →
                {f₁ : X₁ ⟶ Y₁} →
                  {X₂ Y₂ : C₂} → {f₂ : X₂ ⟶ Y₂} → (self : F.PushoutObjObj f₁ f₂) → (F.obj X₁).obj Y₂ ⟶ self.pt
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
/-- Convert a `MatchResult` into an `Array` of `Array`s. Each `Array` corresponds to one pattern.
The better matching patterns are at the start of the outer array.
For each inner array, the entries are ordered in the order they were inserted.
 -/
Lean.Meta.RefinedDiscrTree.MatchResult.flatten : {α : Type} → Lean.Meta.RefinedDiscrTree.MatchResult α → Array (Array α)
-- Mathlib.Algebra.Group.Units.Defs
AddUnits.instSubNegAddMonoid.eq_1 : ∀ {α : Type u} [inst : AddMonoid α],
  AddUnits.instSubNegAddMonoid =
    { toAddMonoid := AddUnits.instAddMonoid, toNeg := AddUnits.instNeg, toSub := AddUnits.instSub,
      zsmul := fun n a =>
        match n, a with
        | Int.ofNat n, a => n • a
        | Int.negSucc n, a => -(n.succ • a),
      sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯ }
-- Mathlib.Data.Matrix.Basic
Matrix.instAlgebra : {n : Type u_3} →
  {R : Type u_7} →
    {α : Type u_11} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : CommSemiring R] → [inst_3 : Semiring α] → [Algebra R α] → Algebra R (Matrix n n α)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_9.eq_1 : ∀ (motive : Std.Tactic.BVDecide.BVBinOp → Sort u_1) (h_1 : Unit → motive Std.Tactic.BVDecide.BVBinOp.and)
  (h_2 : Unit → motive Std.Tactic.BVDecide.BVBinOp.or) (h_3 : Unit → motive Std.Tactic.BVDecide.BVBinOp.xor)
  (h_4 : Unit → motive Std.Tactic.BVDecide.BVBinOp.add) (h_5 : Unit → motive Std.Tactic.BVDecide.BVBinOp.mul)
  (h_6 : Unit → motive Std.Tactic.BVDecide.BVBinOp.udiv) (h_7 : Unit → motive Std.Tactic.BVDecide.BVBinOp.umod),
  (match Std.Tactic.BVDecide.BVBinOp.and with
    | Std.Tactic.BVDecide.BVBinOp.and => h_1 ()
    | Std.Tactic.BVDecide.BVBinOp.or => h_2 ()
    | Std.Tactic.BVDecide.BVBinOp.xor => h_3 ()
    | Std.Tactic.BVDecide.BVBinOp.add => h_4 ()
    | Std.Tactic.BVDecide.BVBinOp.mul => h_5 ()
    | Std.Tactic.BVDecide.BVBinOp.udiv => h_6 ()
    | Std.Tactic.BVDecide.BVBinOp.umod => h_7 ()) =
    h_1 ()
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Membership in a free monoid element  -/
FreeAddMonoid.mem : {α : Type u_1} → FreeAddMonoid α → α → Prop
-- Lean.Elab.Quotation
/-- In a single match step, we match the first discriminant against the "head" of the first pattern of the first
alternative. This datatype describes what kind of check this involves, which helps other patterns decide if
they are covered by the same check and don't have to be checked again (see also `MatchResult`).  -/
Lean.Elab.Term.Quotation.HeadCheck : Type
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.toSubMulAction_injective : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Function.Injective Submodule.toSubMulAction
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Poly.cancelAux : ℕ →
  Nat.Internal.Linear.Poly →
    Nat.Internal.Linear.Poly →
      Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly × Nat.Internal.Linear.Poly
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_gcd_cert.eq_2 : ∀ (a b : ℤ) (p : Lean.Grind.CommRing.Poly) (g k : ℤ) (v : Lean.Grind.CommRing.Mon) (p_3 : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.eq_gcd_cert a b (Lean.Grind.CommRing.Poly.num g) (Lean.Grind.CommRing.Poly.add k v p_3) p = false
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple_smul_iff : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : Module.End K M}
  {t : K}, t ≠ 0 → ((t • f).IsSemisimple ↔ f.IsSemisimple)
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- `reflectsLimitsOfSize_shrink.{w w'} F` tries to obtain `reflectsLimitsOfSize.{w w'} F`
from some other `reflectsLimitsOfSize F`.
 -/
CategoryTheory.Limits.reflectsLimitsOfSize_shrink : ∀ {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.Limits.ReflectsLimitsOfSize.{max w w₂, max w' w₂', v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsLimitsOfSize.{w, w', v₁, v₂, u₁, u₂} F
-- Init.Meta.Defs
Lean.isIdFirstAscii : UInt8 → Bool
-- Init.Data.Option.Lemmas
Option.max_join_right : ∀ {α : Type u_1} [inst : Max α] {o : Option α} {o' : Option (Option α)}, o ⊔ o'.join = (some o ⊔ o').get ⋯
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : CategoryTheory.Functor Cᵒᵖ (Type v)}
  {F G : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)} (η : F ⟶ G)
  (x : Cᵒᵖ),
  (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafMap₁ η).app x =
    TypeCat.ofHom (CategoryTheory.OverPresheafAux.YonedaCollection.map₁ η)
-- Mathlib.RingTheory.TwoSidedIdeal.BigOperators
TwoSidedIdeal.finsuppProd_mem : ∀ {R : Type u_1} [inst : CommRing R] (I : TwoSidedIdeal R) {ι : Type u_2} {β : Type u_3} [inst_1 : Zero β]
  (h : ι → β → R) {f : ι →₀ β}, (∃ i ∈ f.support, h i (f i) ∈ I) → f.prod h ∈ I
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp.instBraided : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.CartesianMonoidalCategory D] →
            [inst_4 : CategoryTheory.BraidedCategory C] →
              [inst_5 : CategoryTheory.BraidedCategory D] →
                (F : CategoryTheory.Functor C D) → [inst_6 : F.Braided] → F.mapGrp.Braided
-- Mathlib.AlgebraicGeometry.EllipticCurve.ModelsWithJ
WeierstrassCurve.ofJ_1728_of_two_ne_zero : ∀ {F : Type u_2} [inst : Field F] [inst_1 : DecidableEq F],
  2 ≠ 0 → WeierstrassCurve.ofJ 1728 = WeierstrassCurve.ofJ1728 F
-- Mathlib.CategoryTheory.Sites.Hypercover.Saturate
/-- For a presheaf of types, sections over the multifork associated to `E.saturate` are equivalent
to compatible families.  -/
CategoryTheory.PreZeroHypercover.sectionsSaturateEquiv : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {S : C} →
      (E : CategoryTheory.PreZeroHypercover S) →
        (F : CategoryTheory.Functor Cᵒᵖ (Type u_3)) →
          (E.saturate.multicospanIndex F).sections ≃ Subtype (CategoryTheory.Presieve.Arrows.Compatible F E.f)
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_self : ∀ {V : Type u_1} {G : SimpleGraph V} {v : V}, G.edist v v = 0
-- Mathlib.CategoryTheory.Limits.Preserves.Filtered
/-- Reflecting cofiltered limits at any universe implies reflecting cofiltered limits at universe `0`.
 -/
CategoryTheory.Limits.reflectsSmallestCofilteredLimits_of_reflectsCofilteredLimits : ∀ {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.Limits.ReflectsCofilteredLimitsOfSize.{w', w, v₁, v₂, u₁, u₂} F],
  CategoryTheory.Limits.ReflectsCofilteredLimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.univ_add_of_zero_mem : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {t : Finset α} [inst_2 : Fintype α],
  0 ∈ t → Finset.univ + t = Finset.univ
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.Trident.IsLimit.hom_ext : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : J → (X ⟶ Y)} [Nonempty J]
  {s : CategoryTheory.Limits.Trident f} (hs : CategoryTheory.Limits.IsLimit s) {W : C} {k l : W ⟶ s.pt},
  CategoryTheory.CategoryStruct.comp k s.ι = CategoryTheory.CategoryStruct.comp l s.ι → k = l
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- If `M` is the zero module, then the identity map of `M` is the zero map.  -/
LinearMap.identityMapOfZeroModuleIsZero : ∀ {R₁ : Type u_2} {M : Type u_8} [inst : Semiring R₁] [inst_1 : AddCommMonoid M] [inst_2 : Module R₁ M]
  [Subsingleton M], LinearMap.id = 0
-- Mathlib.Order.Minimal
minimal_mem_image_antitone_iff : ∀ {α : Type u_2} {β : Type u_3} {a : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  a ∈ s →
    (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) →
      (Minimal (fun x => x ∈ f '' s) (f a) ↔ Maximal (fun x => x ∈ s) a)
-- Mathlib.CategoryTheory.Limits.Filtered
CategoryTheory.Limits.HasFilteredColimitsOfSize.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  (∀ (I : Type w) [inst_1 : CategoryTheory.Category.{w', w} I] [CategoryTheory.IsFiltered I],
      CategoryTheory.Limits.HasColimitsOfShape I C) →
    CategoryTheory.Limits.HasFilteredColimitsOfSize.{w', w, v, u} C
-- Std.Time.DateTime.PlainDateTime
/-- Subtracts a `Second.Offset` from a `PlainDateTime`, adjusting the minute, hour, and date if the seconds underflow.
 -/
Std.Time.PlainDateTime.subSeconds : Std.Time.PlainDateTime → Std.Time.Second.Offset → Std.Time.PlainDateTime
-- Mathlib.Algebra.Jordan.Basic
_private.Mathlib.Algebra.Jordan.Basic.0.termL : Lean.ParserDescr
-- Mathlib.Data.Num.Lemmas
PosNum.cast_bit1 : ∀ {α : Type u_1} [inst : One α] [inst_1 : Add α] (n : PosNum), ↑n.bit1 = ↑n + ↑n + 1
-- Init.Data.Slice.Array.Lemmas
Subarray.toList_mkSlice_rco : ∀ {α : Type u_1} {xs : Subarray α} {lo hi : ℕ},
  Std.Slice.toList (Std.Rco.Sliceable.mkSlice xs lo...hi) = List.drop lo (List.take hi (Std.Slice.toList xs))
-- Mathlib.GroupTheory.Index
Subgroup.index_pi : ∀ {G : Type u_1} [inst : Group G] {ι : Type u_3} [inst_1 : Fintype ι] (H : ι → Subgroup G),
  (Subgroup.pi Set.univ H).index = ∏ i, (H i).index
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
ContinuousMap.UniqueHom.mk : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : MetricSpace R]
  [inst_3 : IsTopologicalSemiring R] [inst_4 : ContinuousStar R] [inst_5 : Ring A] [inst_6 : StarRing A]
  [inst_7 : TopologicalSpace A] [inst_8 : Algebra R A],
  (∀ (s : Set R) [CompactSpace ↑s] (φ ψ : C(↑s, R) →⋆ₐ[R] A),
      Continuous ⇑φ →
        Continuous ⇑ψ →
          φ (ContinuousMap.restrict s (ContinuousMap.id R)) = ψ (ContinuousMap.restrict s (ContinuousMap.id R)) →
            φ = ψ) →
    ContinuousMap.UniqueHom R A
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.HasCodetector.hasCoseparator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasCoequalizers C]
  [CategoryTheory.HasCodetector C], CategoryTheory.HasCoseparator C
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ D` reflects finite products, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` reflects finite
coproducts.  -/
CategoryTheory.Limits.reflectsFiniteCoproducts_op : ∀ {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.Limits.ReflectsFiniteProducts F],
  CategoryTheory.Limits.ReflectsFiniteCoproducts F.op
-- Mathlib.AlgebraicTopology.SimplicialSet.Dimension
SSet.hasDimensionLT_of_mono : ∀ {X Y : SSet} (f : X ⟶ Y) [CategoryTheory.Mono f] (d : ℕ) [Y.HasDimensionLT d], X.HasDimensionLT d
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.specializes_of_subset_closure : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s t : Set α}, s ⊆ t → t ⊆ closure s → s ⤳ t
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
AddSubmonoid.op_iInf : ∀ {ι : Sort u_1} {M : Type u_2} [inst : AddZeroClass M] (S : ι → AddSubmonoid M), (iInf S).op = ⨅ i, (S i).op
-- Mathlib.Data.Multiset.Sort
Multiset.map_sort : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Multiset α) (r : α → α → Prop) [inst : DecidableRel r]
  [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r] [inst_3 : Std.Total r] (r' : β → β → Prop) [inst_4 : DecidableRel r']
  [inst_5 : IsTrans β r'] [inst_6 : Std.Antisymm r'] [inst_7 : Std.Total r'],
  (∀ a ∈ s, ∀ b ∈ s, r a b ↔ r' (f a) (f b)) → List.map f (s.sort r) = (Multiset.map f s).sort r'
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivAt.differentiableAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E}, HasFDerivAt f f' x → DifferentiableAt 𝕜 f x
-- Init.Data.UInt.Lemmas
UInt32.succ_mul : ∀ {a b : UInt32}, (a + 1) * b = a * b + b
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {he : t ≠ ∅} {fallback : α}, t.getKeyD (t.minKey he) fallback = t.minKey he
-- Mathlib.Algebra.GCDMonoid.Nat
Int.coe_gcd : ∀ (i j : ℤ), ↑(i.gcd j) = gcd i j
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.map_injective : ∀ {R : Type u} [inst : CommRing R] {A : Type v} [inst_1 : CommRing A] {f : R →+* A},
  Function.Injective ⇑f → Function.Injective fun W => W.map f
-- Std.Data.DTreeMap.Internal.Model
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.contains' : {α : Type u} → {β : α → Type v} → [Ord α] → (α → Ordering) → Std.DTreeMap.Internal.Impl α β → Bool
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  k ∉ m₂ → (m₁ ∩ m₂).get? k = none
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.truncLT_add : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] [inst_2 : DecidableLT Γ] (c : Γ)
  (x y : HahnSeries Γ R), (HahnSeries.truncLT c) (x + y) = (HahnSeries.truncLT c) x + (HahnSeries.truncLT c) y
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
_private.Mathlib.CategoryTheory.Localization.Monoidal.Basic.0.CategoryTheory.termL' : Lean.ParserDescr
-- Mathlib.Analysis.Analytic.Constructions
/-- Eta-expanded form of `AnalyticAt.sub` -/
AnalyticAt.fun_sub : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  AnalyticAt 𝕜 f x → AnalyticAt 𝕜 g x → AnalyticAt 𝕜 (fun i => f i - g i) x
-- Mathlib.Data.Matrix.Mul
dotProduct.eq_1 : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : Mul α] [inst_2 : AddCommMonoid α] (v w : m → α),
  v ⬝ᵥ w = ∑ i, v i * w i
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
/-- **Alias** of `BoundedContinuousFunction.abs_sub_coe_le_dist`. -/
BoundedContinuousFunction.abs_diff_coe_le_dist : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f g : BoundedContinuousFunction α β) {x : α}, ‖f x - g x‖ ≤ dist f g
-- Init.System.IO
_private.Init.System.IO.0.IO.FS.Stream.readBinToEndInto.loop : IO.FS.Stream → ByteArray → IO ByteArray
-- Mathlib.Data.Set.Lattice
Set.iUnion_coe_set : ∀ {α : Type u_12} {β : Type u_13} (s : Set α) (f : ↑s → Set β), ⋃ i, f i = ⋃ i, ⋃ (h : i ∈ s), f ⟨i, h⟩
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Λ'.Supports.eq_5 : ∀ (S : Finset Turing.PartrecToTM2.Λ') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.Λ'.Supports S q.copy = Turing.PartrecToTM2.Λ'.Supports S q
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_abs_left : ∀ {α : Type u_1} {F : Type u_4} [inst : Norm F] {g : α → F} {l : Filter α} {u : α → ℝ},
  (fun x => |u x|) =o[l] g ↔ u =o[l] g
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionAssocIso : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (x x_1 : Cᴹᵒᵖ) (x_2 : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso x x_1 x_2 =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso x_2 x_1.unmop x.unmop
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.intCoe_one : ∀ {R : Type u_1} [inst : AddGroupWithOne R], ↑1 = 1
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_ne_nil_iff : ∀ {m n : ℤ}, (m<...=n).toArray ≠ #[] ↔ m < n
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- An orthonormal family of vectors whose span has trivial orthogonal complement is a Hilbert
basis.  -/
HilbertBasis.mkOfOrthogonalEqBot : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    [inst : RCLike 𝕜] →
      {E : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : InnerProductSpace 𝕜 E] →
            [CompleteSpace E] →
              {v : ι → E} → Orthonormal 𝕜 v → (Submodule.span 𝕜 (Set.range v))ᗮ = ⊥ → HilbertBasis ι 𝕜 E
-- Mathlib.RingTheory.WittVector.StructurePolynomial
wittStructureInt.eq_1 : ∀ (p : ℕ) {idx : Type u_2} [hp : Fact (Nat.Prime p)] (Φ : MvPolynomial idx ℤ) (n : ℕ),
  wittStructureInt p Φ n =
    AddMonoidAlgebra.ofCoeff
      (Finsupp.mapRange Rat.num wittStructureInt._proof_1
        (wittStructureRat p ((MvPolynomial.map (Int.castRingHom ℚ)) Φ) n).coeff)
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.inter_sdiff_right_comm`. -/
Set.diff_inter_right_comm : ∀ {α : Type u_1} {s t u : Set α}, (s ∩ t) \ u = s \ u ∩ t
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.sub.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.size_erase_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, (m.erase k).size ≤ m.size
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
RingCon.comap.eq_1 : ∀ {R : Type u_2} {R' : Type u_3} {F : Type u_4} [inst : Add R] [inst_1 : Add R'] [inst_2 : FunLike F R R']
  [inst_3 : AddHomClass F R R'] [inst_4 : Mul R] [inst_5 : Mul R'] [inst_6 : MulHomClass F R R'] (J : RingCon R')
  (f : F), J.comap f = { toCon := Con.comap ⇑f ⋯ J.toCon, add' := ⋯ }
-- Mathlib.Data.Fin.Tuple.Basic
Fin.exists_fin_succ_pi : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u} {P : ((i : Fin (n + 1)) → α i) → Prop}, (∃ x, P x) ↔ ∃ a v, P (Fin.cons a v)
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.restrict_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β] [inst_2 : Preorder β] (s : Set α)
  {f g : MeasureTheory.SimpleFunc α β}, f ≤ g → f.restrict s ≤ g.restrict s
-- Mathlib.Algebra.Lie.Solvable
/-- The `→` direction of this lemma is actually true without the `IsNoetherian` assumption.  -/
LieAlgebra.LieIdeal.solvable_iff_le_radical : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [IsNoetherian R L]
  (I : LieIdeal R L), LieAlgebra.IsSolvable ↥I ↔ I ≤ LieAlgebra.radical R L
-- Mathlib.Data.Bundle
Bundle.TotalSpace.mk_injective : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} (b : B), Function.Injective (Bundle.TotalSpace.mk b)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The ring instance on `WithPreorder R` arising from the ring structure on `R`.  -/
ValuativeRel.instSemiringWithPreorder : {R : Type u_1} → [Semiring R] → Semiring (ValuativeRel.WithPreorder R)
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.x_mk : ∀ {d : ℤ} (x y : ℤ) (prop : x ^ 2 - d * y ^ 2 = 1), (Pell.Solution₁.mk x y prop).x = x
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.instIsTriangulatedLeftOrthogonalOfIsStableUnderShiftInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C] [P.IsStableUnderShift ℤ], P.leftOrthogonal.IsTriangulated
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
/-- The map `X ×[Z] Y ⟶ X × Y` is mono.  -/
CategoryTheory.Limits.mono_pullback_to_prod : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.Mono
    (CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g))
-- Mathlib.Computability.TuringMachine.Computable
/-- A (bundled TM2) Turing machine
with input alphabet equivalent to `Γ₀` and output alphabet equivalent to `Γ₁`.  -/
Turing.TM2ComputableAux : Type → Type → Type 1
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.multicospanShape_R : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X), data.multicospanShape.R = data.I₁'
-- Mathlib.Logic.UnivLE
UnivLE.mk : (∀ (α : Type u), Small.{v, u} α) → UnivLE.{u, v}
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
/-- The inverse of an open partial homeomorphism  -/
OpenPartialHomeomorph.symm : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → OpenPartialHomeomorph X Y → OpenPartialHomeomorph Y X
-- Mathlib.Topology.Maps.Basic
isOpenMap_iff_clusterPt_comap : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f ↔ ∀ (x : X) (l : Filter Y), ClusterPt (f x) l → ClusterPt x (Filter.comap f l)