mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The equivalence between reflexive coforks and coforks sends a reflexive cofork to its underlying
cofork.  -/
CategoryTheory.Limits.reflexiveCoforkEquivCoforkObjIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) →
      (G : CategoryTheory.Limits.ReflexiveCofork F) →
        (CategoryTheory.Limits.reflexiveCoforkEquivCofork F).functor.obj G ≅ G.toCofork
-- Mathlib.LinearAlgebra.Dimension.Finrank
/-- The dimensions of the domain and range of an injective linear map are equal.  -/
LinearMap.finrank_range_of_inj : ∀ {R : Type u} {M : Type v} {N : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {f : M →ₗ[R] N},
  Function.Injective ⇑f → Module.finrank R ↥f.range = Module.finrank R M
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT_eq : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (hto : t.Ordered) {k : α} (he : ∃ a ∈ t, compare a k = Ordering.gt),
  Std.DTreeMap.Internal.Impl.Const.getEntryGT k t hto he =
    ((Std.DTreeMap.Internal.Impl.getEntryGT k t hto he).fst, (Std.DTreeMap.Internal.Impl.getEntryGT k t hto he).snd)
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
CategoryTheory.Limits.fiberwiseColimit_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C CategoryTheory.Cat}
  {H : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} H]
  (G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H)
  [inst_2 :
    ∀ {X Y : C} (f : X ⟶ Y),
      CategoryTheory.Limits.HasColimit ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))]
  (X : C),
  (CategoryTheory.Limits.fiberwiseColimit G).obj X =
    CategoryTheory.Limits.colimit ((CategoryTheory.Grothendieck.ι F X).comp G)
-- Mathlib.CategoryTheory.Skeletal
/-- Given a natural transformation `F₁ ⟶ F₂`, induce a natural transformation `map F₁ ⟶ map F₂`.  -/
CategoryTheory.ThinSkeleton.mapNatTrans : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F₁ F₂ : CategoryTheory.Functor C D} →
          (F₁ ⟶ F₂) → (CategoryTheory.ThinSkeleton.map F₁ ⟶ CategoryTheory.ThinSkeleton.map F₂)
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_congr_finset : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {t : Finset ι} {w : ι → R} {z : ι → E} [inst_3 : DecidableEq ι] {t' : Finset ι},
  (∀ i ∈ t ∪ t', w i ≠ 0 → i ∈ t ∩ t') → t.centerMass w z = t'.centerMass w z
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.Int.castDef.match_1.eq_2 : ∀ (motive : ℤ → Sort u_1) (n : ℕ) (h_1 : (n : ℕ) → motive (Int.ofNat n)) (h_2 : (n : ℕ) → motive (Int.negSucc n)),
  (match Int.negSucc n with
    | Int.ofNat n => h_1 n
    | Int.negSucc n => h_2 n) =
    h_2 n
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.constr_eq : ∀ {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M'] (S : Type u_13)
  [inst_5 : Semiring S] [inst_6 : Module S M'] [inst_7 : SMulCommClass R S M'] {g : ι → M'} {f : M →ₗ[R] M'},
  (∀ (i : ι), g i = f (b i)) → (b.constr S) g = f
-- Mathlib.Topology.MetricSpace.TransferInstance
/-- Transfer a `Dist` across an `Equiv`  -/
Equiv.dist : {α : Type u_1} → {β : Type u_2} → α ≃ β → [Dist β] → Dist α
-- Mathlib.Geometry.Euclidean.SignedDist
Affine.Simplex.signedInfDist_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex ℝ P n) {m : ℕ} [inst_5 : NeZero m]
  (e : Fin (n + 1) ≃ Fin (m + 1)) (j : Fin (m + 1)), (s.reindex e).signedInfDist j = s.signedInfDist (e.symm j)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.instAddGroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H],
  AddMonoid.Coprod.instAddGroup =
    { toAddMonoid := AddMonoid.Coprod.inst, toNeg := AddMonoid.Coprod.instNeg, sub := SubNegMonoid.sub',
      zsmul := zsmulRec, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.Order.WellFounded
/-- If `r` is a well-founded relation, then any nonempty set has a minimal element
with respect to `r`.  -/
WellFounded.has_min : ∀ {α : Type u_4} {r : α → α → Prop}, WellFounded r → ∀ (s : Set α), s.Nonempty → ∃ a ∈ s, ∀ x ∈ s, ¬r x a
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_id : ∀ {G : Type u_1} [inst : AddGroup G] (K : AddSubgroup G), AddSubgroup.map (AddMonoidHom.id G) K = K
-- Mathlib.Topology.Sets.OpenCover
TopologicalSpace.IsOpenCover.iSup_set_eq_univ : ∀ {ι : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] {u : ι → TopologicalSpace.Opens X},
  TopologicalSpace.IsOpenCover u → ⋃ i, ↑(u i) = Set.univ
-- Mathlib.Algebra.Homology.Embedding.TruncLE
HomologicalComplex.truncLEMap_comp : ∀ {ι : 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 M : HomologicalComplex C c'} (φ : K ⟶ L) (φ' : L ⟶ M) (e : c.Embedding c') [inst_2 : e.IsTruncLE]
  [inst_3 : ∀ (i' : ι'), K.HasHomology i'] [inst_4 : ∀ (i' : ι'), L.HasHomology i']
  [inst_5 : ∀ (i' : ι'), M.HasHomology i'] [inst_6 : CategoryTheory.Limits.HasZeroObject C],
  HomologicalComplex.truncLEMap (CategoryTheory.CategoryStruct.comp φ φ') e =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.truncLEMap φ e) (HomologicalComplex.truncLEMap φ' e)
-- Mathlib.Data.Matrix.Basic
AddMonoidHom.mapMatrix_zero : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} {β : Type u_12} [inst : AddZeroClass α] [inst_1 : AddZeroClass β],
  AddMonoidHom.mapMatrix 0 = 0
-- Mathlib.RingTheory.Flat.FaithfullyFlat.Basic
Submodule.baseChange_le_iff : ∀ {R : Type u_1} {M : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A]
  [Module.FaithfullyFlat R A] [inst_4 : AddCommGroup M] [inst_5 : Module R M] {p q : Submodule R M},
  Submodule.baseChange A p ≤ Submodule.baseChange A q ↔ p ≤ q
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.e_mem_lieAlgebra : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : Fintype ι] [inst_10 : DecidableEq ι] (i : ↥b.support),
  RootPairing.GeckConstruction.e i ∈ RootPairing.GeckConstruction.lieAlgebra b
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.length_eq_forIn : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] {it : Std.IterM m β},
  it.length = forIn it { down := 0 } fun x acc => pure (ForInStep.yield { down := acc.down + 1 })
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.orderHom.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N] (f : M →*o N),
  MulArchimedeanClass.orderHom f = (MulArchimedeanOrder.orderHom f).antisymmetrization
