mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Set.Monotone
MonotoneOn.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] (f : α → β) (s : Set α),
  MonotoneOn f s = ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → a ≤ b → f a ≤ f b
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.Indep.eRk_eq_encard : ∀ {α : Type u_1} {M : Matroid α} {I : Set α}, M.Indep I → M.eRk I = I.encard
-- Init.Data.Slice.List.Lemmas
ListSlice.toList_mkSlice_roi_eq_toList_mkSlice_roo : ∀ {α : Type u_1} {xs : ListSlice α} {lo : ℕ},
  Std.Slice.toList (Std.Roi.Sliceable.mkSlice xs lo<...*) =
    Std.Slice.toList (Std.Roo.Sliceable.mkSlice xs lo<...Std.Slice.size xs)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_opShiftFunctorEquivalence_unitIso_inv_app_unop_assoc : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ)
  {Z : D}
  (h :
    F.obj
        (Opposite.unop
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj
            ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj X))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X).unop) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).unitIso.inv.app
          (Opposite.op (F.obj (Opposite.unop X)))).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D n).map ((CategoryTheory.Functor.commShiftIso F.op n).hom.app X).unop)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Functor.commShiftIso F n).inv.app
            (Opposite.unop ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X)))
          h))
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.MorphismProperty.isLocallyPresentable_isLocal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [CategoryTheory.IsCardinalLocallyPresentable C κ]
  [CategoryTheory.MorphismProperty.IsSmall.{w, v, u} W],
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → CategoryTheory.IsCardinalPresentable X κ ∧ CategoryTheory.IsCardinalPresentable Y κ) →
    CategoryTheory.IsCardinalLocallyPresentable W.isLocal.FullSubcategory κ
-- Mathlib.Order.Cover
WCovBy.snd : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] {x y : α × β}, x ⩿ y → x.2 ⩿ y.2
-- Mathlib.Topology.Order.Category.AlexDisc
AlexDisc.instHasForgetToTop : CategoryTheory.HasForget₂ AlexDisc TopCat
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.coe_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulZeroOneClass α] [inst_4 : MulZeroOneClass β] [inst_5 : MulZeroOneClass γ] (f : β →*₀o γ) (g : α →*₀o β),
  ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Lean.Server.InfoUtils
Lean.Elab.HoverableInfoPrio.mk : Bool → ℕ → Bool → Bool → Lean.Elab.HoverableInfoPrio
-- Init.Notation
/-- `#guard_panic in cmd` runs `cmd` and succeeds if the command produces a panic message.
This is useful for testing that a command panics without matching the exact (volatile) panic text.
 -/
Lean.guardPanicCmd : Lean.ParserDescr
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.restrict_spanning_iff' : ∀ {α : Type u_2} {M : Matroid α} {R S : Set α}, (M.restrict R).Spanning S ↔ R ∩ M.E ⊆ M.closure S ∧ S ⊆ R
-- Mathlib.Tactic.Translate.Core
/-- `translateLemmas` runs `runAttr` on all elements of `names` and adds translations between
the generated lemmas (the output of `t`).  `names` must be non-empty.  -/
Mathlib.Tactic.Translate.translateLemmas : Mathlib.Tactic.Translate.TranslateData →
  Array Lean.Name →
    String → Mathlib.Tactic.Translate.Config → (Lean.Name → Lean.CoreM (Array Lean.Name)) → Lean.CoreM Unit
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.lintegral_enorm_zero : ∀ {α : Type u_1} {ε'' : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε'']
  [inst_1 : ESeminormedAddMonoid ε''], ∫⁻ (x : α), ‖0‖ₑ ∂μ = 0
