mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.add_compat_right : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {a b c : FreeAlgebra.Pre R X}
  (a_1 : FreeAlgebra.Rel R X a b), FreeAlgebra.Rel.below a_1 → motive a b a_1 → FreeAlgebra.Rel.below ⋯
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkOrCached_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (aig : Std.Sat.AIG α) (input : aig.BinaryInput),
  aig.decls.size ≤ (aig.mkOrCached input).aig.decls.size
-- Mathlib.Analysis.Fourier.FiniteAbelian.Orthogonality
AddChar.expect_eq_ite : ∀ {G : Type u_1} {R : Type u_3} [inst : AddGroup G] [inst_1 : Fintype G] [inst_2 : Semifield R] [inst_3 : CharZero R]
  (ψ : AddChar G R), (Finset.univ.expect fun a => ψ a) = if ψ = 0 then 1 else 0
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.inv_rev : ∀ {α : Type u_1} {𝕜 : Type u_15} {𝕜' : Type u_16} [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜']
  {l : Filter α} {f : α → 𝕜} {g : α → 𝕜'},
  f =O[l] g → (∀ᶠ (x : α) in l, f x = 0 → g x = 0) → (fun x => (g x)⁻¹) =O[l] fun x => (f x)⁻¹
-- Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
/-- If `S` is finitely presented as a module over `R`, it is finitely
presented as an algebra over `R`.  -/
Algebra.FinitePresentation.of_finitePresentation : ∀ (R : Type u) (S : Type u_1) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Module.FinitePresentation R S], Algebra.FinitePresentation R S
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.arrowCongrEquiv_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R₁ →+* R₃} [inst_5 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {M₁ : Type u_4}
  [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_8 : TopologicalSpace M₂]
  [inst_9 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_10 : TopologicalSpace M₃] [inst_11 : AddCommMonoid M₃]
  {M₄ : Type u_7} [inst_12 : TopologicalSpace M₄] [inst_13 : AddCommMonoid M₄] [inst_14 : Module R₁ M₁]
  [inst_15 : Module R₂ M₂] [inst_16 : Module R₃ M₃] {R₄ : Type u_8} [inst_17 : Semiring R₄] [inst_18 : Module R₄ M₄]
  {σ₃₄ : R₃ →+* R₄} {σ₄₃ : R₄ →+* R₃} [inst_19 : RingHomInvPair σ₃₄ σ₄₃] [inst_20 : RingHomInvPair σ₄₃ σ₃₄]
  {σ₂₄ : R₂ →+* R₄} {σ₁₄ : R₁ →+* R₄} [inst_21 : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄]
  [inst_22 : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [inst_23 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] (e₁₂ : M₁ ≃SL[σ₁₂] M₂)
  (e₄₃ : M₄ ≃SL[σ₄₃] M₃) (f : M₁ →SL[σ₁₄] M₄), (e₁₂.arrowCongrEquiv e₄₃) f = ↑e₄₃ ∘SL f ∘SL ↑e₁₂.symm
-- Mathlib.Analysis.RCLike.Basic
RCLike.norm_re_le_norm : ∀ {K : Type u_1} [inst : RCLike K] (z : K), ‖RCLike.re z‖ ≤ ‖z‖
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- **Alias** of `MonoidAlgebra.mapRingEquiv_trans`. -/
MonoidAlgebra.mapRangeRingEquiv_trans : ∀ {R : Type u_3} {S : Type u_4} {T : Type u_5} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : Semiring T] [inst_3 : Monoid M] (e₁ : R ≃+* S) (e₂ : S ≃+* T),
  MonoidAlgebra.mapRingEquiv M (e₁.trans e₂) = (MonoidAlgebra.mapRingEquiv M e₁).trans (MonoidAlgebra.mapRingEquiv M e₂)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- A version of the definition of `skeletonLT` with open cells.  -/
Topology.RelCWComplex.iUnion_openCell_eq_skeletonLT : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  (n : ℕ∞), D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, Topology.RelCWComplex.openCell m j = ↑(Topology.RelCWComplex.skeletonLT C n)
-- Mathlib.RingTheory.TensorProduct.Maps
LinearMap.compl₂.congr_simp : ∀ {R : Type u_14} {R₂ : Type u_15} {R₃ : Type u_16} {R₄ : Type u_17} {R₅ : Type u_18} {M : Type u_19} {N : Type u_20}
  {P : Type u_21} {Q : Type u_22} [inst : Semiring R] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  [inst_3 : Semiring R₄] [inst_4 : Semiring R₅] {σ₂₃ : R₂ →+* R₃} {σ₄₂ : R₄ →+* R₂} {σ₄₃ : R₄ →+* R₃}
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : AddCommMonoid P] [inst_8 : AddCommMonoid Q]
  [inst_9 : Module R M] [inst_10 : Module R₂ N] [inst_11 : Module R₃ P] [inst_12 : Module R₄ Q] [inst_13 : Module R₅ P]
  [inst_14 : RingHomCompTriple σ₄₂ σ₂₃ σ₄₃] [inst_15 : SMulCommClass R₃ R₅ P] {σ₁₅ : R →+* R₅}
  (h h_1 : M →ₛₗ[σ₁₅] N →ₛₗ[σ₂₃] P), h = h_1 → ∀ (g g_1 : Q →ₛₗ[σ₄₂] N), g = g_1 → h.compl₂ g = h_1.compl₂ g_1
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The measure on `ℝ / ℤ` is a Haar measure.  -/
instIsAddHaarMeasureUnitAddCircleVolume : MeasureTheory.volume.IsAddHaarMeasure
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.id_comp : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (f : A →ₑ*[φ] B), (MulDistribMulActionHom.id N).comp f = f
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionLiteralSupportValueSet : Lean.FromJson Lean.Lsp.CodeActionLiteralSupportValueSet
-- Mathlib.RingTheory.FinitePresentation
Algebra.FinitePresentation.out : ∀ {R : Type w₁} {A : Type w₂} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  [self : Algebra.FinitePresentation R A], ∃ n f, Function.Surjective ⇑f ∧ (RingHom.ker f.toRingHom).FG
-- Mathlib.RingTheory.Valuation.LocalSubring
/-- A local subring integrally closed in a field is the intersection of valuation subrings
dominating it.  -/
LocalSubring.eq_iInf_of_isIntegrallyClosedIn : ∀ {K : Type u_3} [inst : Field K] {R : LocalSubring K} [IsIntegrallyClosedIn (↥R.toSubring) K],
  R.toSubring = ⨅ V, (↑V).toSubring
