mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtPlace_smul : ∀ {K : Type u_1} [inst : Field K] (w : NumberField.InfinitePlace K) (x : NumberField.mixedEmbedding.mixedSpace K)
  (c : ℝ), (NumberField.mixedEmbedding.normAtPlace w) (c • x) = |c| * (NumberField.mixedEmbedding.normAtPlace w) x
-- Mathlib.Data.List.Cycle
List.prev_reverse_eq_next : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → ∀ (x : α) (hx : x ∈ l), l.reverse.prev x ⋯ = l.next x hx
-- Mathlib.Algebra.GCDMonoid.Basic
/-- Represent a divisor of `m * n` as a product of a divisor of `m` and a divisor of `n`.

Note: In general, this representation is highly non-unique.

See `Nat.dvdProdDvdOfDvdProd` for a constructive version on `ℕ`.  -/
instDecompositionMonoidOfIsGCDMonoid : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [h : IsGCDMonoid α], DecompositionMonoid α
-- Init.Conv
/-- Executes the given tactic block without converting `conv` goal into a regular goal.  -/
Lean.Parser.Tactic.Conv.nestedTacticCore : Lean.ParserDescr
-- Std.Async.TCP
/-- Gets the local address of the client socket.
 -/
Std.Async.TCP.Socket.Client.getSockName : Std.Async.TCP.Socket.Client → IO Std.Net.SocketAddress
-- Mathlib.Analysis.Complex.Exponential
Complex.norm_exp_sub_sum_le_exp_norm_sub_sum : ∀ (x : ℂ) (n : ℕ),
  ‖Complex.exp x - ∑ m ∈ Finset.range n, x ^ m / ↑m.factorial‖ ≤
    Real.exp ‖x‖ - ∑ m ∈ Finset.range n, ‖x‖ ^ m / ↑m.factorial
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_setWidth : ∀ {n m : ℕ} {x : BitVec n} {i : ℕ}, (BitVec.setWidth m x).getMsbD i = (decide (m - n ≤ i) && x.getMsbD (i + n - m))
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk_symm : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B},
  b ∈ e.baseSet → ∀ (y : F), ⟨b, e.symm b y⟩ = ↑e.symm (b, y)
-- Mathlib.Order.Category.CompleteLat
CompleteLat.dualEquiv_inverse : CompleteLat.dualEquiv.inverse = CompleteLat.dual
-- Init.Coe
/-- Coerces a value `f : α` to type `γ f`, which should be either be a
function type or another `CoeFun` type, in order to resolve a mistyped
application `f x`.  -/
CoeFun.coe : {α : Sort u} → {γ : outParam (α → Sort v)} → [self : CoeFun α γ] → (f : α) → γ f
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.ne_iff : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p q : FormalMultilinearSeries 𝕜 E F}, p ≠ q ↔ ∃ n, p n ≠ q n
-- Mathlib.GroupTheory.Perm.Option
Equiv.Perm.decomposeOption_symm_sign : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (e : Equiv.Perm α),
  Equiv.Perm.sign (Equiv.Perm.decomposeOption.symm (none, e)) = Equiv.Perm.sign e
-- Mathlib.RingTheory.RootsOfUnity.AlgebraicallyClosed
/-- A separably closed field `F` satisfies `HasEnoughRootsOfUnity F n` for all `n`
that are not divisible by the characteristic of `F`.  -/
IsSepClosed.hasEnoughRootsOfUnity : ∀ (F : Type u_1) [inst : Field F] (n : ℕ) [NeZero ↑n] [IsSepClosed F], HasEnoughRootsOfUnity F n
-- Mathlib.Tactic.Push
/-- A simproc variant of `push fun _ ↦ _`, to be used as `simp [↓pushFun]`.  -/
pushFun : Lean.Meta.Simp.Simproc
-- Mathlib.Topology.Bases
separableSpace_univ : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.SeparableSpace α],
  TopologicalSpace.SeparableSpace ↑Set.univ
