mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes  -/
IsClosed.mem_iff_infDist_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {x : α},
  IsClosed s → s.Nonempty → (x ∈ s ↔ Metric.infDist x s = 0)
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
LinearIndepOn.union : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {t : Set ι},
  LinearIndepOn R v s →
    LinearIndepOn R v t → Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t)) → LinearIndepOn R v (s ∪ t)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.curryRingEquiv.eq_1 : ∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N],
  MonoidAlgebra.curryRingEquiv = { toEquiv := MonoidAlgebra.curryAddEquiv.toEquiv, map_mul' := ⋯, map_add' := ⋯ }
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.toPoly.go : ℕ → Nat.Internal.Linear.Expr → Nat.Internal.Linear.Poly → Nat.Internal.Linear.Poly
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `Differentiable.finsetProd`. -/
Differentiable.finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {ι : Type u_2} {𝔸' : Type u_3} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, Differentiable 𝕜 (f i)) → Differentiable 𝕜 (∏ i ∈ u, f i)
-- Init.Data.List.MapIdx
List.mapFinIdx_ne_nil_iff : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : (i : ℕ) → α → i < l.length → β}, l.mapFinIdx f ≠ [] ↔ l ≠ []
-- Mathlib.Algebra.Algebra.Hom
RingHom.toNatAlgHom_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : R), f.toNatAlgHom x = f x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inter_add_singleton : ∀ {α : Type u_2} [inst : Add α] [IsRightCancelAdd α] [inst_2 : DecidableEq α] (s t : Finset α) (a : α),
  s ∩ t + {a} = (s + {a}) ∩ (t + {a})
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.IsRationalOver.exists_birationalOver_affineSpace : ∀ {S X : AlgebraicGeometry.Scheme} (sX : X ⟶ S) [self : AlgebraicGeometry.Scheme.IsRationalOver sX],
  ∃ n, AlgebraicGeometry.Scheme.BirationalOver sX (AlgebraicGeometry.AffineSpace n S ↘ S)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_eq_default : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m).WF → ∀ {a : α}, m.contains a = false → Std.DHashMap.Internal.Raw₀.Const.get! m a = default
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.startsWith_eq_startsWith_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.startsWith pat = s.toSlice.startsWith pat
-- Std.Time.Duration
Std.Time.Duration.instCoeOffset_4 : Coe Std.Time.Week.Offset Std.Time.Duration
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.SpecToEquivOfField_symm_apply : ∀ (K : Type u) [inst : Field K] (X : AlgebraicGeometry.Scheme) (xf : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)),
  (AlgebraicGeometry.Scheme.SpecToEquivOfField K X).symm xf =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map xf.snd) (X.fromSpecResidueField xf.fst)
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.HasCoequalizer.coequalizer_π_app_isLocalHom : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f g : X ⟶ Y)
  (U :
    TopologicalSpace.Opens
      ↑↑(CategoryTheory.Limits.coequalizer (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
              (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).toPresheafedSpace),
  IsLocalHom
    (CommRingCat.Hom.hom
      ((CategoryTheory.Limits.coequalizer.π (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom f)
                (AlgebraicGeometry.LocallyRingedSpace.Hom.toShHom g)).hom.c.app
        (Opposite.op U)))
-- Mathlib.Data.Matrix.Basic
Matrix.entryAddHom_eq_comp : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : Add α] {i : m} {j : n},
  Matrix.entryAddHom α i j =
    ((Pi.evalAddHom (fun x => α) j).comp (Pi.evalAddHom (fun i => n → α) i)).comp ↑Matrix.ofAddEquiv.symm
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.has_pi : CategoryTheory.Limits.HasProducts CategoryTheory.Grpd
-- Mathlib.Algebra.Group.Hom.CompTypeclasses
MonoidHom.CompTriple.comp_assoc : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Monoid P] {Q : Type u_4}
  [inst_3 : Monoid Q] {φ₁ : M →* N} {φ₂ : N →* P} {φ₁₂ : M →* P},
  φ₁.CompTriple φ₂ φ₁₂ →
    ∀ {φ₃ : P →* Q} {φ₂₃ : N →* Q},
      φ₂.CompTriple φ₃ φ₂₃ → ∀ {φ₁₂₃ : M →* Q}, φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.monoid : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Monoid (G i)] → [inst_1 : Monoid H] → {φ : (i : ι) → H →* G i} → Monoid (Monoid.PushoutI φ)