-- Mathlib.RingTheory.Spectrum.Prime.Topology
/-- [Stacks Tag 00HY](https://stacks.math.columbia.edu/tag/00HY) -/
PrimeSpectrum.isClosed_range_of_stableUnderSpecialization : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] (f : R →+* S),
  StableUnderSpecialization (Set.range (PrimeSpectrum.comap f)) → IsClosed (Set.range (PrimeSpectrum.comap f))
-- Init.Data.Array.Range
Array.find?_range'_eq_some : ∀ {s n i : ℕ} {p : ℕ → Bool},
  Array.find? p (Array.range' s n) = some i ↔
    p i = true ∧ i ∈ Array.range' s n ∧ ∀ (j : ℕ), s ≤ j → j < i → (!p j) = true
-- Mathlib.RepresentationTheory.Rep.Basic
/-- The `k`-linear `G`-representation on `k[G]`, induced by left multiplication.  -/
Rep.leftRegular : (k : Type u) → (G : Type v) → [inst : Ring k] → [inst_1 : Monoid G] → Rep.{max u v, u, v} k G
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.Heap.merge.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) (x x_1 : Batteries.BinomialHeap.Imp.Heap α),
  Batteries.BinomialHeap.Imp.Heap.merge le x x_1 =
    match x, x_1 with
    | Batteries.BinomialHeap.Imp.Heap.nil, h => h
    | h, Batteries.BinomialHeap.Imp.Heap.nil => h
    | s₁@h:(Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ t₁),
      s₂@h_1:(Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ t₂) =>
      if r₁ < r₂ then Batteries.BinomialHeap.Imp.Heap.cons r₁ a₁ n₁ (Batteries.BinomialHeap.Imp.Heap.merge le t₁ s₂)
      else
        if r₂ < r₁ then Batteries.BinomialHeap.Imp.Heap.cons r₂ a₂ n₂ (Batteries.BinomialHeap.Imp.Heap.merge le s₁ t₂)
        else
          match Batteries.BinomialHeap.Imp.combine le a₁ a₂ n₁ n₂ with
          | (a, n) =>
            have r := r₁ + 1;
            if t₁.rankGT r then
              if t₂.rankGT r then
                Batteries.BinomialHeap.Imp.Heap.cons r a n (Batteries.BinomialHeap.Imp.Heap.merge le t₁ t₂)
              else Batteries.BinomialHeap.Imp.Heap.merge le (Batteries.BinomialHeap.Imp.Heap.cons r a n t₁) t₂
            else
              if t₂.rankGT r then
                Batteries.BinomialHeap.Imp.Heap.merge le t₁ (Batteries.BinomialHeap.Imp.Heap.cons r a n t₂)
              else Batteries.BinomialHeap.Imp.Heap.cons r a n (Batteries.BinomialHeap.Imp.Heap.merge le t₁ t₂)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- the condition that `premap` is in the presieve  -/