-- Mathlib.Data.Seq.Basic
_private.Mathlib.Data.Seq.Basic.0.Stream'.Seq.take.match_1.eq_1 : ∀ {α : Type u_1} (motive : ℕ → Stream'.Seq α → Sort u_2) (x : Stream'.Seq α) (h_1 : (x : Stream'.Seq α) → motive 0 x)
  (h_2 : (n : ℕ) → (s : Stream'.Seq α) → motive n.succ s),
  (match 0, x with
    | 0, x => h_1 x
    | n.succ, s => h_2 n s) =
    h_1 x
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackZeroZeroIso X Y).hom
      CategoryTheory.Limits.prod.fst =
    CategoryTheory.Limits.pullback.fst 0 0
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natIsoSc'.congr_simp : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k),
  HomologicalComplex.natIsoSc' C c i j k hi hk = HomologicalComplex.natIsoSc' C c i j k hi hk
-- Mathlib.Order.WithBot
WithTop.untopD_le_iff : ∀ {α : Type u_1} {a b : α} [inst : LE α] {x : WithTop α}, x ≠ ⊤ → (WithTop.untopD a x ≤ b ↔ x ≤ ↑b)
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `add_tsub_cancel_left` for the equality if `AddLeftReflectLE α`.  -/
add_tsub_le_left : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  a + b - a ≤ b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.find?_toArray_eq_none_iff_not_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  Array.find? (fun x => cmp x.fst k == Ordering.eq) t.toArray = none ↔ k ∉ t
-- Mathlib.Data.Nat.Multiplicity
_private.Mathlib.Data.Nat.Multiplicity.0.Nat.factorial.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.Order.Closure
LowerAdjoint.instCoeFunForall : {α : Type u_1} →
  {β : Type u_4} → [inst : Preorder α] → [inst_1 : Preorder β] → {u : β → α} → CoeFun (LowerAdjoint u) fun x => α → β
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.norm_condExpL2_le : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) (f : ↥(MeasureTheory.Lp E 2 μ)), ‖(MeasureTheory.condExpL2 E 𝕜 hm) f‖ ≤ ‖f‖
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.op_comp : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Y} {g : Y ⟶ Z},
  (CategoryTheory.CategoryStruct.comp f g).op = CategoryTheory.CategoryStruct.comp g.op f.op
-- Mathlib.Order.Cover
CovBy.trans_antisymmRel : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ⋖ b → AntisymmRel (fun x1 x2 => x1 ≤ x2) b c → a ⋖ c
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntry.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a k : α) (v : β k) (es : Std.DHashMap.Internal.AssocList α β)
  (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true),
  Std.DHashMap.Internal.AssocList.getEntry a (Std.DHashMap.Internal.AssocList.cons k v es) h =
    if hka : (k == a) = true then ⟨k, v⟩ else Std.DHashMap.Internal.AssocList.getEntry a es ⋯