-- Mathlib.Algebra.Homology.HomotopyCategory.Acyclic
HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclic : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  HomotopyCategory.quasiIso C (ComplexShape.up ℤ) = (HomotopyCategory.subcategoryAcyclic C).trW
-- Mathlib.Algebra.Group.Defs
/-- A `SubtractionMonoid` which `IsMulCommutative` is a `SubtractionCommMonoid`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsAddCommutative.instDivisionAddCommMonoid : {M : Type u_2} → [inst : SubtractionMonoid M] → [IsAddCommutative M] → SubtractionCommMonoid M
-- Mathlib.Analysis.Normed.Group.Pointwise
IsCompact.closedBall_zero_sub : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {δ : ℝ} {s : Set E},
  IsCompact s → 0 ≤ δ → Metric.closedBall 0 δ - s = Metric.cthickening δ (-s)
-- Mathlib.Probability.Kernel.Disintegration.StandardBorel
ProbabilityTheory.Kernel.condKernelBorel.instIsCondKernel : ∀ {α : Type u_1} {γ : Type u_3} {Ω : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [inst : MeasurableSpace.CountablyGenerated γ] {mΩ : MeasurableSpace Ω} [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] (κ : ProbabilityTheory.Kernel α (γ × Ω)) [inst_3 : ProbabilityTheory.IsFiniteKernel κ],
  κ.IsCondKernel κ.condKernelBorel
-- Std.Time.Time.Unit.Second
Std.Time.Second.instOfNatOffset : {n : ℕ} → OfNat Std.Time.Second.Offset n
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- `fderivWithin 𝕜 f s` is smooth at `x₀` within `s`.  -/
ContDiffWithinAt.fderivWithin_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} {f : E → F} {x₀ : E}
  {m n : WithTop ℕ∞},
  ContDiffWithinAt 𝕜 n f s x₀ → UniqueDiffOn 𝕜 s → m + 1 ≤ n → x₀ ∈ s → ContDiffWithinAt 𝕜 m (fderivWithin 𝕜 f s) s x₀
-- Std.Data.HashMap.Basic
Std.HashMap.instForMProdOfMonad : {α : Type u} →
  {β : Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → {m : Type w → Type w'} → [Monad m] → ForM m (Std.HashMap α β) (α × β)
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.Presheaf.isSheaf_coherent_of_projective_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u₃}
  [inst_1 : CategoryTheory.Category.{v₃, u₃} A] (F : CategoryTheory.Functor Cᵒᵖ A) {B : Type u₄}
  [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (s : CategoryTheory.Functor A B) [inst_3 : CategoryTheory.Preregular C]
  [inst_4 : CategoryTheory.FinitaryExtensive C] [∀ (X : C), CategoryTheory.Projective X]
  [CategoryTheory.Limits.PreservesFiniteProducts s],
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F →
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) (F.comp s)
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.hasRightHomology_of_preserves' : ∀ {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.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [S.HasRightHomology]
  [F.PreservesRightHomologyOf S], (F.mapShortComplex.obj S).HasRightHomology
-- Mathlib.Algebra.Ring.Subsemiring.Pointwise
Subsemiring.mem_smul_pointwise_iff_exists : ∀ {M : Type u_1} {R : Type u_2} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M) (r : R)
  (S : Subsemiring R), r ∈ m • S ↔ ∃ s ∈ S, m • s = r