CategoryTheory.Presieve.FunctorPushforwardStructure.cover : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {X : C} {S : CategoryTheory.Presieve X} {Y : D} {f : Y ⟶ F.obj X}
  (self : CategoryTheory.Presieve.FunctorPushforwardStructure F S f), S self.premap
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.groupSeminormClass : ∀ {E : Type u_3} [inst : Group E], GroupSeminormClass (GroupSeminorm E) E ℝ
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Reinterpret an equivariant monoid homomorphism as an equivariant function.  -/
MulDistribMulActionHom.toMulActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_4} →
            [inst_2 : Monoid A] →
              [inst_3 : MulDistribMulAction M A] →
                {B : Type u_5} → [inst_4 : Monoid B] → [inst_5 : MulDistribMulAction N B] → (A →ₑ*[φ] B) → A →ₑ[⇑φ] B
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.empty_sub : ∀ {α : Type u_2} [inst : Sub α] {s : Set α}, ∅ - s = ∅
-- Mathlib.Tactic.IntervalCases
/-- Given `a, b`, prove `a ≤ b` or fail.  -/
Mathlib.Tactic.IntervalCases.Methods.proveLE : Mathlib.Tactic.IntervalCases.Methods → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Matrix.Basic
Matrix.entryAddMonoidHom_eq_comp : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_11} [inst : AddZeroClass α] {i : m} {j : n},
  Matrix.entryAddMonoidHom α i j =
    ((Pi.evalAddMonoidHom (fun x => α) j).comp (Pi.evalAddMonoidHom (fun i => n → α) i)).comp ↑Matrix.ofAddEquiv.symm
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α]
  [inst : Inhabited α] {k : α}, (m₁ ∩ m₂).get! k = if k ∈ m₂ then m₁.get! k else default
-- Mathlib.Data.Matrix.DMatrix
DMatrix.instAdd : {m : Type u_1} → {n : Type u_2} → {α : m → n → Type v} → [(i : m) → (j : n) → Add (α i j)] → Add (DMatrix m n α)
-- Mathlib.Tactic.Ring.Common
/-- Create a new cache for `α` by doing the necessary instance searches.  -/
Mathlib.Tactic.Ring.Common.mkCache : {u : Lean.Level} → {α : Q(Type u)} → (sα : Q(CommSemiring «$α»)) → Lean.MetaM (Mathlib.Tactic.Ring.Common.Cache sα)
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- **Alias** of `AlgebraicGeometry.Scheme.Modules.isUnit_algebraMap_end_of_le_basicOpen`. -/
AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen : ∀ {R : CommRingCat} {M : (AlgebraicGeometry.Spec R).Modules} {U : (AlgebraicGeometry.Spec R).Opens} (f : ↑R),
  U ≤ PrimeSpectrum.basicOpen f → IsUnit ((algebraMap (↑R) (Module.End ↑R ↑(M.presheaf.obj (Opposite.op U)))) f)