-- Mathlib.Analysis.SpecificLimits.Normed
tendsto_intCast_atTop_cobounded : ∀ {α : Type u_1} [inst : NormedRing α] [NormSMulClass ℤ α] [Nontrivial α],
  Filter.Tendsto Int.cast Filter.atTop (Bornology.cobounded α)
-- Init.Data.UInt.Lemmas
UInt8.ofNatClamp.eq_1 : ∀ (n : ℕ),
  UInt8.ofNatClamp n =
    if h : n < UInt8.size then UInt8.ofNatLT n h else UInt8.ofNatLT (UInt8.size - 1) UInt8.ofNatClamp._proof_1
-- Init.Data.String.Length
String.length_empty : "".length = 0
-- Mathlib.Topology.Sion
/-- **Alias** of `_private.Mathlib.Topology.Sion.0.Sion.setOfPred_sublevelLeft_subset`.

---

The set of parameters `z` in the segment `[y, y']` such that `f b z ≤ f b' y`.  -/
_private.Mathlib.Topology.Sion.0.Sion.setOf_sublevelLeft_subset : {E : Type u_1} →
  {F : Type u_2} →
    {β : Type u_3} →
      [LinearOrder β] →
        Set E →
          (Y : Set F) →
            (E → F → β) →
              [inst : AddCommGroup F] → [inst_1 : Module ℝ F] → β → β → (y y' : ↑Y) → Set ↑(segment ℝ ↑y ↑y')