-- Init.Prelude
OrElse.mk : {α : Type u} → (α → (Unit → α) → α) → OrElse α
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.instIsModHomComp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D]
  (A : C) [inst_4 : CategoryTheory.MonObj A] {M N O : D} [inst_5 : CategoryTheory.ModObj A M]
  [inst_6 : CategoryTheory.ModObj A N] [inst_7 : CategoryTheory.ModObj A O] (f : M ⟶ N) (g : N ⟶ O)
  [CategoryTheory.IsModHom A f] [CategoryTheory.IsModHom A g],
  CategoryTheory.IsModHom A (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.MeasureTheory.Function.LpSpace.Indicator
MeasureTheory.norm_indicatorConstLp_le : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {s : Set α} {hs : MeasurableSet s} {hμs : μ s ≠ ⊤} {c : E},
  ‖MeasureTheory.indicatorConstLp p hs hμs c‖ ≤ ‖c‖ * μ.real s ^ (1 / p.toReal)
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
SimpleGraph.Finsubgraph.instCompl : {V : Type u} → {G : SimpleGraph V} → [Finite V] → Compl G.Finsubgraph
-- Mathlib.Algebra.Module.StablyFree.Basic
Module.IsStablyFree.exist_free_prod : ∀ (R : Type u) [inst : Ring R] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.IsStablyFree R M],
  ∃ N x x_1, ∃ (_ : Module.Finite R N) (_ : Module.Free R N), Module.Free R (M × N)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.restriction.eq_1 : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R),
  p.restriction = ∑ i ∈ p.support, (Polynomial.monomial i) ⟨p.coeff i, ⋯⟩
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.HasAntitoneBasis.eventually_subset : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] {l : Filter α} {s : ι → Set α},
  l.HasAntitoneBasis s → ∀ {t : Set α}, t ∈ l → ∀ᶠ (i : ι) in Filter.atTop, s i ⊆ t
-- Mathlib.Order.Concept
Concept.isIntent_intent : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} (c : Concept α β r), Order.IsIntent r c.intent
-- Mathlib.Data.FunLike.Fintype
/-- All `FunLike`s are finite if their domain and codomain are.

Non-dependent version of `DFunLike.finite` that might be easier to infer.
Can't be an instance because it can cause infinite loops.
 -/
FunLike.finite : ∀ (G : Sort u_2) {α : Sort u_3} {γ : Sort u_4} [FunLike G α γ] [Finite α] [Finite γ], Finite G
-- Mathlib.Data.Setoid.Basic
/-- The supremum of two equivalence relations r and s is the equivalence closure of the binary
relation `x is related to y by r or s`.  -/
Setoid.sup_eq_eqvGen : ∀ {α : Type u_1} (r s : Setoid α), r ⊔ s = Relation.EqvGen.setoid fun x y => r x y ∨ s x y
-- Mathlib.Logic.Equiv.Defs
Equiv.bijective : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), Function.Bijective ⇑e
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.instFullObjCompPostOfFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : C) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) [G.Faithful], (CategoryTheory.StructuredArrow.post S F G).Full
-- Std.Data.HashSet.Raw
/-- Returns `true` if the hash set contains no elements.

Note that if your `BEq` instance is not reflexive or your `Hashable` instance is not
lawful, then it is possible that this function returns `false` even though `m.contains a = false`
for all `a`.
 -/
Std.HashSet.Raw.isEmpty : {α : Type u} → Std.HashSet.Raw α → Bool
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- This typeclass ensures that an `UpwardEnumerable α` instance is compatible with `≤`.
In this case, `UpwardEnumerable α` fully characterizes the `LE α` instance.
 -/
Std.PRange.LawfulUpwardEnumerableLE : (α : Type u) → [Std.PRange.UpwardEnumerable α] → [LE α] → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  (List.map Sigma.fst toInsert).contains k = false →
    Std.Internal.List.getKey? k (Std.Internal.List.insertList l toInsert) = Std.Internal.List.getKey? k l
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.charFunDual_map_sum_pi_eq_prod : ∀ {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E]
  [SecondCountableTopology E] [inst_4 : Fintype ι] [inst_5 : NormedSpace ℝ E] {μ : ι → MeasureTheory.Measure E}
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)],
  MeasureTheory.charFunDual (MeasureTheory.Measure.map (fun p => ∑ i, p i) (MeasureTheory.Measure.pi μ)) =
    ∏ i, MeasureTheory.charFunDual (μ i)