-- Mathlib.Logic.Basic
eq_true_intro : ∀ {a : Prop}, a → a = True
-- Mathlib.Algebra.Order.Antidiag.Nat
Nat.card_finMulAntidiag_of_squarefree : ∀ {d n : ℕ}, Squarefree n → (d.finMulAntidiag n).card = d ^ ArithmeticFunction.cardDistinctFactors n
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the reverse direction of `upperSemicontinuousAt_inv_iff`. -/
LowerSemicontinuousAt.inv : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {a : α} [inst_1 : PartialOrder β]
  [inst_2 : CommGroup β] [IsOrderedMonoid β], LowerSemicontinuousAt f a → UpperSemicontinuousAt f⁻¹ a
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.isEmpty_iff_forall_contains : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → (m.isEmpty = true ↔ ∀ (a : α), m.contains a = false)
-- Mathlib.NumberTheory.ModularForms.Basic
/-- **Alias** of `FunLike.coe_zero`. -/
CuspForm.coe_zero : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Zero F] [inst_2 : Zero β]
  [IsZeroApply F α β], ⇑0 = 0
-- Mathlib.RingTheory.RingHom.Smooth
RingHom.FormallySmooth.stableUnderComposition : RingHom.StableUnderComposition @RingHom.FormallySmooth
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_maxValue : ∀ (h : System.Platform.numBits = 64), ISize.maxValue.toBitVec64 h = BitVec.intMax 64
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Injective.State.mk.sizeOf_spec : ∀ (thms : Lean.Meta.Grind.InjectiveTheoremsArray)
  (fns : Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.InjectiveInfo),
  sizeOf { thms := thms, fns := fns } = 1 + sizeOf thms + sizeOf fns
-- Mathlib.Tactic.Translate.UnfoldBoundary
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold.inj : ∀ {declName unfold declName_1 unfold_1 : Lean.Name},
  Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold declName unfold =
      Mathlib.Tactic.UnfoldBoundary.UnfoldEntry.unfold declName_1 unfold_1 →
    declName = declName_1 ∧ unfold = unfold_1
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_monomial : ∀ {R : Type u} [inst : Semiring R] (a : R) (n : ℕ),
  Polynomial.derivative ((Polynomial.monomial n) a) = (Polynomial.monomial (n - 1)) (a * ↑n)
-- Init.Data.Nat.Div.Basic
Nat.zero_eq_one_mod_iff : ∀ {n : ℕ}, 0 = 1 % n ↔ n = 1
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_natCast : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (↑n).natTrailingDegree = 0
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_equiv_eq_zero_iff_lift_ne : ∀ {α : Type u} {β' : Type v},
  Cardinal.mk (α ≃ β') = 0 ↔ Cardinal.lift.{v, u} (Cardinal.mk α) ≠ Cardinal.lift.{u, v} (Cardinal.mk β')
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- The family of 2-morphisms into an absolute right Kan lift.  -/
CategoryTheory.Bicategory.RightLift.IsAbsKan.desc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          {t : CategoryTheory.Bicategory.RightLift f g} →
            t.IsAbsKan →
              {x : B} →
                {h : x ⟶ c} →
                  (s : CategoryTheory.Bicategory.RightLift f (CategoryTheory.CategoryStruct.comp h g)) →
                    s.lift ⟶ CategoryTheory.CategoryStruct.comp h t.lift
-- Mathlib.Algebra.DirectSum.Module
DirectSum.IsInternal.congr_simp : ∀ {ι : Type v} {M : Type u_1} {S : Type u_2} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] [inst_2 : AddCommMonoid M]
  [inst_3 : SetLike S M] [inst_4 : AddSubmonoidClass S M] (A A_1 : ι → S),
  A = A_1 → DirectSum.IsInternal A = DirectSum.IsInternal A_1
-- Init.Data.List.Nat.TakeDrop
List.take_prefix_take_left : ∀ {α : Type u_1} {l : List α} {i j : ℕ}, i ≤ j → List.take i l <+: List.take j l
-- Std.Async.System
/-- Time spent on low-priority user processes.
 -/