-- Mathlib.RingTheory.Congruence.Basic
RingCon.instSMulQuotient : {α : Type u_1} →
  {R : Type u_3} →
    [inst : Add R] →
      [inst_1 : MulOneClass R] → [inst_2 : SMul α R] → [IsScalarTower α R R] → (c : RingCon R) → SMul α c.Quotient
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_dvd_lcm_mul_right : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] (m n k : α), lcm m n ∣ lcm (m * k) n
-- Mathlib.GroupTheory.Perm.Sign
/-- This computably represents the fact that any permutation can be represented as the product of
a list of transpositions.  -/
Equiv.Perm.truncSwapFactors : {α : Type u} → [inst : DecidableEq α] → [Fintype α] → (f : Equiv.Perm α) → Trunc { l // l.prod = f ∧ ∀ g ∈ l, g.IsSwap }
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
/-- For fixed `ε > 0`, the mapping `mulExpNegMulSq ε` is Lipschitz with constant `1`  -/
Real.lipschitzWith_one_mulExpNegMulSq : ∀ {ε : ℝ}, 0 < ε → LipschitzWith 1 ε.mulExpNegMulSq
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
/-- `DomAddAct.mk` as a homeomorphism.  -/
DomAddAct.mkHomeomorph : {M : Type u_1} → [inst : TopologicalSpace M] → M ≃ₜ Mᵈᵃᵃ
-- Lean.Elab.Binders
/-- Adds a declaration whose value is a Syntax expression representing `tactic`.
If `name?` is provided, it is used for the declaration name, and otherwise a fresh name is generated.
Returns the declaration name.
 -/
Lean.Elab.Term.declareTacticSyntax : Lean.Syntax → optParam (Option Lean.Name) none → Lean.Elab.TermElabM Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
_private.Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas.0.Nat.nthRoot.match_3.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (x : ℕ) (h_1 : (x : ℕ) → motive 0 x) (h_2 : (a : ℕ) → motive 1 a)
  (h_3 : (n a : ℕ) → motive n.succ.succ a),
  (match 0, x with
    | 0, x => h_1 x
    | 1, a => h_2 a
    | n.succ.succ, a => h_3 n a) =
    h_1 x
-- Mathlib.Order.Hom.BoundedLattice
BoundedLatticeHom.mk : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Lattice α] →
      [inst_1 : Lattice β] →
        [inst_2 : BoundedOrder α] →
          [inst_3 : BoundedOrder β] →
            (toLatticeHom : LatticeHom α β) →
              toLatticeHom.toFun ⊤ = ⊤ → toLatticeHom.toFun ⊥ = ⊥ → BoundedLatticeHom α β
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lanLeftExtension_extension : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g],
  (CategoryTheory.Bicategory.lanLeftExtension f g).extension = CategoryTheory.Bicategory.lan f g
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.flatten.match_1.eq_2 : ∀ {α : Type u_1} (motive : Stream'.WSeq α ⊕ Computation (Stream'.WSeq α) → Sort u_2) (c' : Computation (Stream'.WSeq α))
  (h_1 : (s : Stream'.WSeq α) → motive (Sum.inl s)) (h_2 : (c' : Computation (Stream'.WSeq α)) → motive (Sum.inr c')),
  (match Sum.inr c' with
    | Sum.inl s => h_1 s
    | Sum.inr c' => h_2 c') =
    h_2 c'
-- Std.Time.Format.Modifier
Std.Time.Modifier.x.inj : ∀ {presentation presentation_1 : Std.Time.OffsetX},
  Std.Time.Modifier.x presentation = Std.Time.Modifier.x presentation_1 → presentation = presentation_1
-- Mathlib.Order.Category.Preord
Preord.dualEquiv_inverse : Preord.dualEquiv.inverse = Preord.dual
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.instIsRegularPairingCore : ∀ {m : ℕ} (k : Fin (m + 1)) (n : ℕ), (SSet.prodStdSimplex.pairingCore k n).IsRegular
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
CategoryTheory.instContainsZeroIsArtinianObjectOfHasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C],
  CategoryTheory.isArtinianObject.ContainsZero
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (a₁ : ℤ × M) {a₂ : ℤ × M} {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M},
  l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval → (a₁ ::ᵣ l₁).eval / (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
/-- Euler's infinite product formula for the complex sine function.  -/
Complex.tendsto_euler_sin_prod : ∀ (z : ℂ),
  Filter.Tendsto (fun n => ↑Real.pi * z * ∏ j ∈ Finset.range n, (1 - z ^ 2 / (↑j + 1) ^ 2)) Filter.atTop
    (nhds (Complex.sin (↑Real.pi * z)))
-- Mathlib.CategoryTheory.ObjectProperty.Small
CategoryTheory.ObjectProperty.instSmallMax : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P Q : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.Small.{w, v, u} P] [CategoryTheory.ObjectProperty.Small.{w, v, u} Q],
  CategoryTheory.ObjectProperty.Small.{w, v, u} (P ⊔ Q)