-- Mathlib.GroupTheory.Subgroup.Saturated
AddSubgroup.saturated_iff_zsmul : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.NSMulSaturated ↔ ∀ (n : ℤ) (g : G), n • g ∈ H → n = 0 ∨ g ∈ H
-- Lean.Util.Path
_private.Lean.Util.Path.0.Lean.initSearchPathInternal : IO Unit
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.evaln.match_1.eq_9 : ∀ (motive : ℕ → Nat.Partrec.Code → Sort u_1) (k : ℕ) (cf : Nat.Partrec.Code) (h_1 : (x : Nat.Partrec.Code) → motive 0 x)
  (h_2 : (k : ℕ) → motive k.succ Nat.Partrec.Code.zero) (h_3 : (k : ℕ) → motive k.succ Nat.Partrec.Code.succ)
  (h_4 : (k : ℕ) → motive k.succ Nat.Partrec.Code.left) (h_5 : (k : ℕ) → motive k.succ Nat.Partrec.Code.right)
  (h_6 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.pair cg))
  (h_7 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.comp cg))
  (h_8 : (k : ℕ) → (cf cg : Nat.Partrec.Code) → motive k.succ (cf.prec cg))
  (h_9 : (k : ℕ) → (cf : Nat.Partrec.Code) → motive k.succ cf.rfind'),
  (match k.succ, cf.rfind' with
    | 0, x => h_1 x
    | k.succ, Nat.Partrec.Code.zero => h_2 k
    | k.succ, Nat.Partrec.Code.succ => h_3 k
    | k.succ, Nat.Partrec.Code.left => h_4 k
    | k.succ, Nat.Partrec.Code.right => h_5 k
    | k.succ, cf.pair cg => h_6 k cf cg
    | k.succ, cf.comp cg => h_7 k cf cg
    | k.succ, cf.prec cg => h_8 k cf cg
    | k.succ, cf.rfind' => h_9 k cf) =
    h_9 k cf
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem?_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂)[k]? = none
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSpace_mono : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π),
  τ ≤ π → hτ.measurableSpace ≤ hπ.measurableSpace
-- Mathlib.Analysis.LocallyConvex.WeakSpace
/-- If `E` is a locally convex space over `𝕜` (with `RCLike 𝕜`), and `s : Set E` is `ℝ`-convex, then
the closure of `s` and the weak closure of `s` coincide. More precisely, the topological closure
commutes with `toWeakSpace 𝕜 E`.

