mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
HomotopyCategory.instIsTriangulatedClosed₃IntUpPlus : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproducts C],
  (HomotopyCategory.plus C).IsTriangulatedClosed₃
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- Support of a cycle is nonempty  -/
Equiv.Perm.IsCycle.nonempty_support : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] {g : Equiv.Perm α}, g.IsCycle → g.support.Nonempty
-- Init.Data.List.Sublist
List.IsInfix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ → l₁.reverse <:+: l₂.reverse
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Occurrence sets are open.  -/
SymbolicDynamics.FullShift.isOpen_mulOccursInAt : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : Monoid G]
  [IsLeftCancelMul G] [DiscreteTopology A] (p : SymbolicDynamics.FullShift.Pattern A G) (g : G),
  IsOpen {x | p.mulOccursInAt x g}
-- Mathlib.Order.Max
isMin_toDual_iff : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMin (OrderDual.toDual a) ↔ IsMax a
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- **Alias** of `mul_le_mul_iff_left₀`. -/
mul_le_mul_iff_of_pos_right : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] {a b c : α} [MulPosMono α] [MulPosReflectLE α],
  0 < a → (b * a ≤ c * a ↔ b ≤ c)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
Rat.valuation_le_one_iff_den : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Algebra R ℚ] [inst_3 : IsFractionRing R ℚ]
  {𝔭 : IsDedekindDomain.HeightOneSpectrum R} {x : ℚ},
  (IsDedekindDomain.HeightOneSpectrum.valuation ℚ 𝔭) x ≤ 1 ↔ ↑x.den ∉ 𝔭.asIdeal
-- Mathlib.NumberTheory.Padics.Measure.Basic
/-- For profinite spaces, the two product structures on measures agree.  -/
AbstractMeasure.prodMk_eq_prodMk' : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : CommRing R] [inst_3 : TopologicalSpace R] [inst_4 : IsTopologicalRing R] (μ : AbstractMeasure X R R)
  (ν : AbstractMeasure Y R R) [inst_5 : CompactSpace X] [inst_6 : CompactSpace Y] [inst_7 : T2Space X]
  [inst_8 : T2Space Y] [TotallyDisconnectedSpace X] [T0Space R],
  (AbstractMeasure.prodMk μ) ν = (AbstractMeasure.prodMk' μ) ν
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.id_union : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {s t : Set M},
  LinearIndepOn R id s →
    LinearIndepOn R id t → Disjoint (Submodule.span R s) (Submodule.span R t) → LinearIndepOn R id (s ∪ t)
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_sub : ∀ {a b c : ℤ}, a ∣ b → a ∣ c → a ∣ b - c
-- Mathlib.Algebra.Polynomial.Eval.Coeff
/-- The polynomial ring over a finite product of rings is isomorphic to
the product of polynomial rings over individual rings.  -/
Polynomial.piEquiv : {ι : Type u_2} →
  [Finite ι] →
    (R : ι → Type u_1) → [inst : (i : ι) → Semiring (R i)] → Polynomial ((i : ι) → R i) ≃+* ((i : ι) → Polynomial (R i))
-- Mathlib.Order.BoundedOrder.Basic
OrderDual.instBoundedOrder : (α : Type u) → [inst : LE α] → [BoundedOrder α] → BoundedOrder αᵒᵈ
-- Mathlib.Topology.Order.IntermediateValue
Continuous.strictAnti_of_inj_boundedOrder : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  [inst_7 : BoundedOrder α] {f : α → δ}, Continuous f → f ⊤ ≤ f ⊥ → Function.Injective f → StrictAnti f
-- Mathlib.Probability.Kernel.Disintegration.Basic
MeasureTheory.Measure.IsCondKernel.disintegrate : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} {ρ : MeasureTheory.Measure (α × Ω)}
  {ρCond : ProbabilityTheory.Kernel α Ω} [self : ρ.IsCondKernel ρCond], ρ.fst.compProd ρCond = ρ
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonCreateFile : Lean.ToJson Lean.Lsp.CreateFile
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
/-- The red and the blue arrows in ![this diagram](https://i.imgur.com/0GiBUh6.png) commute.  -/
AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.V (i, j))),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp (D.f i j) U)
      ((D.f i k).c.app
        (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor (D.f i j)).obj U))) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
          (CategoryTheory.Limits.pullback.snd (D.f i j) (D.f i k))
          (Opposite.unop
            (Opposite.op
              ((TopologicalSpace.Opens.map (CategoryTheory.Limits.pullback.fst (D.f i j) (D.f i k)).base).1
                (Opposite.unop (Opposite.op U))))))
        ((D.V (i, k)).presheaf.map (CategoryTheory.eqToHom ⋯)))