-- Mathlib.Order.Category.FinBoolAlg
FinBoolAlg.Iso.mk_hom : ∀ {α β : FinBoolAlg} (e : ↑α.toBoolAlg ≃o ↑β.toBoolAlg),
  (FinBoolAlg.Iso.mk e).hom =
    CategoryTheory.InducedCategory.homMk
      (BoolAlg.ofHom
        (have __src := { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯ };
        { toFun := ⇑e, map_sup' := ⋯, map_inf' := ⋯, map_top' := ⋯, map_bot' := ⋯ }))
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.constMaxEntry!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)],
  t₁.WF → t₂.WF → t₁.Equiv t₂ → Std.DTreeMap.Raw.Const.maxEntry! t₁ = Std.DTreeMap.Raw.Const.maxEntry! t₂
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.snd : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {M' : Type u_3} [inst_1 : Zero M'] {f : α → M × M'},
  Function.HasFiniteSupport f → Function.HasFiniteSupport fun a => (f a).2
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.toArray_eq_match_step.match_1.splitter : {α β : Type u_1} →
  {m : Type u_1 → Type u_2} →
    (motive : Std.IterStep (Std.IterM m β) β → Sort u_3) →
      (x : Std.IterStep (Std.IterM m β) β) →
        ((it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out)) →
          ((it' : Std.IterM m β) → motive (Std.IterStep.skip it')) → (Unit → motive Std.IterStep.done) → motive x
-- Mathlib.CategoryTheory.Limits.Types.Images
CategoryTheory.Limits.Types.instHasImage : ∀ {α β : Type u} (f : α ⟶ β), CategoryTheory.Limits.HasImage f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color : Type
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
LinearMap.finrank_le_of_isSMulRegular : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {S : Type u_2} [inst_4 : CommSemiring S] [inst_5 : Algebra S R] [inst_6 : Module S M] [IsScalarTower S R M]
  (L L' : Submodule R M) [Module.Finite R ↥L'] {s : S},
  IsSMulRegular M s → (∀ x ∈ L, s • x ∈ L') → Module.finrank R ↥L ≤ Module.finrank R ↥L'
-- Mathlib.RingTheory.PowerSeries.PiTopology
/-- Coefficients are uniformly continuous  -/
PowerSeries.WithPiTopology.uniformContinuous_coeff : ∀ (R : Type u_1) [inst : UniformSpace R] [inst_1 : Semiring R] (d : ℕ),
  UniformContinuous fun f => (PowerSeries.coeff d) f
-- Init.Data.Array.Zip
Array.zipWith_append : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {as as' : Array α} {bs bs' : Array β},
  as.size = bs.size → Array.zipWith f (as ++ as') (bs ++ bs') = Array.zipWith f as bs ++ Array.zipWith f as' bs'
-- Mathlib.Data.Nat.Pairing
Set.iUnion_unpair : ∀ {α : Type u_1} (f : ℕ → ℕ → Set α), ⋃ n, f (Nat.unpair n).1 (Nat.unpair n).2 = ⋃ i, ⋃ j, f i j
-- Mathlib.Data.Analysis.Topology
Ctop.Realizer.σ : {α : Type u_6} → [T : TopologicalSpace α] → Ctop.Realizer α → Type u_5
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
_private.Mathlib.CategoryTheory.Monoidal.Braided.Reflection.0.CategoryTheory.Monoidal.Reflective.adjRetraction_is_retraction : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory D]
  [inst_3 : CategoryTheory.SymmetricCategory D] [inst_4 : CategoryTheory.MonoidalClosed D]
  {R : CategoryTheory.Functor C D} [inst_5 : R.Faithful] [inst_6 : R.Full] {L : CategoryTheory.Functor D C}
  (adj : L ⊣ R) (c : C) (d : D)
  [inst_7 :
    CategoryTheory.IsIso
      (L.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app (d ⟹ R.obj c)) (adj.unit.app d)))],
  CategoryTheory.CategoryStruct.comp (adj.unit.app (d ⟹ R.obj c))
      (CategoryTheory.Monoidal.Reflective.adjRetraction✝ adj c d) =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id D).obj (d ⟹ R.obj c))
-- Mathlib.Algebra.Category.HopfAlgCat.Basic
CategoryTheory.Iso.toHopfAlgEquiv_symm : ∀ {R : Type u} [inst : CommRing R] {X Y : HopfAlgCat R} (e : X ≅ Y), e.symm.toHopfAlgEquiv = e.toHopfAlgEquiv.symm
-- Mathlib.Topology.Order.LeftRight
nhdsWithin_Iic_neBot : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : Preorder α] {a b : α}, b ≤ a → (nhdsWithin b (Set.Iic a)).NeBot
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.eval_T_real_eq_one_iff : ∀ {n : ℕ},
  n ≠ 0 →
    ∀ (x : ℝ), Polynomial.eval x (Polynomial.Chebyshev.T ℝ ↑n) = 1 ↔ ∃ k ≤ n, Even k ∧ x = Real.cos (↑k * Real.pi / ↑n)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.HaveLebesgueDecomposition.mk : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  (∃ p, Measurable p.2 ∧ p.1.MutuallySingular ν ∧ μ = p.1 + ν.withDensity p.2) → μ.HaveLebesgueDecomposition ν
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.SharedExprs.ordEqExpr : Lean.Meta.Sym.SharedExprs → Lean.Expr
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
/-- The inclusion of *alternating* continuous multilinear maps into continuous multilinear maps
as a continuous linear map.  -/
ContinuousAlternatingMap.toContinuousMultilinearMapCLM : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {ι : Type u_4} →
        [inst : NormedField 𝕜] →
          [inst_1 : AddCommGroup E] →
            [inst_2 : Module 𝕜 E] →
              [inst_3 : TopologicalSpace E] →
                [inst_4 : AddCommGroup F] →
                  [inst_5 : Module 𝕜 F] →
                    [inst_6 : TopologicalSpace F] →
                      [inst_7 : IsTopologicalAddGroup F] →
                        (R : Type u_5) →
                          [inst_8 : Semiring R] →
                            [inst_9 : Module R F] →
                              [inst_10 : ContinuousConstSMul R F] →
                                [inst_11 : SMulCommClass 𝕜 R F] →
                                  E [⋀^ι]→L[𝕜] F →L[R] ContinuousMultilinearMap 𝕜 (fun x => E) F
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_zero_mul_updateCol_zero : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq l] [inst_1 : DecidableEq n]
  [inst_2 : Fintype m] [inst_3 : NonUnitalNonAssocSemiring α] (i : l) (r : m → α) (j : n) (c : m → α),
  Matrix.updateRow 0 i r * Matrix.updateCol 0 j c = Matrix.single i j (r ⬝ᵥ c)