-- Mathlib.RingTheory.FiniteType
/-- If a monoid `M` is finitely generated then `R[M]` is of finite type.  -/
MonoidAlgebra.finiteType_of_fg : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid M] [inst_1 : CommRing R] [Monoid.FG M],
  Algebra.FiniteType R (MonoidAlgebra R M)
-- Lean.Meta.Tactic.Grind.CheckResult
/-- Closed the goal.  -/
Lean.Meta.Grind.CheckResult.closed : Lean.Meta.Grind.CheckResult
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthInf_le_of_eventually_le : ∀ {u v : ℕ → ENNReal} {b : ENNReal},
  b ≠ ⊤ → (∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ b * v n) → ExpGrowth.expGrowthInf u ≤ ExpGrowth.expGrowthInf v
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toList_eq_toList_roo : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : LT α] [inst_3 : DecidableLT α]
  [inst_4 : Std.PRange.UpwardEnumerable α] [inst_5 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLE α] [Std.PRange.LawfulUpwardEnumerableLT α] [inst_8 : Std.Rxc.IsAlwaysFinite α]
  [inst_9 : Std.Rxo.IsAlwaysFinite α] [inst_10 : Std.PRange.InfinitelyUpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α], r.toList = (r.lower<...Std.PRange.succ r.upper).toList
-- Mathlib.NumberTheory.Padics.RingHoms
PadicInt.zmodRepr_unique : ∀ {p : ℕ} [hp_prime : Fact (Nat.Prime p)] (x : ℤ_[p]), ∀ y < p, x - ↑y ∈ IsLocalRing.maximalIdeal ℤ_[p] → x.zmodRepr = y
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcCallParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams) (sessionId : UInt64) (method : Lean.Name)
  (params : Lean.Json),
  sizeOf
      { toTextDocumentPositionParams := toTextDocumentPositionParams, sessionId := sessionId, method := method,
        params := params } =
    1 + sizeOf toTextDocumentPositionParams + sizeOf sessionId + sizeOf method + sizeOf params
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A right homology data for a short complex `S` in the opposite category
induces a left homology data for `S.unop`.  -/
CategoryTheory.ShortComplex.RightHomologyData.unop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex Cᵒᵖ} → S.RightHomologyData → S.unop.LeftHomologyData
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.lift_unique : ∀ {N : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group N] [inst_1 : Group G] [inst_2 : Group H]
  {φ : G →* MulAut N} (F : N ⋊[φ] G →* H),
  F = SemidirectProduct.lift (F.comp SemidirectProduct.inl) (F.comp SemidirectProduct.inr) ⋯
-- Mathlib.LinearAlgebra.Ray
rayOfNeZero.congr_simp : ∀ (R : Type u_1) [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (v v_1 : M) (e_v : v = v_1) (h : v ≠ 0),
  rayOfNeZero R v h = rayOfNeZero R v_1 ⋯
-- Mathlib.NumberTheory.Dioph
/-- The set of places where one Diophantine function is less than another is Diophantine.  -/
Dioph.«term_D<_» : Lean.TrailingParserDescr
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rxi.Iterator.nodup_toList : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α]
  {it : Std.Iter α}, it.toList.Nodup
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_of_measurable_on_compl_finite : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {mβ : MeasurableSpace β} [MeasurableSingletonClass α]
  {f : α → β} (s : Set α), s.Finite → Measurable (sᶜ.domRestrict f) → Measurable f
-- Mathlib.Order.BoundedOrder.Basic
/-- A top element can be replaced with `⊤`.

Prefer `IsTop.eq_top` if `α` already has a top element.  -/
IsTop.rec : {α : Type u} →
  [inst : LE α] →
    {motive : (x : α) → IsTop x → Sort u_1} →
      ([inst_1 : OrderTop α] → motive ⊤ ⋯) → (x : α) → (hx : IsTop x) → motive x hx