-- Mathlib.Probability.Kernel.Composition.MeasureComp
MeasureTheory.Measure.AbsolutelyContinuous.comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ ν : MeasureTheory.Measure α}
  {κ η : ProbabilityTheory.Kernel α β},
  μ.AbsolutelyContinuous ν →
    (∀ᵐ (a : α) ∂μ, (κ a).AbsolutelyContinuous (η a)) → (μ.bind ⇑κ).AbsolutelyContinuous (ν.bind ⇑η)
-- Mathlib.Algebra.Ring.Opposite
MulOpposite.instCommSemiring : {R : Type u_1} → [CommSemiring R] → CommSemiring Rᵐᵒᵖ
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
/-- An indexed set of vectors is linearly dependent iff there is a nontrivial
`Finsupp.linearCombination` of the vectors that is zero.  -/
linearDepOn_iff' : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {v : ι → M},
  ¬LinearIndepOn R v s ↔ ∃ f ∈ Finsupp.supported R R s, (Finsupp.linearCombination R v) f = 0 ∧ f ≠ 0
-- Init.Data.Array.Lemmas
Array.foldl_flatten' : ∀ {β : Type u_1} {α : Type u_2} {f : β → α → β} {b : β} {xss : Array (Array α)} {stop : ℕ},
  stop = xss.flatten.size → Array.foldl f b xss.flatten 0 stop = Array.foldl (fun b xs => Array.foldl f b xs) b xss
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
RootPairing.coxeterWeightIn_eq_zero_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [CharZero R]
  [inst_6 : P.IsCrystallographic] (i j : ι) [IsDomain R], P.coxeterWeightIn ℤ i j = 0 ↔ P.pairingIn ℤ i j = 0
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryFan.π_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryFan X Y),
  s.π.app { as := CategoryTheory.Limits.WalkingPair.left } = s.fst
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_right_zero : ∀ {n : ℕ} [inst : NeZero n] {i : Fin n}, i.predAbove 0 = 0
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseQuarterLong : Std.Time.DateFormatSymbols → Std.Internal.Parsec.String.Parser Std.Time.Month.Quarter
-- Mathlib.Algebra.CharP.Two
/-- See `frobenius` for the Frobenius map.  -/
_private.Mathlib.Algebra.CharP.Two.0.CharTwo.sqAddMonoidHom : {R : Type u_1} → [inst : CommSemiring R] → [CharP R 2] → R →+ R
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_insertIfNew_le_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.isEmpty = false →
    ∀ {k : α} {v : β k} {fallback : α}, (cmp ((t.insertIfNew k v).minKeyD fallback) (t.minKeyD fallback)).isLE = true
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.map_update_add : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
  f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y)
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.RightLinear.instIsIsoδᵣ : ∀ {D : Type u_1} {D' : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D'] (F : CategoryTheory.Functor D D') {C : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C] [inst_3 : CategoryTheory.MonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D]
  [inst_5 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D'] [inst_6 : F.RightLinear C] (c : C) (d : D),
  CategoryTheory.IsIso (CategoryTheory.Functor.OplaxRightLinear.δᵣ F d c)
-- Mathlib.Algebra.Module.GradedModule
DirectSum.gsmulHom_apply_apply : ∀ {ιA : Type u_1} {ιB : Type u_2} (A : ιA → Type u_3) (M : ιB → Type u_4) [inst : AddMonoid ιA] [inst_1 : VAdd ιA ιB]
  [inst_2 : (i : ιA) → AddCommMonoid (A i)] [inst_3 : (i : ιB) → AddCommMonoid (M i)] [inst_4 : GradedMonoid.GMonoid A]
  [inst_5 : DirectSum.Gmodule A M] {i : ιA} {j : ιB} (a : A i) (b : M j),
  ((DirectSum.gsmulHom A M) a) b = GradedMonoid.GSMul.smul a b
-- Init.Data.Vector.Lemmas
/-- Variant of `any_eq_false` in terms of membership rather than an array index.  -/
Vector.any_eq_false' : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n}, xs.any p = false ↔ ∀ x ∈ xs, ¬p x = true
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- Stabilizers in group SubMulAction coincide with stabilizers in the ambient space  -/
SubMulAction.stabilizer_of_subMul : ∀ {R : Type u} {M : Type v} [inst : Group R] [inst_1 : MulAction R M] {p : SubMulAction R M} (m : ↥p),
  MulAction.stabilizer R m = MulAction.stabilizer R ↑m
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceL.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (rs : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l_1 : Std.DTreeMap.Internal.Impl α β) →
      l_1.Balanced →
        Std.DTreeMap.Internal.Impl.BalanceLPrecond l_1.size (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
          Sort u_3)
  (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β)
  (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
      (Std.DTreeMap.Internal.Impl.inner rs k v l r).size)
  (h_1 :
    (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLPrecond Std.DTreeMap.Internal.Impl.leaf.size
            (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
        motive Std.DTreeMap.Internal.Impl.leaf hlb hlr)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr),
  (match Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr => h_1 hlb hlr
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr => h_2 ls lk lv ll lr hlb hlr) =
    h_2 ls lk lv ll lr hlb hlr
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.instCategory.eq_1 : AddGrpCat.instCategory =
  { Hom := fun X Y => X.Hom Y, id := fun X => { hom' := AddMonoidHom.id ↑X },
    comp := fun {X Y Z} f g => { hom' := g.hom'.comp f.hom' }, id_comp := @AddGrpCat.instCategory._proof_1,
    comp_id := @AddGrpCat.instCategory._proof_2, assoc := @AddGrpCat.instCategory._proof_3 }
-- Mathlib.Geometry.Manifold.StructureGroupoid
instCompleteLatticeStructureGroupoid : {H : Type u_1} → [inst : TopologicalSpace H] → CompleteLattice (StructureGroupoid H)
-- Mathlib.GroupTheory.OrderOfElement
isOfFinAddOrder_iff_zsmul_eq_zero : ∀ {G : Type u_6} [inst : SubtractionMonoid G] {x : G}, IsOfFinAddOrder x ↔ ∃ n, n ≠ 0 ∧ n • x = 0
-- Mathlib.Topology.EMetricSpace.Defs
Metric.isClosed_eball_top : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α}, IsClosed (Metric.eball x ⊤)
-- Mathlib.Order.Hom.Bounded
TopHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : LE α] [inst_1 : OrderTop α] [inst_2 : LE β] [inst_3 : OrderTop β]
  [inst_4 : LE γ] [inst_5 : OrderTop γ] (g : BotHom βᵒᵈ γᵒᵈ) (f : BotHom αᵒᵈ βᵒᵈ),
  TopHom.dual.symm (g.comp f) = (TopHom.dual.symm g).comp (TopHom.dual.symm f)
-- Mathlib.Order.CompleteSublattice
CompleteSublattice.sInfClosed' : ∀ {α : Type u_1} [inst : CompleteLattice α] (self : CompleteSublattice α) ⦃s : Set α⦄,
  s ⊆ self.carrier → sInf s ∈ self.carrier
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- Preserving zero morphisms implies preserving terminal objects.  -/
CategoryTheory.Functor.preservesInitialObject_of_preservesZeroMorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroObject D]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) F
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.HeightOneSpectrum.isNonarchimedean_adicAbv`.

---

The `v`-adic absolute value is nonarchimedean  -/
NumberField.RingOfIntegers.HeightOneSpectrum.isNonarchimedean_adicAbv : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R], IsNonarchimedean ⇑(NumberField.HeightOneSpectrum.adicAbv K v)
-- Mathlib.Topology.Algebra.Field
Subfield.topologicalClosure_minimal : ∀ {α : Type u_2} [inst : Field α] [inst_1 : TopologicalSpace α] [inst_2 : IsTopologicalDivisionRing α] (s : Subfield α)
  {t : Subfield α}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isCofilteredOrEmpty_of_directed_ge : ∀ (α : Type u) [inst : Preorder α] [IsCodirectedOrder α], CategoryTheory.IsCofilteredOrEmpty α
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.algebraMap_inj : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R] (x y : R),
  (algebraMap R (FreeAlgebra R X)) x = (algebraMap R (FreeAlgebra R X)) y ↔ x = y
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.AtomNode.mk.injEq : ∀ (vPos hPosSrc hPosTar : ℕ) (atom : Mathlib.Tactic.BicategoryLike.Atom) (vPos_1 hPosSrc_1 hPosTar_1 : ℕ)
  (atom_1 : Mathlib.Tactic.BicategoryLike.Atom),
  ({ vPos := vPos, hPosSrc := hPosSrc, hPosTar := hPosTar, atom := atom } =
      { vPos := vPos_1, hPosSrc := hPosSrc_1, hPosTar := hPosTar_1, atom := atom_1 }) =
    (vPos = vPos_1 ∧ hPosSrc = hPosSrc_1 ∧ hPosTar = hPosTar_1 ∧ atom = atom_1)
-- Init.Data.Rat.Lemmas
Rat.mkRat_zero : ∀ (n : ℤ), mkRat n 0 = 0
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.isCompact_compactSet : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  IsCompact (NumberField.mixedEmbedding.fundamentalCone.compactSet K)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Basic
_private.Mathlib.RingTheory.DedekindDomain.Ideal.Basic.0.IsDedekindDomainInv.dimensionLEOne : ∀ {A : Type u_2} [inst : CommRing A] [inst_1 : IsDomain A], IsDedekindDomainInv✝ A → Ring.DimensionLEOne A
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- The relation “there exists an element that semiconjugates `a` to `b`” on an
additive semigroup is transitive.  -/
AddSemiconjBy.isTrans : ∀ {S : Type u_1} [inst : AddSemigroup S], IsTrans S fun a b => ∃ c, AddSemiconjBy c a b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.contains_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {a : α},
  ∅.contains a = false
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.powC_nc.eq_def : ∀ (p : Lean.Grind.CommRing.Poly) (k c : ℕ),
  p.powC_nc k c =
    match k with
    | 0 => Lean.Grind.CommRing.Poly.num 1
    | 1 => p
    | k.succ => (p.powC_nc k c).mulC_nc p c
-- Mathlib.GroupTheory.GroupAction.Hom
AddActionHom.End.equivAddOpposite_symm_apply_apply : ∀ {M : Type u_2} [inst : AddMonoid M] (m : Mᵃᵒᵖ) (x : M),
  (AddActionHom.End.equivAddOpposite.symm m) x = x + AddOpposite.unop m
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
/-- The center of a non-unital star algebra is the set of elements which commute with every element.
They form a non-unital star subalgebra.  -/
NonUnitalStarSubalgebra.center : (R : Type u) →
  (A : Type v) →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalSemiring A] →
        [inst_2 : StarRing A] →
          [inst_3 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → NonUnitalStarSubalgebra R A
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.eq_1 : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (h : f v = 0),
  LinearEquiv.transvection h =
    { toFun := ⇑(LinearMap.transvection f v), map_add' := ⋯, map_smul' := ⋯, invFun := ⇑(LinearMap.transvection f (-v)),
      left_inv := ⋯, right_inv := ⋯ }
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_le_ediv : ∀ {a b c : ℤ}, 0 < c → a ≤ b → a / c ≤ b / c
-- Mathlib.Algebra.Module.PUnit
PUnit.vadd.eq_1 : ∀ {R : Type u_1}, PUnit.vadd = { vadd := fun x x_1 => PUnit.unit }
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.inf_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Subalgebra R A),
  (S ⊓ T).toSubsemiring = S.toSubsemiring ⊓ T.toSubsemiring
-- Mathlib.Analysis.Calculus.Deriv.Basic
Set.EqOn.deriv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f g : 𝕜 → F} {s : Set 𝕜}, Set.EqOn f g s → IsOpen s → Set.EqOn (deriv f) (deriv g) s
-- Lean.LibrarySuggestions.SineQuaNon
_private.Lean.LibrarySuggestions.SineQuaNon.0.Lean.LibrarySuggestions.SineQuaNon.sineQuaNonExt.unsafe_impl_4 : Lean.Environment → Lean.OLeanEntries (Array (Lean.NameMap (List (Lean.Name × Float))))
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofBitVec : ∀ (b : BitVec System.Platform.numBits), (ISize.ofBitVec b).toNatClampNeg = b.toInt.toNat
-- Mathlib.Tactic.Widget.Calc
/-- Rpc function for the calc widget.  -/
CalcPanel.rpc : CalcParams → Lean.Server.RequestM (Lean.Server.RequestTask ProofWidgets.Html)
-- Mathlib.GroupTheory.Index
AddSubgroup.index_eq_one : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 1 ↔ H = ⊤
-- Mathlib.Data.Finset.Order
Directed.finset_le : ∀ {α : Type u} {r : α → α → Prop} [IsTrans α r] {ι : Type u_1} [hι : Nonempty ι] {f : ι → α},
  Directed r f → ∀ (s : Finset ι), ∃ z, ∀ i ∈ s, r (f i) (f z)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instRpcEncodableDiagnosticWith : {α : Type} → [Lean.Server.RpcEncodable α] → Lean.Server.RpcEncodable (Lean.Lsp.DiagnosticWith α)
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.eqOn_eqLocus : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f g : M →ₛₗ[τ₁₂] M₂}, Set.EqOn ⇑f ⇑g ↑(f.eqLocus g)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- Given `I : MorphismProperty C` and a regular cardinal `κ : Cardinal.{w}`,
this property asserts the technical conditions which allow to proceed
to the small object argument by doing a construction by transfinite
induction indexed by the well-ordered type `κ.ord.ToType`.  -/
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → (κ : Cardinal.{w}) → [Fact κ.IsRegular] → [OrderBot κ.ord.ToType] → Prop
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsFiniteKernel.comap : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} {g : γ → α} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsFiniteKernel κ]
  (hg : Measurable g), ProbabilityTheory.IsFiniteKernel (κ.comap g hg)
-- Mathlib.Topology.UnitInterval
unitInterval.mul_le_right : ∀ {x y : ↑unitInterval}, x * y ≤ y
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.untop₀_max : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] {a b : WithTop α},
  a ≠ ⊤ → b ≠ ⊤ → (max a b).untop₀ = max a.untop₀ b.untop₀
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
/-- Given a pair of modules equipped with bilinear maps, this is the condition for a pair of
maps between them to be mutually adjoint.  -/
LinearMap.IsAdjointPair : {R : Type u_1} →
  {M : Type u_5} →
    {M₁ : Type u_6} →
      {M₃ : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommMonoid M₁] →
                [inst_4 : Module R M₁] →
                  [inst_5 : AddCommMonoid M₃] →
                    [inst_6 : Module R M₃] →
                      {I : R →+* R} → (M →ₗ[R] M →ₛₗ[I] M₃) → (M₁ →ₗ[R] M₁ →ₛₗ[I] M₃) → (M → M₁) → (M₁ → M) → Prop
-- Mathlib.Data.Finset.Basic
Finset.attach_eq_empty_iff : ∀ {α : Type u_1} {s : Finset α}, s.attach = ∅ ↔ s = ∅
-- Mathlib.Order.Category.Preord
Preord.hom_id : ∀ {X : Preord}, Preord.Hom.hom (CategoryTheory.CategoryStruct.id X) = OrderHom.id
-- Mathlib.Topology.JacobsonSpace
jacobsonSpace_iff_locallyClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  JacobsonSpace X ↔ ∀ (Z : Set X), Z.Nonempty → IsLocallyClosed Z → (Z ∩ closedPoints X).Nonempty
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodAssoc_apply_inl_inr : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : AddMonoid M] [inst_1 : AddMonoid N] [inst_2 : AddMonoid P]
  (x : N),
  (AddEquiv.coprodAssoc M N P) (AddMonoid.Coprod.inl (AddMonoid.Coprod.inr x)) =
    AddMonoid.Coprod.inr (AddMonoid.Coprod.inl x)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.lift_f_snd_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : M ⟶ K) (β : CochainComplex.HomComplex.Cochain M L (-1))
  (hαβ :
    CochainComplex.HomComplex.δ (-1) 0 β +
        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
      0)
  (p q : ℤ) (hpq : p + -1 = q),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.lift φ α β hαβ).f p)
      ((CochainComplex.mappingCocone.snd φ).v p q hpq) =
    β.v p q hpq