mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDiv : {α : Type u_1} → [Div α] → Div αᵒᵈ
-- Lean.DocString.Types
Lean.Doc.instAppendInline : {i : Type u_1} → Append (Lean.Doc.Inline i)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.Language.presburger.realize_natCast : ∀ {α : Type u_1} {M : Type u_2} {v : α → M} [inst : AddMonoidWithOne M] {n : ℕ},
  FirstOrder.Language.Term.realize v ↑n = ↑n
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.instIsScalarTowerResidueField : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsLocalRing R] {R₁ : Type u_4} {R₂ : Type u_5} [inst_2 : CommRing R₁]
  [inst_3 : CommRing R₂] [inst_4 : Algebra R₁ R₂] [inst_5 : Algebra R₁ R] [inst_6 : Algebra R₂ R]
  [IsScalarTower R₁ R₂ R], IsScalarTower R₁ R₂ (IsLocalRing.ResidueField R)
-- Lean.Elab.DeclModifiers
Lean.Elab.ExpandDeclIdResult.mk.sizeOf_spec : ∀ (shortName declName : Lean.Name) (levelNames : List Lean.Name)
  (docString? : Option (Lean.TSyntax `Lean.Parser.Command.docComment)),
  sizeOf { shortName := shortName, declName := declName, levelNames := levelNames, docString? := docString? } =
    1 + sizeOf shortName + sizeOf declName + sizeOf levelNames + sizeOf docString?
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {K L : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} (f : K ⟶ L) (n : ι),
  (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f).f.f n = (f.f n).f
-- Mathlib.Logic.Encodable.Basic
_private.Mathlib.Logic.Encodable.Basic.0.Encodable.decodeSum.match_1.eq_1 : ∀ (motive : Bool → ℕ → Sort u_1) (m : ℕ) (h_1 : (m : ℕ) → motive false m) (h_2 : (x : Bool) → (m : ℕ) → motive x m),
  (match false, m with
    | false, m => h_1 m
    | x, m => h_2 x m) =
    h_1 m
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toArray_roo_eq_zero : ∀ {m n i : ℕ}, n ≤ i + (m + 1) → (m<...n).toArray[i]! = 0
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_insert : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k} {h₁ : a ∈ m.insert k v},
  (m.insert k v).getKey a h₁ = if h₂ : (k == a) = true then k else m.getKey a ⋯
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instPreservesColimitsOfShapeOppositeCommRingCatSchemeDiscreteSpecOfFinite : ∀ {J : Type u_1} [Finite J],
  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete J) AlgebraicGeometry.Scheme.Spec
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_sub_pi_div_two : ∀ (x : ℂ), Complex.sin (x - ↑Real.pi / 2) = -Complex.cos x
-- Mathlib.Data.Ordmap.Ordset
Ordnode.insert'_eq_insertWith : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLE α] (x : α) (t : Ordnode α),
  Ordnode.insert' x t = Ordnode.insertWith id x t
-- Mathlib.Topology.LocalAtTarget
/-- **Alias** of `Set.restrictPreimage_isClosedEmbedding`. -/
Topology.IsClosedEmbedding.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} (s : Set β),
  Topology.IsClosedEmbedding f → Topology.IsClosedEmbedding (s.restrictPreimage f)
-- Mathlib.Topology.UniformSpace.Cauchy
/-- Every Cauchy sequence over `ℕ` is totally bounded.  -/
CauchySeq.totallyBounded_range : ∀ {α : Type u} [uniformSpace : UniformSpace α] {s : ℕ → α}, CauchySeq s → TotallyBounded (Set.range s)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_comp_functorπ_assoc : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (a : α) {Z : CategoryTheory.Functor (α → C) C}
  (h : CategoryTheory.Pi.eval (fun x => C) a ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.functorπ a) h) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.piEquivalenceFunctorDiscrete α C).functor.whiskerLeft (CategoryTheory.Limits.lim.π { as := a }))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.piEquivalenceFunctorDiscreteCompEvaluationIso C a).hom h)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.neg_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (f : CauSeq β abv) (i : ℕ), ↑(-f) i = -↑f i
-- Mathlib.Topology.Sheaves.PresheafOfFunctions
TopCat.presheafToTop_obj : ∀ (X T : TopCat) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (X.presheafToTop T).obj U = ((TopologicalSpace.Opens.toTopCat X).obj (Opposite.unop U) ⟶ T)
-- Batteries.Data.UInt
UInt8.toNat_max : ∀ (x y : UInt8), (x ⊔ y).toNat = max x.toNat y.toNat
-- Mathlib.Topology.MetricSpace.Dilation
Isometry.toDilation_ratio : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β}
  {hf : Isometry f}, Dilation.ratio (Isometry.toDilation f hf) = 1
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.ofSliceTo_prev : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos} {h : p ≠ (s.sliceTo p₀).startPos},
  String.Slice.Pos.ofSliceTo (p.prev h) = (String.Slice.Pos.ofSliceTo p).prev ⋯
-- Batteries.Data.List.Lemmas
List.idxOfNth_nil : ∀ {α : Type u_1} {x : α} {n : ℕ} [inst : BEq α], List.idxOfNth x [] n = 0
-- Aesop.Rule
Aesop.NormSimpRule.mk.inj : ∀ {name : Aesop.RuleName} {entries : Array Lean.Meta.SimpEntry} {name_1 : Aesop.RuleName}
  {entries_1 : Array Lean.Meta.SimpEntry},
  { name := name, entries := entries } = { name := name_1, entries := entries_1 } → name = name_1 ∧ entries = entries_1
-- Mathlib.Topology.MetricSpace.TransferInstance
/-- Transfer a `MetricSpace` across an `Equiv`  -/
Equiv.metricSpace : {α : Type u_1} → {β : Type u_2} → [MetricSpace β] → α ≃ β → MetricSpace α
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.QuasiCompactCover.mk : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : CategoryTheory.PreZeroHypercover S},
  (∀ {U : S.Opens}, AlgebraicGeometry.IsAffineOpen U → IsCompactOpenCovered (fun x => ⇑(𝒰.f x)) ↑U) →
    AlgebraicGeometry.QuasiCompactCover 𝒰
-- Init.Data.String.Basic
String.Slice.Pos.le_ofSlice : ∀ {s : String.Slice} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {pos : (s.slice p₀ p₁ h).Pos}, p₀ ≤ String.Slice.Pos.ofSlice pos
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_eq_sInf : ∀ {a b : ENNReal}, a - b = sInf {d | a ≤ d + b}
-- Mathlib.Analysis.Complex.Basic
/-- The complex-conjugation function from `ℂ` to itself is a continuous `ℝ`-algebra isomorphism.  -/
Complex.conjCAE : ℂ ≃A[ℝ] ℂ
-- Init.Data.Slice.List.Lemmas
List.toList_mkSlice_rii : ∀ {α : Type u_1} {xs : List α}, Std.Slice.toList (Std.Rii.Sliceable.mkSlice xs *...*) = xs
-- Init.Data.Vector.Perm
Vector.Perm.mem_iff : ∀ {α : Type u_1} {n : ℕ} {a : α} {xs ys : Vector α n}, xs.Perm ys → (a ∈ xs ↔ a ∈ ys)
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.nthHomSeq_one : ∀ {R : Type u_1} [inst : NonAssocSemiring R] {p : ℕ} {f : (k : ℕ) → R →+* ZMod (p ^ k)} [hp_prime : Fact (Nat.Prime p)]
  (f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1),
  PadicInt.nthHomSeq f_compat 1 ≈ 1
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.mk.sizeOf_spec : ∀ {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} (toFun : UpperHalfPlane → ℂ)
  (slash_action_eq' : ∀ γ ∈ Γ, SlashAction.map k γ toFun = toFun),
  sizeOf { toFun := toFun, slash_action_eq' := slash_action_eq' } = 1
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.image_domRestrict`. -/
Set.image_restrict : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t : Set α), s.domRestrict f '' Subtype.val ⁻¹' t = f '' (t ∩ s)
-- Mathlib.Combinatorics.Enumerative.Composition
_private.Mathlib.Combinatorics.Enumerative.Composition.0.List.splitWrtCompositionAux.match_3.eq_2 : ∀ {α : Type u_1} (motive : List α → List ℕ → Sort u_2) (l : List α) (n : ℕ) (ns : List ℕ)
  (h_1 : (x : List α) → motive x []) (h_2 : (l : List α) → (n : ℕ) → (ns : List ℕ) → motive l (n :: ns)),
  (match l, n :: ns with
    | x, [] => h_1 x
    | l, n :: ns => h_2 l n ns) =
    h_2 l n ns
-- Mathlib.Algebra.Group.Units.Basic
add_eq_zero' : ∀ {α : Type u} [inst : AddCancelMonoid α] [Subsingleton (AddUnits α)] {a b : α}, a + b = 0 ↔ a = 0 ∧ b = 0
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.exists_gcd_eq_one_of_isOfFinAddOrder : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [hp : Fact (0 < p)]
  {u : AddCircle p},
  IsOfFinAddOrder u → ∃ m, m.gcd (addOrderOf u) = 1 ∧ m < addOrderOf u ∧ ↑(↑m / ↑(addOrderOf u) * p) = u
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_nonempty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α}, (s + t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter!_le_size : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF → ∀ {k : α} {f : Option β → Option β}, (Std.DTreeMap.Internal.Impl.Const.alter! k f t).size ≤ t.size + 1
-- Mathlib.RingTheory.Valuation.ValuationSubring
/-- The pullback of a valuation subring `A` along a ring homomorphism `K →+* L`.  -/
ValuationSubring.comap : {K : Type u} →
  [inst : Field K] → {L : Type u_1} → [inst_1 : Field L] → ValuationSubring L → (K →+* L) → ValuationSubring K
-- Mathlib.Data.Multiset.Sym
Multiset.mk_mem_sym2_iff : ∀ {α : Type u_1} {m : Multiset α} {a b : α}, s(a, b) ∈ m.sym2 ↔ a ∈ m ∧ b ∈ m
-- Batteries.Data.ByteSlice
/-- Inner loop of the `forIn` implementation for `ByteSlice`.  -/
_private.Batteries.Data.ByteSlice.0.ByteSlice.forIn.loop : {m : Type u_1 → Type u_2} →
  {β : Type u_1} → [Monad m] → (s : ByteSlice) → (UInt8 → β → m (ForInStep β)) → (i : ℕ) → i ≤ s.size → β → m β
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ringHom_ext'_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddMonoid M]
  {f g : AddMonoidAlgebra R M →+* S},
  f = g ↔
    f.comp AddMonoidAlgebra.singleZeroRingHom = g.comp AddMonoidAlgebra.singleZeroRingHom ∧
      (↑f).comp (AddMonoidAlgebra.of R M) = (↑g).comp (AddMonoidAlgebra.of R M)
-- Mathlib.RingTheory.Smooth.StandardSmoothOfFree
/-- If `S` is `R`-smooth at a prime `p`, then `S` is `R`-standard-smooth in a neighbourhood of `p`:
there exists a basic open `p ∈ D(f)` of `Spec S` such that `S[1/f]` is standard smooth.  -/
Algebra.IsSmoothAt.exists_notMem_isStandardSmooth : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] (p : Ideal S) [inst_4 : p.IsPrime] [Algebra.IsSmoothAt R p],
  ∃ f ∉ p, Algebra.IsStandardSmooth R (Localization.Away f)