-- Mathlib.Data.Nat.Find
Nat.find_eq_zero : ∀ {p : ℕ → Prop} [inst : DecidablePred p] (h : ∃ n, p n), Nat.find h = 0 ↔ p 0
-- Mathlib.RingTheory.Trace.Basic
Module.Basis.traceDual_involutive : ∀ (K : Type u_4) (L : Type u_5) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {ι : Type w}
  [inst_3 : FiniteDimensional K L] [inst_4 : Algebra.IsSeparable K L] [inst_5 : Finite ι] [inst_6 : DecidableEq ι],
  Function.Involutive Module.Basis.traceDual
-- Mathlib.Order.Max
/-- **Alias** of `not_isMin_of_lt`. -/
LT.lt.not_isMin : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, b < a → ¬IsMin a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_sub : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddGroup α] [inst_1 : SubtractionMonoid β]
  [inst_2 : FunLike F α β] [AddMonoidHomClass F α β] (m : F),
  Function.Injective ⇑m → ∀ {s t : Set β}, s ⊆ Set.range ⇑m → t ⊆ Set.range ⇑m → ⇑m ⁻¹' (s - t) = ⇑m ⁻¹' s - ⇑m ⁻¹' t
-- Batteries.Data.List.Basic
List.takeList_eq_takeListTR : @List.takeList = @List.takeListTR
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
add_le_add_right : ∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddLeftMono α] {b c : α}, b ≤ c → ∀ (a : α), a + b ≤ a + c
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toHomeomorph_symm : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.symm.toHomeomorph = e.toHomeomorph.symm
-- Mathlib.Topology.Order.Bornology
orderBornology_isBounded : ∀ {α : Type u_1} {s : Set α} [inst : Lattice α] [inst_1 : Nonempty α], Bornology.IsBounded s ↔ BddBelow s ∧ BddAbove s
-- Mathlib.Analysis.Complex.ReImTopology
Complex.closure_preimage_im : ∀ (s : Set ℝ), closure (Complex.im ⁻¹' s) = Complex.im ⁻¹' closure s
-- Mathlib.LinearAlgebra.Matrix.ToLin
/-- A basis of a module induces an equivalence of algebras from the endomorphisms of the module to
square matrices.  -/
algEquivMatrix : {R : Type u_1} →
  [inst : CommSemiring R] →
    {n : Type u_3} →
      [inst_1 : DecidableEq n] →
        {M : Type u_4} →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] → [inst_4 : Fintype n] → Module.Basis n R M → Module.End R M ≃ₐ[R] Matrix n n R
-- Std.Do.Internal.Ensures.Def
/-- A `P`-tagged refinement of `x` exists.  -/
Std.Do.Internal.Ensures.exists_refinement : ∀ {m : Type u → Type v} [inst : Bind m] {α : Type u} {P : α → Prop} {x : m α},
  Std.Do.Internal.Ensures P x → ∃ y, Std.Do.Internal.ErasesTo y x
-- Mathlib.CategoryTheory.Sites.Precoverage.Generates
CategoryTheory.Coverage.generates_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.Coverage C}, K.Generates J ↔ K.toGrothendieck = J
-- Mathlib.Control.Functor
_private.Mathlib.Control.Functor.0.Functor.Comp.map.match_1.eq_1 : ∀ {F : Type u_1 → Type u_3} {G : Type u_2 → Type u_1} {α : Type u_2} (motive : Functor.Comp F G α → Sort u_4)
  (x : F (G α)) (h_1 : (x : F (G α)) → motive x),
  (match x with
    | x => h_1 x) =
    h_1 x
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.IdealSheafData.ideal_map : ∀ {X Y : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f]
  (U : ↑Y.affineOpens) (H : AlgebraicGeometry.IsAffineOpen ((TopologicalSpace.Opens.map f.base).obj ↑U)),
  (I.map f).ideal U =
    Ideal.comap (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f ↑U))
      (I.ideal ⟨(TopologicalSpace.Opens.map f.base).obj ↑U, H⟩)
-- Batteries.Data.Float.Lemmas
Float.ofBits_toBits : ∀ (f : Float), Float.ofBits f.toBits = f
-- Mathlib.Data.Multiset.Filter
Multiset.map_filterMap : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (f : α → Option β) (g : β → γ) (s : Multiset α),
  Multiset.map g (Multiset.filterMap f s) = Multiset.filterMap (fun x => Option.map g (f x)) s