This holds more generally for any linear equivalence `e : E ≃ₗ[𝕜] F` between locally convex spaces
such that precomposition with `e` and `e.symm` preserves continuity of linear functionals. See
`LinearEquiv.image_closure_of_convex`.  -/
Convex.toWeakSpace_closure : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] [inst_3 : Module ℝ E]
  [IsScalarTower ℝ 𝕜 E] [inst_5 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [LocallyConvexSpace ℝ E] {s : Set E}, Convex ℝ s → ⇑(toWeakSpace 𝕜 E) '' closure s = closure (⇑(toWeakSpace 𝕜 E) '' s)
-- Mathlib.Analysis.Complex.BorelCaratheodory
/-- Norm inequality for the inverse Schwarz transform: if `‖w‖ < 1`, then
`‖2M * w / (1 + w)‖ ≤ 2M * ‖w‖ / (1 - ‖w‖)`.  -/
_private.Mathlib.Analysis.Complex.BorelCaratheodory.0.Complex.norm_two_mul_div_one_add_le : ∀ {M : ℝ} {w : ℂ}, 0 < M → ‖w‖ < 1 → ‖2 * ↑M * w / (1 + w)‖ ≤ 2 * M * ‖w‖ / (1 - ‖w‖)
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.map_apply_ι : ∀ {R : Type u_1} [inst : CommRing R] {M₁ : Type u_4} {M₂ : Type u_5} [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {Q₁ : QuadraticForm R M₁}
  {Q₂ : QuadraticForm R M₂} (f : Q₁ →qᵢ Q₂) (m : M₁),
  (CliffordAlgebra.map f) ((CliffordAlgebra.ι Q₁) m) = (CliffordAlgebra.ι Q₂) (f m)
-- Mathlib.Order.Filter.Curry
Filter.Tendsto.curry : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ},
  (∀ᶠ (a : α) in la, Filter.Tendsto (fun b => f a b) lb lc) → Filter.Tendsto (↿f) (la.curry lb) lc
-- Mathlib.MeasureTheory.PiSystem
/-- If `s` is in a Dynkin system `d`, we can form the new Dynkin system `{s ∩ t | t ∈ d}`.  -/
MeasurableSpace.DynkinSystem.restrictOn : {α : Type u_3} → (d : MeasurableSpace.DynkinSystem α) → {s : Set α} → d.Has s → MeasurableSpace.DynkinSystem α
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.instInnerRegularOfSigmaFinite : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] [MeasureTheory.SigmaFinite μ], μ.InnerRegular
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sub_of_left_eq_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v x = 0 → v (x - y) = v y
-- Init.Data.Int.Lemmas
Int.toNat_of_nonpos : ∀ {z : ℤ}, z ≤ 0 → z.toNat = 0
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.ofList_nil : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeSet.ofList [] cmp = ∅
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.reachable_iff_nonempty_univ : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Reachable u v ↔ Set.univ.Nonempty
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.get.congr_simp : ∀ {α : Type u} {δ : Type w} [inst : Ord α] (t t_1 : Std.DTreeMap.Internal.Impl α fun x => δ) (e_t : t = t_1) (k k_1 : α)
  (e_k : k = k_1) (hlk : Std.DTreeMap.Internal.Impl.contains k t = true),
  Std.DTreeMap.Internal.Impl.Const.get t k hlk = Std.DTreeMap.Internal.Impl.Const.get t_1 k_1 ⋯