-- Mathlib.Data.Set.Monotone
StrictMonoOn.mono : ∀ {α : Type u_1} {β : Type u_2} {s s₂ : Set α} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  StrictMonoOn f s → s₂ ⊆ s → StrictMonoOn f s₂
-- Mathlib.FieldTheory.Perfect
PerfectField.ofFinite : ∀ {K : Type u_1} [inst : Field K] [Finite K], PerfectField K
-- Mathlib.Order.LiminfLimsup
/-- **Alias** of `Filter.limsupReparam`.

---

Given an indexed family of sets `s j` and a function `f`, then `limsupReparam j` is equal
to `j` if `f` is bounded above on `s j`, and otherwise to some index `k` such that `f` is bounded
above on `s k` (if there exists one). To ensure good measurability behavior, this index `k` is
chosen as the minimal suitable index. This function is used to write down a limsup in a measurable
way, in `Filter.HasBasis.limsup_eq_ciInf_ciSup` and `Filter.HasBasis.limsup_eq_ite`.  -/
Filter.limsup_reparam : {α : Type u_1} →
  {ι : Type u_4} →
    {ι' : Type u_5} →
      [ConditionallyCompleteLinearOrder α] →
        (ι → α) →
          (ι' → Set ι) → (p : ι' → Prop) → [Countable (Subtype p)] → [Nonempty (Subtype p)] → Subtype p → Subtype p
-- Mathlib.Geometry.Euclidean.Circumcenter
Affine.Simplex.circumradius.eq_1 : ∀ {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 : ℕ} (s : Affine.Simplex ℝ P n), s.circumradius = s.circumsphere.radius
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.comp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.OplaxTrans X Y)
  (θ : CategoryTheory.Lax.OplaxTrans Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp η θ).app a = CategoryTheory.CategoryStruct.comp (η.app a) (θ.app a)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