-- Lean.Data.Lsp.Basic
/-- More detailed associated progress message.  -/
Lean.Lsp.WorkDoneProgressReport.message? : Lean.Lsp.WorkDoneProgressReport → Option String
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.srange_subtype : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] (s : NonUnitalSubsemiring R),
  NonUnitalRingHom.srange (NonUnitalSubsemiringClass.subtype s) = s
-- Mathlib.Data.List.Rotate
List.isRotated_singleton_iff : ∀ {α : Type u} {l : List α} {x : α}, l ~r [x] ↔ l = [x]
-- Mathlib.GroupTheory.OrderOfElement
isOfFinOrder_iff_isUnit : ∀ {G : Type u_1} [inst : Monoid G] [Finite Gˣ] {x : G}, IsOfFinOrder x ↔ IsUnit x
-- Mathlib.Order.Filter.Subsingleton
Filter.Subsingleton.prod : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α},
  l.Subsingleton → ∀ {l' : Filter β}, l'.Subsingleton → (l ×ˢ l').Subsingleton
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_union_inter : ∀ {α : Type u_1} (s t : Set α), s \ t ∪ s ∩ t = s
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.inf_of_right : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l l' : Filter α},
  MeasureTheory.IntegrableAtFilter f l μ → MeasureTheory.IntegrableAtFilter f (l' ⊓ l) μ
-- Mathlib.MeasureTheory.SetSemiring
_private.Mathlib.MeasureTheory.SetSemiring.0.MeasureTheory.IsSetSemiring.exists_finpartition_sdiff_sUnion : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} {I : Finset (Set α)},
  MeasureTheory.IsSetSemiring C → s ∈ C → ↑I ⊆ C → ∃ P, ↑P.parts ⊆ C
-- Mathlib.Topology.Sequences
/-- The range of sequentially continuous function on a sequentially compact space is sequentially
compact.  -/
IsSeqCompact.range : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y}
  [SeqCompactSpace X], SeqContinuous f → IsSeqCompact (Set.range f)
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projectionOnto_apply_of_mem_right`.

---

**Alias** of the reverse direction of `Submodule.projectionOnto_apply_eq_zero_iff`. -/
Submodule.linearProjOfIsCompl_apply_right' : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (h : IsCompl p q) {x : E}, x ∈ q → (p.projectionOnto q h) x = 0
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- A version of `Matroid.dual_eRk_add_eRank` for non-subsets of the ground set.  -/
Matroid.eRk_dual_add_eRank' : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), M✶.eRk X + M.eRank = M.eRk (M.E \ X) + (X ∩ M.E).encard
-- Mathlib.Logic.Equiv.Basic
/-- To give an equivalence between two subsingleton types, it is sufficient to give any two
functions between them.  -/
equivOfSubsingletonOfSubsingleton : {α : Sort u_1} → {β : Sort u_4} → [Subsingleton α] → [Subsingleton β] → (α → β) → (β → α) → α ≃ β
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is a weakly regular measure, then any open set can be approximated by a closed subset.  -/
IsOpen.measure_eq_iSup_isClosed : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] ⦃U : Set α⦄,
  IsOpen U → ∀ (μ : MeasureTheory.Measure α) [μ.WeaklyRegular], μ U = ⨆ F, ⨆ (_ : F ⊆ U), ⨆ (_ : IsClosed F), μ F
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.one_le_logSizeRadius : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {V : Finset T} {t : T},
  1 < a → 1 ≤ PairReduction.logSizeRadius t V a c
-- Mathlib.Data.List.Lemmas
_private.Mathlib.Data.List.Lemmas.0.List.mapAccumr.match_1.eq_1 : ∀ {α : Type u_1} {γ : Type u_3} (motive : List α → γ → Sort u_2) (c : γ) (h_1 : (c : γ) → motive [] c)
  (h_2 : (y : α) → (yr : List α) → (c : γ) → motive (y :: yr) c),
  (match [], c with
    | [], c => h_1 c
    | y :: yr, c => h_2 y yr c) =
    h_1 c
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.instInhabited : Inhabited AddMonCat
-- Mathlib.Data.Fin.Tuple.Basic
/-- Sends `(g₀, ..., gₙ)` to `(g₀, ..., op gⱼ gⱼ₊₁, ..., gₙ)`.  -/
Fin.contractNth : {n : ℕ} → {α : Sort u_1} → Fin (n + 1) → (α → α → α) → (Fin (n + 1) → α) → Fin n → α
-- Mathlib.Data.Finset.Pi
/-- **Alias** of `Finset.domRestrict_preimage`. -/
Finset.restrict_preimage : ∀ {ι : Type u_2} {π : ι → Type u_3} [inst : DecidableEq ι] {I : Set ι} [inst_1 : DecidablePred fun x => x ∈ I]
  (s : Finset ↑I) (u : (i : ↑I) → Set (π ↑i)),
  I.domRestrict ⁻¹' (↑s).pi u = (↑(Finset.image Subtype.val s)).pi fun i => if h : i ∈ I then u ⟨i, h⟩ else Set.univ
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_pos_iff_nonempty_of_vaddInvariant : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] [inst_3 : TopologicalSpace α]
  [ContinuousConstVAdd G α] [AddAction.IsMinimal G α] {U : Set α} [μ.Regular], μ ≠ 0 → IsOpen U → (0 < μ U ↔ U.Nonempty)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.monoCLM_eq_of_scalars : ∀ (𝕜 : 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] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n₁ n₂ : ℕ∞} {K₁ K₂ : TopologicalSpace.Compacts E} (𝕜' : Type u_5)
  [inst_7 : NontriviallyNormedField 𝕜'] [inst_8 : NormedSpace 𝕜' F] [inst_9 : SMulCommClass ℝ 𝕜' F],
  ⇑(ContDiffMapSupportedIn.monoCLM 𝕜) = ⇑(ContDiffMapSupportedIn.monoCLM 𝕜')
-- Mathlib.Analysis.Complex.Circle
Circle.exp_sub : ∀ (x y : ℝ), Circle.exp (x - y) = Circle.exp x / Circle.exp y
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_insert_algebraMap : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : R) (s : Set A),
  Algebra.adjoin R (insert ((algebraMap R A) x) s) = Algebra.adjoin R s
-- Mathlib.Data.Set.Piecewise
Set.univ_pi_piecewise_univ : ∀ {ι : Type u_8} {α : ι → Type u_9} (s : Set ι) (t : (i : ι) → Set (α i)) [inst : (x : ι) → Decidable (x ∈ s)],
  Set.univ.pi (s.piecewise t fun x => Set.univ) = s.pi t
-- Mathlib.ModelTheory.Basic
/-- `HomClass L F M N` states that `F` is a type of `L`-homomorphisms. You should extend this
typeclass when you extend `FirstOrder.Language.Hom`.  -/
FirstOrder.Language.HomClass : (L : outParam FirstOrder.Language) →
  (F : Type u_3) →
    (M : outParam (Type u_4)) → (N : outParam (Type u_5)) → [FunLike F M N] → [L.Structure M] → [L.Structure N] → Prop
-- Mathlib.Topology.Semicontinuity.Basic
UpperSemicontinuousAt.inf : ∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {a : α},
  UpperSemicontinuousAt f a → UpperSemicontinuousAt g a → UpperSemicontinuousAt (fun x => min (f x) (g x)) a
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.inf_limZero : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {f g : CauSeq α abs},
  f.LimZero → g.LimZero → (f ⊓ g).LimZero
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_ofList_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : Std.LawfulEqCmp cmp]
  {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = Ordering.eq) {v : β k} [inst_1 : Inhabited (β k')],
  List.Pairwise (fun a b => ¬cmp a.fst b.fst = Ordering.eq) l →
    ⟨k, v⟩ ∈ l → (Std.DTreeMap.ofList l cmp).get! k' = cast ⋯ v
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsTuranMaximal.card_parts_le : ∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ} (h : G.IsTuranMaximal r)
  [inst_2 : DecidableEq V], h.finpartition.parts.card ≤ r