Std.Async.System.CPUTimes.niceTime : Std.Async.System.CPUTimes → Std.Time.Millisecond.Offset
-- Init.Data.SInt.Lemmas
instLawfulOrderLTISize : Std.LawfulOrderLT ISize
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.small_Ico : ∀ (a b : Cardinal.{u}), Small.{u, u + 1} ↑(Set.Ico a b)
-- Mathlib.Analysis.Normed.Group.CocompactMap
ContinuousMapClass.toCocompactMapClass_of_norm : ∀ {E : Type u_2} {F : Type u_3} {𝓕 : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [ProperSpace E] [inst_3 : FunLike 𝓕 E F] [ContinuousMapClass 𝓕 E F],
  (∀ (f : 𝓕) (ε : ℝ), ∃ r, ∀ (x : E), r < ‖x‖ → ε < ‖f x‖) → CocompactMapClass 𝓕 E F
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
/-- The composition of two pushforward functors for sheaves of modules on schemes
identify to the pushforward for the composition.  -/
AlgebraicGeometry.Scheme.Modules.pushforwardComp : {X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Y) →
    (g : Y ⟶ Z) →
      (AlgebraicGeometry.Scheme.Modules.pushforward f).comp (AlgebraicGeometry.Scheme.Modules.pushforward g) ≅
        AlgebraicGeometry.Scheme.Modules.pushforward (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_zero : Complex.sin 0 = 0
-- Mathlib.Algebra.CubicDiscriminant
/-- The degree-3 coefficient  -/
Cubic.a : {R : Type u_1} → Cubic R → R
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
Units.inv_mul_le_one : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a : M}, ↑u⁻¹ * a ≤ 1 ↔ a ≤ ↑u
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Basic
groupHomology.inhomogeneousChains.ext_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} {n : ℕ} {M : ModuleCat k}
  {x y : (groupHomology.inhomogeneousChains A).X n ⟶ M},
  x = y ↔
    ∀ (g : Fin n → G),
      CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle g)) x =
        CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (Finsupp.lsingle g)) y
-- Mathlib.Order.Zorn
zorn_superset : ∀ {α : Type u_1} (S : Set (Set α)),
  (∀ c ⊆ S, IsChain (fun x1 x2 => x1 ⊆ x2) c → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) → ∃ m, Minimal (fun x => x ∈ S) m