ContDiff.exp : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {n : WithTop ℕ∞},
  ContDiff ℝ n f → ContDiff ℝ n fun x => Real.exp (f x)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey?_insertMany_list_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
      k ∈ List.map Sigma.fst l → (t.insertMany l).getKey? k' = some k
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_min!_eq_min : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {hc : t.min! ∈ t}, t.get t.min! hc = t.min ⋯
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistribEquiv.eq_1 : ∀ (R : Type u_7) (M : Type u_8) (N : Type u_9) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [inst_5 : Module.Finite R M]
  [inst_6 : Module.Finite R N] [inst_7 : Module.Free R M] [inst_8 : Module.Free R N],
  TensorProduct.dualDistribEquiv R M N =
    TensorProduct.dualDistribEquivOfBasis (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R N)
-- Std.Internal.Parsec.Basic
/-- Try `p`, then decide what to do based on success or failure without consuming input on failure.
 -/
Std.Internal.Parsec.tryCatch : {α ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] →
      [Std.Internal.Parsec.Input ι elem idx] →
        {β : Type} →
          Std.Internal.Parsec ι α →
            (α → Std.Internal.Parsec ι β) → (Unit → Std.Internal.Parsec ι β) → Std.Internal.Parsec ι β
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.id_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.LaxFunctor B C) (a : B),
  (CategoryTheory.CategoryStruct.id F).app a = CategoryTheory.CategoryStruct.id (F.obj a)