-- Aesop.RuleSet
_private.Aesop.RuleSet.0.Aesop.LocalRuleSet.applicableForwardRulesWith.mkMsg : Aesop.ForwardRule → Aesop.PremiseIndex → Lean.MessageData
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.instAddRightMono : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α], AddRightMono (Finset α)
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.image_op_smul_distrib : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (f : F) (a : α) (s : Set α), ⇑f '' (MulOpposite.op a • s) = MulOpposite.op (f a) • ⇑f '' s
-- Mathlib.Data.ENNReal.Operations
ENNReal.mul_pos_iff : ∀ {a b : ENNReal}, 0 < a * b ↔ 0 < a ∧ 0 < b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
addRightReflectLE_of_addLeftReflectLE : ∀ (N : Type u_2) [inst : AddCommSemigroup N] [inst_1 : LE N] [AddLeftReflectLE N], AddRightReflectLE N
-- Mathlib.Data.Set.Image
Function.Commute.set_image : ∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Commute (Set.image f) (Set.image g)
-- Mathlib.NumberTheory.NumberField.AdeleRing
NumberField.AdeleRing.algebraMap_snd_apply : ∀ (R : Type u_1) (K : Type u_2) [inst : CommRing R] [inst_1 : IsDedekindDomain R] [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (x : K) (v : IsDedekindDomain.HeightOneSpectrum R),
  ((algebraMap K (NumberField.AdeleRing R K)) x).2 v =
    { toCompletion := ↑((WithVal.equiv (IsDedekindDomain.HeightOneSpectrum.valuation K v)).symm x) }
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
jacobiTheta₂'.eq_1 : ∀ (z τ : ℂ), jacobiTheta₂' z τ = ∑' (n : ℤ), jacobiTheta₂'_term n z τ
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- `alter` preserves well-formedness. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.alter : ∀ {α : Type u} [inst : Ord α] {x : α → Type v} [inst_1 : Std.LawfulEqOrd α] {t : Std.DTreeMap.Internal.Impl α x}
  {h : t.Balanced} {k : α} {f : Option (x k) → Option (x k)}, t.WF → (Std.DTreeMap.Internal.Impl.alter k f t h).impl.WF
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.isMaxRank_fundSystem : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K], NumberField.Units.IsMaxRank (NumberField.Units.fundSystem K)
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.cons.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i : ι} (m : M i) (w : Monoid.CoprodI.Word M)
  (hmw : w.fstIdx ≠ some i) (h1 : m ≠ 1),
  Monoid.CoprodI.Word.cons m w hmw h1 = { toList := ⟨i, m⟩ :: w.toList, ne_one := ⋯, chain_ne := ⋯ }
-- Mathlib.MeasureTheory.PiSystem
IsPiSystem.comap : ∀ {α : Type u_3} {β : Type u_4} {S : Set (Set β)}, IsPiSystem S → ∀ (f : α → β), IsPiSystem {s | ∃ t ∈ S, f ⁻¹' t = s}
-- Mathlib.Algebra.Group.Equiv.Opposite
AddMonoidHom.op.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N],
  AddMonoidHom.op =
    { toFun := fun f => { toFun := AddOpposite.op ∘ ⇑f ∘ AddOpposite.unop, map_zero' := ⋯, map_add' := ⋯ },
      invFun := fun f => { toFun := AddOpposite.unop ∘ ⇑f ∘ AddOpposite.op, map_zero' := ⋯, map_add' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_sub_self_iff : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] (a : α) {b : α}, a ≤ a - b ↔ b ≤ 0
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.ext_ring_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  [inst_3 : Algebra R A] [inst_4 : TopologicalSpace R] {f g : R →A[R] A}, f = g ↔ f 1 = g 1
-- Init.Dynamic
_private.Init.Dynamic.0.Dynamic.typeNameImpl : Dynamic → Lean.Name
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.card_eq_zero : ∀ {o : Ordinal.{u_1}}, o.card = 0 ↔ o = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey?_eq_some_minKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false}, t.minKey? = some (t.minKey he)
-- Init.Grind.Offset
Lean.Grind.Nat.ro_ro : ∀ (u w v k₁ k₂ : ℕ), u ≤ w + k₁ → w ≤ v + k₂ → u ≤ v + (k₁ + k₂)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `lt_sub_iff_add_lt'`. -/
add_lt_of_lt_sub_left : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, b < c - a → a + b < c
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ground_indep_iff_isBase : ∀ {α : Type u_1} {M : Matroid α}, M.Indep M.E ↔ M.IsBase M.E
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
MonoidAlgebra.instHopfAlgebraStruct : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [HopfAlgebra R A] → (G : Type u_3) → [inst_3 : Group G] → HopfAlgebraStruct R (MonoidAlgebra A G)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput.mk.injEq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {len : ℕ} (lhs : aig.RefVec len)
  (bit : aig.Ref) (lhs_1 : aig.RefVec len) (bit_1 : aig.Ref),
  ({ lhs := lhs, bit := bit } = { lhs := lhs_1, bit := bit_1 }) = (lhs = lhs_1 ∧ bit = bit_1)
