mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_toArray : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.toArray.isEmpty = t.isEmpty
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_zero : ∀ {R : Type u_1} {a b : R} [inst : Zero R], QuadraticAlgebra.C 0 = 0
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
not_isStationary_empty : ∀ {α : Type v} [inst : LinearOrder α], ¬IsStationary ∅
-- Mathlib.Order.Max
IsMax.eq_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, IsMax a → a ≤ b → b = a
-- Mathlib.LinearAlgebra.Orientation
/-- An orientation of a module, intended to be used when `ι` is a `Fintype` with the same
cardinality as a basis.  -/
Orientation : (R : Type u_1) →
  [inst : CommSemiring R] →
    [inst_1 : PartialOrder R] →
      [IsStrictOrderedRing R] →
        (M : Type u_2) → [inst_3 : AddCommMonoid M] → [Module R M] → Type u_4 → Type (max (max u_4 u_1) u_2)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.isUniform_comm : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] (G : SimpleGraph α)
  [inst_2 : DecidableRel G.Adj] {ε : 𝕜} {s t : Finset α}, G.IsUniform ε s t ↔ G.IsUniform ε t s
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.ObjectProperty.instHasInducedTStructureMinOfIsClosedUnderIsomorphisms : ∀ {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]
  (P P' : CategoryTheory.ObjectProperty C) [inst_6 : P.IsTriangulated] [inst_7 : P'.IsTriangulated]
  (t : CategoryTheory.Triangulated.TStructure C) [P.HasInducedTStructure t] [P'.HasInducedTStructure t]
  [inst_10 : P.IsClosedUnderIsomorphisms] [P'.IsClosedUnderIsomorphisms], (P ⊓ P').HasInducedTStructure t
-- Lean.Server.InfoUtils
Lean.Elab.Info.contains : Lean.Elab.Info → String.Pos.Raw → optParam Bool false → Bool
-- Mathlib.RingTheory.Valuation.Basic
AddValuation.IsEquiv.ne_top : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : LinearOrderedAddCommMonoidWithTop Γ₀]
  [inst_1 : LinearOrderedAddCommMonoidWithTop Γ'₀] [inst_2 : Ring R] {v₁ : AddValuation R Γ₀} {v₂ : AddValuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {r : R}, v₁ r ≠ ⊤ ↔ v₂ r ≠ ⊤
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.faceι.congr_simp : ∀ {n : ℕ} (i j : Fin (n + 1)) (hij : j ≠ i), SSet.horn.faceι i j hij = SSet.horn.faceι i j hij
-- Std.Data.DHashMap.Basic
Std.DHashMap.mk : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] → [inst_1 : Hashable α] → (inner : Std.DHashMap.Raw α β) → inner.WF → Std.DHashMap α β
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The product of almost everywhere measurable functions is measurable.  -/
AEMeasurable.tprod : ∀ {X : Type u_6} {E : Type u_7} {ι : Type u_8} [inst : MeasurableSpace X] [inst_1 : CommMonoid E]
  [inst_2 : TopologicalSpace E] [TopologicalSpace.IsCompletelyPseudoMetrizableSpace E] [SecondCountableTopology E]
  [inst_5 : MeasurableSpace E] [BorelSpace E] [MeasurableMul₂ E] [Countable ι] {L : SummationFilter ι} [L.NeBot]
  [L.filter.IsCountablyGenerated] {μ : MeasureTheory.Measure X} {f : ι → X → E},
  (∀ (i : ι), AEMeasurable (f i) μ) → AEMeasurable (fun x => ∏'[L] (i : ι), f i x) μ
-- Mathlib.Data.Int.LeastGreatest
Int.greatestOfBdd.congr_simp : ∀ {P : ℤ → Prop} [inst : DecidablePred P] (b b_1 : ℤ) (e_b : b = b_1) (Hb : ∀ (z : ℤ), P z → z ≤ b) (Hinh : ∃ z, P z),
  b.greatestOfBdd Hb Hinh = b_1.greatestOfBdd ⋯ Hinh
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix₂'_compl₂ : ∀ {n : Type u_11} {m : Type u_12} {m' : Type u_14} {R : Type u_16} [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : DecidableEq m] [inst_5 : Fintype m'] [inst_6 : DecidableEq m']
  (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (f : (m' → R) →ₗ[R] m → R),
  (LinearMap.toMatrix₂' R) (B.compl₂ f) = (LinearMap.toMatrix₂' R) B * LinearMap.toMatrix' f
-- Mathlib.Topology.Algebra.Group.Basic
Subgroup.instIsTopologicalGroupSubtypeMem : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (S : Subgroup G),
  IsTopologicalGroup ↥S
-- Mathlib.CategoryTheory.Limits.Shapes.PiProd
CategoryTheory.Limits.hasBinaryProduct_of_products : ∀ {C : Type u_1} {I : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : I → C} (P : I → Prop)
  [CategoryTheory.Limits.HasProduct X] [inst_2 : CategoryTheory.Limits.HasProduct fun i => X ↑i]
  [inst_3 : CategoryTheory.Limits.HasProduct fun i => X ↑i],
  CategoryTheory.Limits.HasBinaryProduct (∏ᶜ fun i => X ↑i) (∏ᶜ fun i => X ↑i)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.rel_eq_coe : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon R), ⇑c.toSetoid = ⇑c
-- Mathlib.MeasureTheory.Measure.AEDisjoint
/-- **Alias** of `MeasureTheory.AEDisjoint.stdSymm`. -/
MeasureTheory.AEDisjoint.symmetric : ∀ {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}, Std.Symm (MeasureTheory.AEDisjoint μ)
-- Mathlib.Data.NNReal.Star
instStarModuleNNRealOfReal : ∀ {E : Type u_1} [inst : AddCommMonoid E] [inst_1 : Star E] [inst_2 : Module ℝ E] [StarModule ℝ E], StarModule NNReal E
-- Init.Data.List.MinMaxOn
List.isSome_maxOn?_iff : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] {f : α → β} {xs : List α},
  (List.maxOn? f xs).isSome = true ↔ xs ≠ []
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.centralizer_toAddSubsemigroup : ∀ {M : Type u_1} (S : Set M) [inst : AddMonoid M],
  (AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
ContMDiff.extend_zero : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] [T2Space M]
  [inst_12 : Zero M'] {n : WithTop ℕ∞} {U : TopologicalSpace.Opens M} {f : ↥U → M'},
  HasCompactSupport f → ContMDiff I I' n f → ContMDiff I I' n (Function.extend Subtype.val f 0)
-- Mathlib.Data.Finsupp.Basic
/-- When `f` is an embedding we have an embedding `(α →₀ ℕ) ↪ (β →₀ ℕ)` given by `mapDomain`.  -/
Finsupp.mapDomainEmbedding : {α : Type u_12} → {β : Type u_13} → (α ↪ β) → (α →₀ ℕ) ↪ β →₀ ℕ
-- Mathlib.NumberTheory.Modular
ModularGroup.stabilizer_I : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ},
  g • UpperHalfPlane.I = UpperHalfPlane.I ↔ g ∈ {1, -1, ModularGroup.S, -ModularGroup.S}
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Adding the angles between two vectors in each order, with the first vector in each angle
negated, results in 0.  -/
Orientation.oangle_add_oangle_rev_neg_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), o.oangle (-x) y + o.oangle (-y) x = 0
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.decodeFun.match_1.splitter : {n : ℕ} →
  (motive : (x : ℕ) → Fin (n ^ x) → Sort u_1) →
    (x : ℕ) →
      (x_1 : Fin (n ^ x)) →
        ((x : Fin (n ^ 0)) → motive 0 x) → ((m k : ℕ) → (hk : k < n ^ (m + 1)) → motive m.succ ⟨k, hk⟩) → motive x x_1