-- Mathlib.Data.ENNReal.Operations
ENNReal.iInf_add_iInf : ∀ {ι : Sort u_1} {f g : ι → ENNReal}, (∀ (i j : ι), ∃ k, f k + g k ≤ f i + g j) → iInf f + iInf g = ⨅ a, f a + g a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.GrpObj.comp_div : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {G X Y : C} [inst_2 : CategoryTheory.GrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G),
  CategoryTheory.CategoryStruct.comp f (g / h) =
    CategoryTheory.CategoryStruct.comp f g / CategoryTheory.CategoryStruct.comp f h
-- Mathlib.Analysis.InnerProductSpace.Orientation
Orientation.volumeForm_apply_le : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (v : Fin n → E), o.volumeForm v ≤ ∏ i, ‖v i‖
-- Mathlib.Order.Antichain
IsAntichain.eq' : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsAntichain r s → ∀ {a b : α}, a ∈ s → b ∈ s → r b a → a = b
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.eraseIdx.eq_def : ∀ {α : Type u} (xs : Array α) (i : ℕ) (h : i < xs.size),
  xs.eraseIdx i h =
    if h' : i + 1 < xs.size then
      let xs' := xs.swap (i + 1) i h' h;
      xs'.eraseIdx (i + 1) ⋯
    else xs.pop
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsTangent.notMem_of_dist_lt : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {as : AffineSubspace ℝ P},
  s.IsTangent as → ∀ {p : P}, dist p s.center < s.radius → p ∉ as
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.comp_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C}
  {X Y Z : J.ZeroHypercover S} (f : X.Hom Y.toPreZeroHypercover) (g : Y.Hom Z.toPreZeroHypercover) (a : X.I₀),
  (CategoryTheory.CategoryStruct.comp f g).s₀ a = g.s₀ (f.s₀ a)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.left_inv : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  (X : C) [self : CategoryTheory.GrpObj X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift CategoryTheory.GrpObj.inv (CategoryTheory.CategoryStruct.id X))
      CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X) CategoryTheory.MonObj.one
-- Lean.MetavarContext
Lean.LocalInstance.mk.sizeOf_spec : ∀ (className : Lean.Name) (fvar : Lean.Expr),
  sizeOf { className := className, fvar := fvar } = 1 + sizeOf className + sizeOf fvar
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt8.size ≤ n →
    (UInt8.ofNatClamp n).toUInt64 = UInt64.ofNatLT (UInt8.size - 1) UInt8.toUInt64_ofNatClamp_of_le._proof_1
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAlgebra : {n : Type u_2} →
  {R : Type u_3} →
    {A : Type u_5} →
      [inst : Fintype n] →
        [inst_1 : DecidableEq n] →
          [inst_2 : CommSemiring R] → [inst_3 : Semiring A] → [Algebra R A] → Algebra R (CStarMatrix n n A)
-- Mathlib.Data.Set.Basic
Set.inter_eq_inter_iff_right : ∀ {α : Type u} {s t u : Set α}, s ∩ u = t ∩ u ↔ t ∩ u ⊆ s ∧ s ∩ u ⊆ t
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If `F : ι → X → α` is an equicontinuous family of functions,
`f : X → α` is a continuous function, and `l` is a filter on `ι`,
then `{x | Filter.Tendsto (F · x) l (𝓝 (f x))}` is a closed set.  -/
Equicontinuous.isClosed_setOfPred_tendsto : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {l : Filter ι}
  {F : ι → X → α} {f : X → α},
  Equicontinuous F → Continuous f → IsClosed {x | Filter.Tendsto (fun x_1 => F x_1 x) l (nhds (f x))}