-- Mathlib.Order.Hom.CompleteLattice
sInfHom.symm_dual_comp : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : InfSet α] [inst_1 : InfSet β] [inst_2 : InfSet γ]
  (g : sSupHom βᵒᵈ γᵒᵈ) (f : sSupHom αᵒᵈ βᵒᵈ),
  sInfHom.dual.symm (g.comp f) = (sInfHom.dual.symm g).comp (sInfHom.dual.symm f)
-- Mathlib.SetTheory.Cardinal.Basic
/-- **Alias** of the reverse direction of `Cardinal.mk_le_one_iff_set_subsingleton`. -/
Set.Subsingleton.cardinalMk_le_one : ∀ {α : Type u} {s : Set α}, s.Subsingleton → Cardinal.mk ↑s ≤ 1
-- Init.Data.Vector.Basic
/-- Returns `true` if `p` returns `true` for any element of the vector.  -/
Vector.any : {α : Type u_1} → {n : ℕ} → Vector α n → (α → Bool) → Bool
-- Mathlib.Analysis.Convex.Topology
/-- Convex hull of a finite set is closed.  -/
Set.Finite.isClosed_convexHull : ∀ {E : Type u_3} (𝕜 : Type u_4) [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [inst_7 : AddCommGroup E]
  [inst_8 : Module 𝕜 E] [inst_9 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E]
  {s : Set E}, s.Finite → IsClosed ((convexHull 𝕜) s)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
mem_nonZeroDivisors_iff_ne_zero : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} [NoZeroDivisors M₀] [Nontrivial M₀],
  x ∈ nonZeroDivisors M₀ ↔ x ≠ 0