-- Mathlib.Algebra.Group.Action.Prod
Prod.smulCommClass : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} {β : Type u_6} [inst : SMul M α] [inst_1 : SMul M β] [inst_2 : SMul N α]
  [inst_3 : SMul N β] [SMulCommClass M N α] [SMulCommClass M N β], SMulCommClass M N (α × β)
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The sum of almost everywhere measurable functions is measurable.  -/
AEMeasurable.tsum' : ∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.PseudoMetrizableSpace E] [inst_4 : MeasurableSpace E] [BorelSpace E]
  [MeasurableAdd₂ E] {L : SummationFilter ι} [L.NeBot] [L.filter.IsCountablyGenerated] {μ : MeasureTheory.Measure X}
  {f : ι → X → E}, (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (∑'[L] (i : ι), f i) μ
-- Mathlib.Algebra.MvPolynomial.Rename
/-- Every polynomial is a polynomial in finitely many variables.  -/
MvPolynomial.exists_fin_rename : ∀ {σ : Type u_1} {R : Type u_4} [inst : CommSemiring R] (p : MvPolynomial σ R),
  ∃ n f, ∃ (_ : Function.Injective f), ∃ q, p = (MvPolynomial.rename f) q
-- Mathlib.Data.Set.Lattice
Set.union_iUnion_nat_succ : ∀ {α : Type u_1} (u : ℕ → Set α), u 0 ∪ ⋃ i, u (i + 1) = ⋃ i, u i
-- Mathlib.Algebra.Lie.Basic
/-- Lie algebra equivalences are transitive.  -/
LieEquiv.trans : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      {L₃ : Type w₁} →
        [inst : CommRing R] →
          [inst_1 : LieRing L₁] →
            [inst_2 : LieRing L₂] →
              [inst_3 : LieRing L₃] →
                [inst_4 : LieAlgebra R L₁] →
                  [inst_5 : LieAlgebra R L₂] → [inst_6 : LieAlgebra R L₃] → (L₁ ≃ₗ⁅R⁆ L₂) → (L₂ ≃ₗ⁅R⁆ L₃) → L₁ ≃ₗ⁅R⁆ L₃
-- Std.Data.TreeSet.Basic
/-- Tries to retrieve the smallest element of the tree set, returning `none` if the set is empty.
 -/
Std.TreeSet.min? : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Option α
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokenType.parameter.sizeOf_spec : sizeOf Lean.Lsp.SemanticTokenType.parameter = 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
/-- The clifford algebra over a 0-dimensional vector space is isomorphic to its scalars.  -/
CliffordAlgebraRing.equiv : {R : Type u_1} → [inst : CommRing R] → CliffordAlgebra 0 ≃ₐ[R] R
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
_private.Mathlib.Algebra.BigOperators.Group.Finset.Defs.0.BigOperators.FinsetResult.Iio : Lean.Term → BigOperators.FinsetResult✝
-- Mathlib.GroupTheory.Nilpotent
AddGroup.IsNilpotent.isVirtuallyNilpotent : ∀ {G : Type u_1} [inst : AddGroup G], AddGroup.IsNilpotent G → AddGroup.IsVirtuallyNilpotent G
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_distinguished : ∀ {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.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (X : C),
  (t.eTriangleLTGE.obj i).obj X ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Data.ENat.Basic
ENat.toNatHom_apply : ∀ (n : ℕ), ENat.toNatHom ↑n = (↑n).toNat
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
CategoryTheory.ShortComplex.ShortExact.epi_g : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C}, S.ShortExact → CategoryTheory.Epi S.g
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.le_maxKey_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : k ∈ t), (cmp k (t.maxKey ⋯)).isLE = true
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.l_inv.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (X : CategoryTheory.FreeMonoidalCategory C),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.l_inv X) = 1 + sizeOf X
-- Lean.Elab.Do.ForwardSyntax
Lean.Elab.Do.ForwardArg.binders : Lean.Elab.Do.ForwardArg → Array (Lean.TSyntax `Lean.Parser.Term.funBinder)
-- Init.Data.Range.Polymorphic.Nat
Std.instLawfulRcoIntersectionNat_4 : Std.Rcc.LawfulRcoIntersection ℕ
-- Mathlib.Order.Lattice
/-- Transfer `LinearOrder` across an `Equiv`.  -/
Equiv.linearOrder : {α : Type u} → {β : Type v} → α ≃ β → [LinearOrder β] → [DecidableEq α] → LinearOrder α
-- Mathlib.Topology.Connected.Basic
/-- The iUnion of connected sets indexed by a type with an archimedean successor (like `ℕ` or `ℤ`)
such that any two neighboring sets meet is preconnected.  -/
IsPreconnected.iUnion_of_chain : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] [inst_2 : SuccOrder β]
  [IsSuccArchimedean β] {s : β → Set α},
  (∀ (n : β), IsPreconnected (s n)) → (∀ (n : β), (s n ∩ s (Order.succ n)).Nonempty) → IsPreconnected (⋃ n, s n)
-- Mathlib.Order.Category.FinPartOrd
FinPartOrd.hasForgetToPartOrd : CategoryTheory.HasForget₂ FinPartOrd PartOrd
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonZeroHom.eq_1 : ∀ {α : Type u_2} [inst : Zero α], Set.singletonZeroHom = { toFun := singleton, map_zero' := ⋯ }
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Context.mk.injEq : ∀ (sharedExprs : Lean.Meta.Sym.SharedExprs) (config : Lean.Meta.Sym.Config) (sharedExprs_1 : Lean.Meta.Sym.SharedExprs)
  (config_1 : Lean.Meta.Sym.Config),
  ({ sharedExprs := sharedExprs, config := config } = { sharedExprs := sharedExprs_1, config := config_1 }) =
    (sharedExprs = sharedExprs_1 ∧ config = config_1)
-- Mathlib.Topology.Order.IntermediateValue
/-- Intermediate value theorem for two functions: if `f` and `g` are two functions continuous
on a preconnected set `s` and for some `a b ∈ s` we have `f a ≤ g a` and `g b ≤ f b`,
then for some `x ∈ s` we have `f x = g x`.  -/
IsPreconnected.intermediate_value₂ : ∀ {X : Type u} {α : Type v} [inst : TopologicalSpace X] [inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α]
  [OrderClosedTopology α] {s : Set X},
  IsPreconnected s →
    ∀ {a b : X},
      a ∈ s → b ∈ s → ∀ {f g : X → α}, ContinuousOn f s → ContinuousOn g s → f a ≤ g a → g b ≤ f b → ∃ x ∈ s, f x = g x
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Basic
MeasureTheory.VectorMeasure.variation_map_le : ∀ {X : Type u_1} {V : Type u_2} {mX : MeasurableSpace X} [inst : TopologicalSpace V] [inst_1 : ENormedAddCommMonoid V]
  [inst_2 : T2Space V] {μ : MeasureTheory.VectorMeasure X V} {Y : Type u_3} [inst_3 : MeasurableSpace Y] {φ : X → Y},
  (μ.map φ).variation ≤ MeasureTheory.Measure.map φ μ.variation
-- Mathlib.Algebra.Order.Module.Defs
PosSMulMono.toPosSMulReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β] [inst_3 : Zero α]
  [PosSMulMono α β], PosSMulReflectLT α β
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- `liminf` over `ℕ` is measurable. See `Measurable.liminf'` for a version with a general filter.
 -/
Measurable.liminf : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {f : ℕ → δ → α}, (∀ (i : ℕ), Measurable (f i)) → Measurable fun x => Filter.liminf (fun i => f i x) Filter.atTop
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonneg_of_nonpos_of_nonpos : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
  [AddRightReflectLE R], a ≤ 0 → b ≤ 0 → 0 ≤ a * b
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.mker.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), MonoidHom.mker f = Submonoid.comap f ⊥
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.substFunc.match_1.splitter : {L : FirstOrder.Language} →
  {L' : FirstOrder.Language} →
    {α : Type u_3} →
      (motive : L.Term α → ({n : ℕ} → L.Functions n → L'.Term (Fin n)) → Sort u_6) →
        (x : L.Term α) →
          (x_1 : {n : ℕ} → L.Functions n → L'.Term (Fin n)) →
            ((a : α) → (x : {n : ℕ} → L.Functions n → L'.Term (Fin n)) → motive (FirstOrder.Language.var a) x) →
              ((l : ℕ) →
                  (f : L.Functions l) →
                    (ts : Fin l → L.Term α) →
                      (tf : {n : ℕ} → L.Functions n → L'.Term (Fin n)) → motive (FirstOrder.Language.func f ts) tf) →
                motive x x_1
-- Mathlib.Data.Rel
/-- Composition of relation.

Note that this follows the `CategoryTheory` order of arguments.  -/
SetRel.«term_○_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Lie.Ideal
/-- The range of a morphism of Lie algebras as an ideal in the codomain.  -/
LieHom.idealRange : {R : Type u} →
  {L : Type v} →
    {L' : Type w₂} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieRing L'] → [inst_3 : LieAlgebra R L'] → [inst_4 : LieAlgebra R L] → (L →ₗ⁅R⁆ L') → LieIdeal R L'