-- Mathlib.Order.Hom.BoundedLattice
/-- Special case of `map_symmDiff` for Boolean algebras.  -/
map_symmDiff' : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β]
  [inst_2 : FunLike F α β] [BoundedLatticeHomClass F α β] (f : F) (a b : α), f (symmDiff a b) = symmDiff (f a) (f b)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.notMem_uIcc_of_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, c < a → c < b → c ∉ Set.uIcc a b
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- Reindex the indexing type of an effective epi family struct.
 -/
CategoryTheory.EffectiveEpiFamilyStruct.reindex : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B : C} →
      {α : Type u_2} →
        {α' : Type u_3} →
          (X : α → C) →
            (π : (a : α) → X a ⟶ B) →
              (e : α' ≃ α) →
                (CategoryTheory.EffectiveEpiFamilyStruct (fun a => X (e a)) fun a => π (e a)) →
                  CategoryTheory.EffectiveEpiFamilyStruct X π
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.dirac_unit_compProd_const : ∀ {β : Type u_2} {mβ : MeasurableSpace β} (μ : MeasureTheory.Measure β) [MeasureTheory.SFinite μ],
  (MeasureTheory.Measure.dirac ()).compProd (ProbabilityTheory.Kernel.const Unit μ) =
    MeasureTheory.Measure.map (Prod.mk ()) μ
-- Init.Data.String.Termination
String.Slice.Pos.instWellFoundedRelationDown : {s : String.Slice} → WellFoundedRelation (String.Slice.Pos.Down s)
-- Mathlib.Algebra.Order.Sub.Defs
/-- This lemma (and some of its corollaries) also holds for `ENNReal`, but this proof doesn't work
for it. Maybe we should add this lemma as field to `OrderedSub`?  -/
lt_tsub_of_add_lt_left : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a + c < b → c < b - a
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.lift_unique : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f] (g : M →ₗ[R] M'')
  (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (l : M' →ₗ[R] M''),
  l ∘ₗ f = g → IsLocalizedModule.lift S f g h = l
-- Lean.Server.Completion.CompletionUtils
Lean.Server.Completion.unfoldDefinitionGuarded? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f p : Polynomial R),
  (AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).symm
      ((DoubleQuot.quotQuotMk (Ideal.map Polynomial.C I) (Ideal.span {f})) p) =
    (Ideal.Quotient.mk (Ideal.map (Ideal.Quotient.mk (Ideal.span {f})) (Ideal.map Polynomial.C I)))
      ((AdjoinRoot.mk f) p)
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_single_mul_eq_mul_coeff`. -/
MonoidAlgebra.single_mul_apply_aux : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x : MonoidAlgebra R M} {r : R} {m m₁ : M} [inst_1 : Mul M]
  (m₂ : M), (∀ m' ∈ x.coeff.support, m * m' = m₁ ↔ m' = m₂) → (MonoidAlgebra.single m r * x).coeff m₁ = r * x.coeff m₂
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.notConvergentSeqLTIndex_spec : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace α} [inst : PseudoEMetricSpace β]
  {μ : MeasureTheory.Measure α} {s : Set α} {ε : ℝ} {f : ι → α → β} {g : α → β} [inst_1 : SemilatticeSup ι]
  [inst_2 : Nonempty ι] [inst_3 : Countable ι] (hε : 0 < ε) (hf : ∀ (n : ι), Measurable fun a => edist (f n a) (g a))
  (hsm : MeasurableSet s) (hs : μ s ≠ ⊤)
  (hfg : ∀ᵐ (x : α) ∂μ, x ∈ s → Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (g x))) (n : ℕ),
  μ
      (s ∩
        MeasureTheory.Egorov.notConvergentSeq f g n (MeasureTheory.Egorov.notConvergentSeqLTIndex hε hf hsm hs hfg n)) ≤
    ENNReal.ofReal (ε * 2⁻¹ ^ n)
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A morphism `k : S.X₂ ⟶ A` such that `S.f ≫ k = 0` descends to a morphism `S.opcycles ⟶ A`.  -/
CategoryTheory.ShortComplex.descOpcycles : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        {A : C} →
          (k : S.X₂ ⟶ A) → CategoryTheory.CategoryStruct.comp S.f k = 0 → [inst_2 : S.HasRightHomology] → S.opcycles ⟶ A
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.Δ_of_isCharTwoJEqZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJEqZeroNF],
  W.Δ = -(64 * W.a₄ ^ 3 + 27 * W.b₆ ^ 2)
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.inner_eq_ite : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : OrthonormalBasis ι 𝕜 E) (i j : ι),
  inner 𝕜 (b i) (b j) = if i = j then 1 else 0
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun.eq_1 : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} (μ : MeasureTheory.Measure α)
  (T : Set α → E →L[ℝ] F) {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : α → E),
  MeasureTheory.setToFun μ T hT f =
    if _hF : CompleteSpace F then
      if hf : MeasureTheory.Integrable f μ then (MeasureTheory.L1.setToL1 hT) (MeasureTheory.Integrable.toL1 f hf)
      else 0
    else 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- **Alias** of the forward direction of `pow_le_pow_iff_left`. -/
le_of_pow_le_pow_left' : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M] {a b : M}
  {n : ℕ}, n ≠ 0 → a ^ n ≤ b ^ n → a ≤ b
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
Affine.Simplex.faceOpposite_restrict : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) {S : AffineSubspace k P}
  (hS : affineSpan k (Set.range s.points) ≤ S) (i : Fin (n + 1)),
  (s.restrict S hS).faceOpposite i = (s.faceOpposite i).restrict S ⋯
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.ord.congr_simp : ∀ (I : Type u) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] (i i_1 : I),
  i = i_1 → Profinite.NobelingProof.ord I i = Profinite.NobelingProof.ord I i_1
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- Construct a natural transformation between profunctors from a `ProfunctorCore.Hom`.  -/
CategoryTheory.Profunctor.ofHom : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {P Q : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D} →
          P.Hom Q → (CategoryTheory.Profunctor.ofCore P ⟶ CategoryTheory.Profunctor.ofCore Q)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_count' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {f : α → ENNReal},
  Measurable f → ∫⁻ (a : α), f a ∂MeasureTheory.Measure.count = ∑' (a : α), f a
-- Mathlib.Analysis.Convex.Side
AffineSubspace.sSameSide_comm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SSameSide x y ↔ s.SSameSide y x
-- Init.Data.Vector.Lemmas
Vector.foldlM_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] {f : β → α → m β} {init : β},
  Vector.foldlM f init #v[] = pure init
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.eq_C_of_natDegree_eq_zero : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.natDegree = 0 → p = Polynomial.C (p.coeff 0)
-- Mathlib.ModelTheory.Basic
FirstOrder.Language.HomClass.map_constants : ∀ {L : FirstOrder.Language} {F : Type u_3} {M : Type u_4} {N : Type u_5} [inst : L.Structure M] [inst_1 : L.Structure N]
  [inst_2 : FunLike F M N] [L.HomClass F M N] (φ : F) (c : L.Constants), φ ↑c = ↑c
-- Mathlib.Combinatorics.Quiver.SingleObj
Quiver.SingleObj.toPrefunctor_apply_map : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {X Y : Quiver.SingleObj α} (a : α),
  (Quiver.SingleObj.toPrefunctor f).map a = f a
-- Mathlib.Algebra.Order.Monoid.Unbundled.Units
/-- **Alias** of the reverse direction of `Units.inv_mul_le_iff`. -/
Units.inv_mul_le_of_le_mul : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : LE M] [MulLeftMono M] (u : Mˣ) {a b : M}, a ≤ ↑u * b → ↑u⁻¹ * a ≤ b
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.exists_rep : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.RationalMap Y), ∃ g, g.toRationalMap = f
-- Mathlib.Topology.Algebra.Valued.NormedValued
Valuation.norm_eq_zero : ∀ {L : Type u_1} [inst : Field L] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation L Γ₀)
  [hv : v.RankOne] {x : L}, v.norm x = 0 → x = 0
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Iso.toEmbedding_completeGraph : ∀ {α : Type u_5} {β : Type u_6} (f : α ≃ β),
  (SimpleGraph.Iso.completeGraph f).toEmbedding = SimpleGraph.Embedding.completeGraph f.toEmbedding
-- Lean.Data.Lsp.CodeActions
/-- CodeActionKinds that this server may return.

The list of kinds may be generic, such as `"refactor"`, or the server may list out every specific kind they provide.  -/
Lean.Lsp.CodeActionOptions.codeActionKinds? : Lean.Lsp.CodeActionOptions → Option (Array Lean.Lsp.CodeActionKind)
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.addToDerive : Lean.Name → Lean.Expr → Lean.Elab.ConfigEval.M✝ Unit
-- Std.Time.Zoned.TimeZone
Std.Time.TimeZone.Offset.ext_iff : ∀ {x y : Std.Time.TimeZone.Offset}, x = y ↔ x.second = y.second
-- Mathlib.CategoryTheory.Types.Monomorphisms
CategoryTheory.Types.instIsStableUnderFilteredColimitsMonomorphismsType : CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{v', u', u, u + 1}
  (CategoryTheory.MorphismProperty.monomorphisms (Type u))
-- Mathlib.Data.Int.Bitwise
/-- `ldiff a b` performs bitwise set difference. For each corresponding
pair of bits taken as Booleans, say `aᵢ` and `bᵢ`, it applies the
Boolean operation `aᵢ ∧ ¬bᵢ` to obtain the `iᵗʰ` bit of the result.  -/
Int.ldiff : ℤ → ℤ → ℤ
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
/-- The canonical map from the restriction to the subspace.  -/
AlgebraicGeometry.LocallyRingedSpace.ofRestrict : {U : TopCat} →
  (X : AlgebraicGeometry.LocallyRingedSpace) →
    {f : U ⟶ X.toTopCat} → (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) → X.restrict h ⟶ X
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.instUnopOfProjectiveOpposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : Cᵒᵖ} [CategoryTheory.Projective P],
  CategoryTheory.Injective (Opposite.unop P)
-- Mathlib.Algebra.Group.Basic
eq_sub_of_add_eq : ∀ {G : Type u_3} [inst : AddGroup G] {a b c : G}, a + c = b → a = b - c
-- Lean.Data.Options
Lean.Options.insert : Lean.Options → Lean.Name → Lean.DataValue → Lean.Options
-- Init.Data.UInt.Bitwise
UInt32.toFin_shiftLeft : ∀ (a b : UInt32), b < 32 → (a <<< b).toFin = a.toFin <<< b.toFin
-- Mathlib.Order.Grade
grade_self : ∀ {α : Type u_3} [inst : Preorder α] (a : α), grade α a = a
-- Mathlib.Algebra.Category.Grp.Injective
AddCommGrpCat.injective_of_divisible : ∀ (A : Type u) [inst : AddCommGroup A] [DivisibleBy A ℤ], CategoryTheory.Injective (AddCommGrpCat.of A)
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- The measure of a closed set is at most the integral of any function in a decreasing
approximating sequence to the indicator of the set.  -/
HasOuterApproxClosed.measure_le_lintegral : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : HasOuterApproxClosed X] {F : Set X} (hF : IsClosed F)
  [inst_2 : MeasurableSpace X] [OpensMeasurableSpace X] (μ : MeasureTheory.Measure X) (n : ℕ),
  μ F ≤ ∫⁻ (x : X), ↑((hF.apprSeq n) x) ∂μ
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalTermApplyNewGoals.evalTerm : Lean.Term → Lean.Elab.TermElabM (Lean.Meta.ApplyNewGoals × Lean.Expr)
-- Mathlib.Algebra.Category.Semigrp.Basic
mulEquivIsoSemigrpIso.eq_1 : ∀ {X Y : Type u} [inst : Semigroup X] [inst_1 : Semigroup Y],
  mulEquivIsoSemigrpIso =
    { hom := TypeCat.ofHom fun e => e.toSemigrpIso, inv := TypeCat.ofHom fun i => i.semigrpIsoToMulEquiv,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.RingTheory.RingHom.FaithfullyFlat
RingHom.FaithfullyFlat.respectsIso : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => RingHom.FaithfullyFlat
-- Std.Async.IO
Std.Async.IO.AsyncStream.next : {α : Type} → {β : outParam Type} → [self : Std.Async.IO.AsyncStream α β] → α → Std.Async.Selector β
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffInv₀.mk : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : Inv G] [inst_5 : Zero G] [inst_6 : TopologicalSpace G] [inst_7 : ChartedSpace H G],
  (∀ ⦃x : G⦄, x ≠ 0 → ContMDiffAt I I n (fun y => y⁻¹) x) → ContMDiffInv₀ I n G
-- Mathlib.LinearAlgebra.TensorProduct.Finiteness
/-- For any element `x` of `M ⊗[R] N`, there exists a (finite) multiset `{ (m_i, n_i) }`
of `M × N`, such that `x` is equal to the sum of `m_i ⊗ₜ[R] n_i`.  -/
TensorProduct.exists_multiset : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (x : TensorProduct R M N),
  ∃ S, x = (Multiset.map (fun i => i.1 ⊗ₜ[R] i.2) S).sum
-- Init.Meta.Defs
Lean.TSyntax.expandInterpolatedStrChunks : Array Lean.Syntax →
  (Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax) →
    (Lean.Syntax → Lean.MacroM Lean.Syntax) → (String → Lean.MacroM Lean.Syntax) → Lean.MacroM Lean.Syntax
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.alter.match_3.eq_1 : ∀ (motive : Ordering → Sort u_1) (h_1 : Ordering.lt = Ordering.lt → motive Ordering.lt)
  (h_2 : Ordering.lt = Ordering.gt → motive Ordering.gt) (h_3 : Ordering.lt = Ordering.eq → motive Ordering.eq),
  (match h : Ordering.lt with
    | Ordering.lt => h_1 h
    | Ordering.gt => h_2 h
    | Ordering.eq => h_3 h) =
    h_1 ⋯
-- Mathlib.CategoryTheory.Shift.CommShiftTwo
CategoryTheory.CommShift₂Setup.mk.sizeOf_spec : ∀ {D : Type u_5} [inst : CategoryTheory.Category.{v_5, u_5} D] {M : Type u_6} [inst_1 : AddCommMonoid M]
  [inst_2 : CategoryTheory.HasShift D M] [inst_3 : SizeOf D] [inst_4 : SizeOf M]
  (toTwistShiftData :
    CategoryTheory.TwistShiftData (CategoryTheory.PullbackShift D (AddMonoidHom.fst M M + AddMonoidHom.snd M M))
      (M × M))
  (z_zero₁ :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (0, m₁) (0, m₂) = 1) CategoryTheory.CommShift₂Setup.z_zero₁._autoParam)
  (z_zero₂ :
    autoParam (∀ (m₁ m₂ : M), toTwistShiftData.z (m₁, 0) (m₂, 0) = 1) CategoryTheory.CommShift₂Setup.z_zero₂._autoParam)
  (ε : M → M → (CategoryTheory.CatCenter D)ˣ)
  (hε :
    autoParam (∀ (m n : M), ε m n = (toTwistShiftData.z (0, n) (m, 0))⁻¹ * toTwistShiftData.z (m, 0) (0, n))
      CategoryTheory.CommShift₂Setup.hε._autoParam),
  sizeOf { toTwistShiftData := toTwistShiftData, z_zero₁ := z_zero₁, z_zero₂ := z_zero₂, ε := ε, hε := hε } =
    1 + sizeOf toTwistShiftData
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.coe_symm_toEquiv : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  ⇑h.symm = ⇑h.symm
-- Mathlib.GroupTheory.FreeGroup.Reduce
/-- The first theorem that characterises the function `reduce`: a word reduces to its
maximal reduction.  -/
FreeAddGroup.reduce.red : ∀ {α : Type u_1} {L : List (α × Bool)} [inst : DecidableEq α], FreeAddGroup.Red L (FreeAddGroup.reduce L)
-- Mathlib.Computability.Reduce
disjoin_manyOneReducible : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable γ]
  {p : α → Prop} {q : β → Prop} {r : γ → Prop}, p ≤₀ r → q ≤₀ r → Sum.elim p q ≤₀ r