-- Mathlib.Data.Multiset.Filter
Multiset.sub_filter_eq_filter_not : ∀ {α : Type u_1} [inst : DecidableEq α] (p : α → Prop) [inst_1 : DecidablePred p] (s : Multiset α),
  s - Multiset.filter p s = Multiset.filter (fun a => ¬p a) s
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.prodEquivalence_unitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D'),
  (CategoryTheory.CostructuredArrow.prodEquivalence S S' T T').unitIso =
    CategoryTheory.NatIso.ofComponents
      (fun f =>
        CategoryTheory.Iso.refl
          ((CategoryTheory.Functor.id (CategoryTheory.CostructuredArrow (S.prod S') (T, T'))).obj f))
      ⋯
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_support : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)]
  (f : Π₀ (x : ι), M), f.toFinsupp.support = f.support
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Int
Int.reduceAdd : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.l_hom.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C] (X : CategoryTheory.FreeMonoidalCategory C),
  sizeOf (CategoryTheory.FreeMonoidalCategory.Hom.l_hom X) = 1 + sizeOf X
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.leftOp_inverse_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ Dᵒᵖ) (X : D), e.leftOp.inverse.obj X = Opposite.op (e.inverse.obj (Opposite.op X))
-- Mathlib.LinearAlgebra.Pi
LinearMap.single_eq_pi_diag : ∀ (R : Type u) {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (i : ι),
  LinearMap.single R φ i = LinearMap.pi (LinearMap.diag i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- The deduplication of `E` refines `E`.  -/
CategoryTheory.PreZeroHypercover.fromShrink : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {S : C} → (E : CategoryTheory.PreZeroHypercover S) → E.shrink.Hom E
-- Mathlib.Analysis.Complex.Trigonometric
Real.neg_one_le_sin : ∀ (x : ℝ), -1 ≤ Real.sin x
-- Mathlib.CategoryTheory.Monoidal.Action.End
CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop_obj_unmop_obj : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (X : C) (y : D),
  ((CategoryTheory.MonoidalCategory.MonoidalLeftAction.curriedActionMop C D).obj X).unmop.obj y =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj X y
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L]
  [LieModule.IsTriangularizable K (↥H) L] [PerfectField K] {α : ↥H → K} {x : L},
  x ∈ LieAlgebra.rootSpace H α → ∀ (h : ↥H), ⁅h, x⁆ = α h • x
-- Std.Http.Data.Headers.Basic
/-- The `Expect` header.

Represents an expectation token.
The only standardized expectation is `100-continue`.

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-expect
 -/
Std.Http.Header.Expect : Type
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffWithinAt_iff_source_of_mem_maximalAtlas : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {e : OpenPartialHomeomorph M H}
  {f : M → M'} {s : Set M} {x : M} {n : WithTop ℕ∞},
  e ∈ IsManifold.maximalAtlas I n M →
    x ∈ e.source →
      (ContMDiffWithinAt I I' n f s x ↔
        ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(e.extend I).symm)
          (↑(e.extend I).symm ⁻¹' s ∩ Set.range ↑I) (↑(e.extend I) x))
-- Mathlib.Data.NNRat.Defs
Rat.toNNRat_lt_toNNRat_iff' : ∀ {p q : ℚ}, q.toNNRat < p.toNNRat ↔ q < p ∧ 0 < p
-- Mathlib.MeasureTheory.Measure.Support
/-- A point `x` is in the support of `μ` if any open neighborhood of `x` has positive measure.
We provide the definition in terms of the filter-theoretic equivalent
`∃ᶠ u in (𝓝 x).smallSets, 0 < μ u`.  -/
MeasureTheory.Measure.support : {X : Type u_1} → [TopologicalSpace X] → [inst : MeasurableSpace X] → MeasureTheory.Measure X → Set X
-- Mathlib.Order.Max
instNoMaxOrderForallOfNonempty : ∀ {ι : Type u} {π : ι → Type u_3} [Nonempty ι] [inst : (i : ι) → Preorder (π i)] [∀ (i : ι), NoMaxOrder (π i)],
  NoMaxOrder ((i : ι) → π i)
-- Std.Time.Time.Unit.Minute
/-- `Offset` represents a duration offset in minutes.
 -/
Std.Time.Minute.Offset : Type
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.subgroupOf_range_eq_of_le : ∀ {G₁ : Type u_7} {G₂ : Type u_8} [inst : Group G₁] [inst_1 : Group G₂] {K : Subgroup G₂} (f : G₁ →* G₂)
  (h : f.range ≤ K), f.range.subgroupOf K = (f.codRestrict K ⋯).range
-- Mathlib.MeasureTheory.Function.EssSup
essInf_cond_count_eq_ciInf : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : ConditionallyCompleteLattice β] {f : α → β} [Nonempty α]
  [MeasurableSingletonClass α] [Finite α],
  BddBelow (Set.range f) → essInf f (ProbabilityTheory.uniformOn Set.univ) = ⨅ a, f a
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
/-- Two equivalent open partial homeomorphisms have the same target.  -/
OpenPartialHomeomorph.EqOnSource.target_eq : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  {e e' : OpenPartialHomeomorph X Y}, e ≈ e' → e.target = e'.target
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.mkOfUnitCounit_counit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : CategoryTheory.Adjunction.CoreUnitCounit F G),
  (CategoryTheory.Adjunction.mkOfUnitCounit adj).counit = adj.counit
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
/-- The isomorphism `(K.restriction e).cycles j ≅ K.cycles j'` when `e.f j = j'`
and the successors `k` and `k'` of `j` and `j'` satisfy `e.f k = k'`.  -/
HomologicalComplex.restrictionCyclesIso : {ι : 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 : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsRelIff] →
                    (j k : ι) →
                      c.next j = k →
                        {j' k' : ι'} →
                          e.f j = j' →
                            e.f k = k' →
                              c'.next j' = k' →
                                [inst_3 : K.HasHomology j'] →
                                  [inst_4 : (K.restriction e).HasHomology j] → (K.restriction e).cycles j ≅ K.cycles j'