-- Mathlib.Data.Nat.ChineseRemainder
/-- The natural number less than `(l.map s).prod` congruent to
`a i` mod `s i` for all  `i ∈ l`.  -/
Nat.chineseRemainderOfList : {ι : Type u_1} →
  (a s : ι → ℕ) → (l : List ι) → List.Pairwise (Function.onFun Nat.Coprime s) l → { k // ∀ i ∈ l, k ≡ a i [MOD s i] }
-- Mathlib.Algebra.Homology.CochainComplexOpposite
/-- The embedding of the complex shape `down ℤ` in `up ℤ` given by `n ↦ -n`.  -/
ComplexShape.embeddingDownIntUpInt : (ComplexShape.down ℤ).Embedding (ComplexShape.up ℤ)
-- Mathlib.Order.Std
PartialOrder.OfStdArgs.mk.inj : ∀ {α : Type u_1} {toPreorderArgs : Preorder.OfStdArgs α}
  {isPartialOrder :
    autoParam
      (let this := toPreorderArgs.le;
      Std.IsPartialOrder α)
      PartialOrder.OfStdArgs.isPartialOrder._autoParam}
  {toPreorderArgs_1 : Preorder.OfStdArgs α}
  {isPartialOrder_1 :
    autoParam
      (let this := toPreorderArgs_1.le;
      Std.IsPartialOrder α)
      PartialOrder.OfStdArgs.isPartialOrder._autoParam},
  { toPreorderArgs := toPreorderArgs, isPartialOrder := isPartialOrder } =
      { toPreorderArgs := toPreorderArgs_1, isPartialOrder := isPartialOrder_1 } →
    toPreorderArgs = toPreorderArgs_1
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.neg_mk : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddGroup γ] [inst_3 : IsTopologicalAddGroup γ] (f : α → γ) (hf : MeasureTheory.AEStronglyMeasurable f μ),
  -MeasureTheory.AEEqFun.mk f hf = MeasureTheory.AEEqFun.mk (-f) ⋯
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_prodMk_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} [ContinuousSMul 𝕜 E] [ContinuousSMul 𝕜 F] {k : α → G},
  (fun x => (f x, g x)) =o[𝕜; l] k ↔ f =o[𝕜; l] k ∧ g =o[𝕜; l] k
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.MemLp.star : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_5} [inst : NormedAddCommGroup R]
  [inst_1 : StarAddMonoid R] [NormedStarGroup R] {p : ENNReal} {f : α → R},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (star f) p μ
-- Mathlib.Topology.Constructions
continuous_toDual : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous ⇑OrderDual.toDual
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductIso_inv_comp_snd_apply : ∀ (X Y : Type u) (x : X × Y),
  (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd)
      ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Types.binaryProductIso X Y).inv) x) =
    x.2
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b},
  CurveIntegrable ω₁ γ →
    CurveIntegrable ω₂ γ → curveIntegral (ω₁ - ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x - ∫ᶜ (x : E) in γ, ω₂ x
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Another, more explicit, formulation of the universal property of a limit cone.
See also `homIso`.  -/
CategoryTheory.Limits.IsLimit.homIso' : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            CategoryTheory.Limits.IsLimit t →
              (W : C) →
                ULift.{u₁, v₃} (W ⟶ t.pt) ≅
                  { p // ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (p j) (F.map f) = p j' }
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
AddSubgroup.closure_image_isAddIndecomposable_baseOf : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : AddCommGroup G] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : InvolutiveNeg ι] [inst_4 : AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G),
  (∀ (i : ι), v (-i) = -v i) →
    ∀ (f : G →+ S),
      (∀ (i : ι), f (v i) ≠ 0) →
        AddSubgroup.closure (v '' IsAddIndecomposable.baseOf v f) = AddSubgroup.closure (Set.range v)
-- Mathlib.Topology.ShrinkingLemma
/-- For each `i ∈ carrier`, the refined set satisfies `p`.  -/
ShrinkingLemma.PartialRefinement.pred_of_mem : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {u : ι → Set X} {s : Set X} {p : Set X → Prop}
  (self : ShrinkingLemma.PartialRefinement u s p) {i : ι}, i ∈ self.carrier → p (self.toFun i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = true → t.maxKey? = none
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
/-- The left-inverse of `algebraMap`.  -/
ExteriorAlgebra.algebraMapInv : {R : Type u1} →
  [inst : CommRing R] → {M : Type u2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → ExteriorAlgebra R M →ₐ[R] R