-- Mathlib.Data.List.Lookmap
List.lookmap_cons_none : ∀ {α : Type u_1} (f : α → Option α) {a : α} (l : List α), f a = none → List.lookmap f (a :: l) = a :: List.lookmap f l
-- Mathlib.Order.RelSeries
SetRel.finiteDimensional_or_infiniteDimensional : ∀ {α : Type u_1} (r : SetRel α α) [Nonempty α], r.FiniteDimensional ∨ r.InfiniteDimensional
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.le_sqrt_log : ∀ {N : ℕ}, 4096 ≤ N → Real.log (2 / (1 - 2 / Real.exp 1)) * (69 / 50) ≤ √(Real.log ↑N)
-- Mathlib.CategoryTheory.Sites.Sieves
/-- The sieve generated by the morphisms in `R.category`
for a presieve `R` is the sieve generated by `R`.  -/
CategoryTheory.Sieve.ofArrows_category' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {S : C} (R : CategoryTheory.Presieve S),
  (CategoryTheory.Sieve.ofArrows (fun f => f.obj.left) fun f => f.obj.hom) = CategoryTheory.Sieve.generate R
-- Mathlib.Order.Partition.Finpartition
Finpartition.mem_toSubtype_iff : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : α} (P : Finpartition s) {Pr : α → Prop}
  (Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)) (Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)) (Prbot : Pr ⊥)
  (hs : Pr s) (hP : ∀ p ∈ P.parts, Pr p) (p : Subtype Pr),
  p ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts ↔ ↑p ∈ P.parts
-- Init.Data.Range.Polymorphic.UInt
USize.instUpwardEnumerable : Std.PRange.UpwardEnumerable USize
-- Init.Data.Range.Polymorphic.Map
Std.PRange.UpwardEnumerable.LT.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (a b : α),
  Std.PRange.UpwardEnumerable.LT a b = ∃ n, Std.PRange.succMany? (n + 1) a = some b
-- Mathlib.Data.ENNReal.BigOperators
/-- Seeing `ℝ≥0∞` as `ℝ≥0` does not change their sum, unless one of the `ℝ≥0∞` is
infinity  -/
ENNReal.toNNReal_sum : ∀ {α : Type u_1} {s : Finset α} {f : α → ENNReal},
  (∀ a ∈ s, f a ≠ ⊤) → (∑ a ∈ s, f a).toNNReal = ∑ a ∈ s, (f a).toNNReal
-- Mathlib.AlgebraicGeometry.Morphisms.Smooth
/-- A morphism of schemes is smooth if and only if for each `x : X` there exists an affine open
neighborhood `V` of `x` and an affine open neighborhood `U` of `f.base x` with `V ≤ f ⁻¹ᵁ U`
such that the induced map `Γ(Y, U) ⟶ Γ(X, V)` is standard smooth.
 -/
AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.Smooth f ↔
    ∀ (x : ↥X),
      ∃ U,
        ∃ (_ : AlgebraicGeometry.IsAffineOpen U),
          ∃ V,
            ∃ (_ : AlgebraicGeometry.IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
              (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).IsStandardSmooth
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
ContMDiffMap.coe_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {H : Type u_4}
  [inst_5 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {N : Type u_6} [inst_7 : TopologicalSpace N] [inst_8 : ChartedSpace H N]
  {n : WithTop ℕ∞} {G : Type u_10} [inst_9 : Group G] [inst_10 : TopologicalSpace G] [inst_11 : ChartedSpace H' G]
  [inst_12 : LieGroup I' n G] (f : ContMDiffMap I I' N G n), ⇑f⁻¹ = (⇑f)⁻¹
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.sign_excenterWeights_empty : ∀ {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) (i : Fin (n + 1)),
  SignType.sign (s.excenterWeights ∅ i) = 1
-- Mathlib.RingTheory.RingHom.StandardSmooth
RingHom.IsStandardSmoothOfRelativeDimension.comp : ∀ {n m : ℕ} {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] {T : Type u_1} [inst_2 : CommRing T]
  {g : S →+* T} {f : R →+* S},
  RingHom.IsStandardSmoothOfRelativeDimension n g →
    RingHom.IsStandardSmoothOfRelativeDimension m f → RingHom.IsStandardSmoothOfRelativeDimension (n + m) (g.comp f)
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
Lex.instSMulWithZero' : {G₀ : Type u_1} →
  {M₀ : Type u_2} → [inst : Zero G₀] → [inst_1 : Zero M₀] → [SMulWithZero G₀ M₀] → SMulWithZero G₀ (Lex M₀)
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.lt_natCast_add_one_iff : ∀ {n : ℕ} {c : Cardinal.{u_1}}, c < ↑n + 1 ↔ c ≤ ↑n
-- Mathlib.GroupTheory.Commutator.Basic
addCommutator_eq_normalClosure : ∀ (G : Type u_1) [inst : AddGroup G], addCommutator G = AddSubgroup.normalClosure (addCommutatorSet G)
-- Lean.Meta.Sym.Arith.Types
/-- Set the exponent threshold.  -/
Lean.Meta.Sym.Arith.setExpThreshold : ℕ → Lean.Meta.Sym.SymM Unit
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
/-- Monomorphisms are separated.  -/
AlgebraicGeometry.IsSeparated.isSeparated_of_mono : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.Mono f], AlgebraicGeometry.IsSeparated f
-- Mathlib.Algebra.Category.CommAlgCat.Basic
instHasLimitsCommAlgCat : ∀ {R : Type u} [inst : CommRing R], CategoryTheory.Limits.HasLimits (CommAlgCat R)
-- Mathlib.Algebra.Group.Action.Defs
add_vadd_add_comm : ∀ {α : Type u_5} {β : Type u_6} [inst : Add α] [inst_1 : Add β] [inst_2 : VAdd α β] [VAddAssocClass α β β]
  [VAddAssocClass α α β] [VAddCommClass α β β] (a b : α) (c d : β), (a + b) +ᵥ c + d = (a +ᵥ c) + (b +ᵥ d)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- A monotone function on `ω`-continuous partial orders is said to be continuous
if for every chain `c : chain α`, `f (⊔ i, c i) = ⊔ i, f (c i)`.
This is just the bundled version of `OrderHom.continuous`.  -/
OmegaCompletePartialOrder.«term_→𝒄_» : Lean.TrailingParserDescr
-- Mathlib.Data.Set.Finite.Lattice
/-- If the image of `s` under `f` is finite, and each fiber of `f` has a finite intersection
with `s`, then `s` is itself finite.

It is useful to give `f` explicitly here so this can be used with `apply`.
 -/
Set.Finite.of_finite_fibers : ∀ {α : Type u} {β : Type v} (f : α → β) {s : Set α}, (f '' s).Finite → (∀ x ∈ f '' s, (s ∩ f ⁻¹' {x}).Finite) → s.Finite
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- For any `K`-basis of `L`, we have `B.norm 0 = 0`.  -/
Module.Basis.norm_zero : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] (B : Module.Basis ι K L), B.norm 0 = 0
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement'_bot_left : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G}, ⊥.IsComplement' H ↔ H = ⊤
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instInvolutiveInv : {α : Type u_1} → [InvolutiveInv α] → InvolutiveInv (Lex α)
-- Mathlib.RingTheory.QuasiFinite.Polynomial
Polynomial.map_under_lt_comap_of_quasiFiniteAt : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (f : Polynomial R →ₐ[R] S) (P : Ideal S) [inst_3 : P.IsPrime] [Algebra.QuasiFiniteAt R P],
  Ideal.map Polynomial.C (Ideal.under R P) < Ideal.comap (↑f) P
-- Mathlib.MeasureTheory.Measure.Regular
/-- Let `μ` be a locally finite measure on an R₁ topological space with Borel σ-algebra.
If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated in measure by an open set.
See also `Set.exists_isOpen_lt_of_lt` and `MeasurableSet.exists_isOpen_diff_lt`
for the case of an outer regular measure.  -/
MeasurableSet.exists_isOpen_symmDiff_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] [MeasureTheory.IsLocallyFiniteMeasure μ] [R1Space α] [BorelSpace α] {s : Set α},
  MeasurableSet s → μ s ≠ ⊤ → ∀ {ε : ENNReal}, ε ≠ 0 → ∃ U, IsOpen U ∧ μ U < ⊤ ∧ μ (symmDiff U s) < ε