-- Mathlib.CategoryTheory.Action.Basic
Action.Hom.mk.inj : ∀ {V : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} V} {G : Type u_2} {inst_1 : Monoid G} {M N : Action V G}
  {hom : M.V ⟶ N.V}
  {comm :
    autoParam
      (∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) hom = CategoryTheory.CategoryStruct.comp hom (N.ρ g))
      Action.Hom.comm._autoParam}
  {hom_1 : M.V ⟶ N.V}
  {comm_1 :
    autoParam
      (∀ (g : G), CategoryTheory.CategoryStruct.comp (M.ρ g) hom_1 = CategoryTheory.CategoryStruct.comp hom_1 (N.ρ g))
      Action.Hom.comm._autoParam},
  { hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 } → hom = hom_1
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
isDedekindDomain_iff_mul_inv_cancel : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K]
  [inst_3 : IsFractionRing A K] [inst_4 : IsDomain A],
  IsDedekindDomain A ↔ ∀ (I : FractionalIdeal (nonZeroDivisors A) K), I ≠ ⊥ → I * I⁻¹ = 1
-- Mathlib.Topology.Algebra.Group.GroupTopology
GroupTopology.instSemilatticeInf : {α : Type u} → [inst : Group α] → SemilatticeInf (GroupTopology α)
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.totalSpaceMk_isInducing : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (self : FiberPrebundle F E) (b : B),
  Topology.IsInducing (↑(self.pretrivializationAt b) ∘ Bundle.TotalSpace.mk b)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_carrier : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] {s : StarSubalgebra R A} {x : A},
  x ∈ s.carrier ↔ x ∈ s
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.isSimplyLaced_E₈ : CartanMatrix.E₈.IsSimplyLaced
-- Lean.Data.Lsp.Extra
Lean.Lsp.PlainTermGoalParams.mk.inj : ∀ {toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams},
  { toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 } →
    toTextDocumentPositionParams = toTextDocumentPositionParams_1
-- Lean.Data.JsonRpc
Lean.JsonRpc.Notification.mk.inj : ∀ {α : Type u} {method : String} {param : α} {method_1 : String} {param_1 : α},
  { method := method, param := param } = { method := method_1, param := param_1 } → method = method_1 ∧ param = param_1
-- Mathlib.Dynamics.Transitive
IsOpen.dense_iUnion_vadd : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α]
  [h : AddAction.IsTopologicallyTransitive M α] {U : Set α}, IsOpen U → U.Nonempty → Dense (⋃ m, m +ᵥ U)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_ne_zero_of_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α}, b ≠ 0 → gcd a b ≠ 0
-- Mathlib.FieldTheory.Perfect
/-- The `p`-th power automorphism for a perfect monoid.  -/
powMulEquiv : (M : Type u_1) → (p : ℕ) → [inst : CommMonoid M] → [PerfectRing M p] → M ≃* M
-- Mathlib.FieldTheory.CardinalEmb
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.«termE⟮<_⟯» : Lean.ParserDescr
-- Lean.LibrarySuggestions.Basic
/-- The trivial premise selector, which returns no suggestions.
 -/
Lean.LibrarySuggestions.empty : Lean.LibrarySuggestions.Selector
-- Mathlib.Analysis.Distribution.TemperateGrowth
Function.HasTemperateGrowth.neg : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] {f : E → F}, Function.HasTemperateGrowth f → Function.HasTemperateGrowth (-f)
-- Mathlib.Analysis.Normed.Group.Bounded
comap_norm_atTop' : ∀ {E : Type u_2} [inst : SeminormedGroup E], Filter.comap norm Filter.atTop = Bornology.cobounded E
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- For each `1 ≤ p < ∞`, the linear span of the monomials `mFourier n` is dense in the `Lᵖ` space
of functions on `UnitAddTorus d`.  -/
UnitAddTorus.span_mFourierLp_closure_eq_top : ∀ {d : Type u_1} [inst : Fintype d] {p : ENNReal} [inst_1 : Fact (1 ≤ p)],
  p ≠ ⊤ → (Submodule.span ℂ (Set.range (UnitAddTorus.mFourierLp p))).topologicalClosure = ⊤
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The diagram `S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃` for any
`S : SnakeInput C`.  -/
CategoryTheory.ShortComplex.SnakeInput.composableArrows : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → CategoryTheory.ShortComplex.SnakeInput C → CategoryTheory.ComposableArrows C 5