mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Constructions.UnitInterval
unitInterval.volume_Iio : ∀ (x : ↑unitInterval), MeasureTheory.volume (Set.Iio x) = ENNReal.ofReal ↑x
-- Mathlib.Computability.Primrec.List
_private.Mathlib.Computability.Primrec.List.0.list_cons' : ∀ {β : Type u_2} [inst : Primcodable β] (H : Nat.Primrec fun n => Encodable.encode (Encodable.decode n)),
  Primrec₂ List.cons
-- Lean.Parser.Command
/-- Documents a recommended spelling for a notation in identifiers.

Theorems should generally be systematically named after their statement, rather than creatively.
Non-identifier notations should be referred to consistently by their recommended spelling.

```
/-- some additional info -/
recommended_spelling "and" for "∧" in [And, «term_∧_»]
```

will do the following:
* Adds the sentence "The recommended spelling of `∧` in identifiers is `and` (some additional info)."
  to the end of the docstring for `And` and for `∧`. If the additional info is more than a single
  line, it will be placed below the sentence instead of in parentheses.
* Registers this information in an environment extension, so that it will later be possible to
  generate a table with all recommended spellings.

You can add attach the recommended spelling to as many declarations as you want. It is recommended
to attach the recommended spelling to all relevant parsers as well as the declaration the parsers
refer to (if such a declaration exists). Note that the `inherit_doc` attribute does *not* copy
recommended spellings, so even though the parser for `∧` uses `@[inherit_doc And]`, we have to
attach the recommended spelling to both `And` and `«term_∧_»`.

The `syntax`, `macro`, `elab` and `notation` commands accept a `(name := parserName)` option to
assign a name to the created parser so that you do not have to guess the automatically generated
name. The `syntax`, `macro` and `elab` commands can be hovered to see the name of the parser.

For complex notations which enclose identifiers, the convention is to use example identifiers rather
than other placeholders. This is an example following the convention:
```
recommended_spelling "singleton" for "[a]" in [List.cons, «term[_]»]
```
Using `[·]` or `[⋯]` or `[…]` instead of `[a]` would be against the convention. When attaching a
recommended spelling to a notation whose docstring already has an example, try to reuse the
identifier names chosen in the docstring for consistency.
 -/
Lean.Parser.Command.recommended_spelling : Lean.Parser.Parser
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_lt_arg_add_two_pi : ∀ (x y : ℂ), x.arg < y.arg + 2 * Real.pi
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurryMid_curryMid : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (p : Fin (n + 1)) (f : ContinuousMultilinearMap 𝕜 Ei G),
  ContinuousLinearMap.uncurryMid p (ContinuousMultilinearMap.curryMid p f) = f
-- Mathlib.Logic.Equiv.Set
Equiv.prod_assoc_image : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ},
  ⇑(Equiv.prodAssoc α β γ) '' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.mk.inj : ∀ {R : Type u_1} {S : Type u_2} {inst : Semiring R} {inst_1 : Semiring S} {σ : R →+* S} {M : Type u_3}
  {inst_2 : TopologicalSpace M} {inst_3 : AddCommMonoid M} {M₂ : Type u_4} {inst_4 : TopologicalSpace M₂}
  {inst_5 : AddCommMonoid M₂} {inst_6 : Module R M} {inst_7 : Module S M₂} {toLinearMap : M →ₛₗ[σ] M₂}
  {cont : autoParam (Continuous toLinearMap.toFun) ContinuousLinearMap.cont._autoParam} {toLinearMap_1 : M →ₛₗ[σ] M₂}
  {cont_1 : autoParam (Continuous toLinearMap_1.toFun) ContinuousLinearMap.cont._autoParam},
  { toLinearMap := toLinearMap, cont := cont } = { toLinearMap := toLinearMap_1, cont := cont_1 } →
    toLinearMap = toLinearMap_1
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.Hom.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  [inst_1 : SizeOf C] (h : d.mid ⟶ e.mid)
  (ι_h : autoParam (CategoryTheory.CategoryStruct.comp d.ι h = e.ι) CategoryTheory.Factorisation.Hom.ι_h._autoParam)
  (h_π : autoParam (CategoryTheory.CategoryStruct.comp h e.π = d.π) CategoryTheory.Factorisation.Hom.h_π._autoParam),
  sizeOf { h := h, ι_h := ι_h, h_π := h_π } = 1 + sizeOf h + sizeOf ι_h + sizeOf h_π
-- Lean.Data.Options
Lean.getNatOption : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → Lean.Name → optParam ℕ 0 → m ℕ
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupOrderIso K v =
    { toFun := ⇑(WithZero.map' ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv K v)),
      invFun := ⇑(WithZero.map' ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletion.valueGroupEquiv K v).symm),
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_le_map_iff' := ⋯ }
-- Init.Grind.AC
Lean.Grind.AC.diseq_norm_ai : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  {x : Std.LawfulIdentity ctx.op (Lean.Grind.AC.Var.denote ctx 0)} (lhs rhs : Lean.Grind.AC.Expr)
  (lhs' rhs' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.eq_norm_ai_cert lhs rhs lhs' rhs' = true →
    Lean.Grind.AC.Expr.denote ctx lhs ≠ Lean.Grind.AC.Expr.denote ctx rhs →
      Lean.Grind.AC.Seq.denote ctx lhs' ≠ Lean.Grind.AC.Seq.denote ctx rhs'
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instStarAddMonoid : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddMonoid β] →
          [inst_3 : StarAddMonoid β] →
            [ContinuousStar β] → [inst_5 : ContinuousAdd β] → StarAddMonoid (ZeroAtInftyContinuousMap α β)
-- Mathlib.Computability.Reduce
/-- Lifts a function on sets of natural numbers to many-one degrees.  -/
ManyOneDegree.liftOn : {φ : Sort u_1} → ManyOneDegree → (f : Set ℕ → φ) → (∀ (p q : ℕ → Prop), ManyOneEquiv p q → f p = f q) → φ
-- Mathlib.Algebra.DirectSum.Module
DirectSum.component_comp_lof_same : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i : ι),
  DirectSum.component R ι M i ∘ₗ DirectSum.lof R ι M i = LinearMap.id
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddEquiv.ofLeftInverse.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (f : M →ₙ+ N) {g : N → M}
  (h : Function.LeftInverse g ⇑f),
  AddEquiv.ofLeftInverse f h =
    { toFun := ⇑f.srangeRestrict, invFun := g ∘ ⇑(AddMemClass.subtype f.srange), left_inv := h, right_inv := ⋯,
      map_add' := ⋯ }
-- Mathlib.Topology.UniformSpace.Equicontinuity
Equicontinuous.equicontinuousOn : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α},
  Equicontinuous F → ∀ (S : Set X), EquicontinuousOn F S
-- Mathlib.Order.Filter.Extr
isMaxOn_iff : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α}, IsMaxOn f s a ↔ ∀ x ∈ s, f x ≤ f a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.arccos_pos : ∀ {x : ℝ}, 0 < Real.arccos x ↔ x < 1
-- Mathlib.AlgebraicTopology.SimplicialSet.CoherentIso
CategoryTheory.WalkingIso.fromIso_one : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (e : X ≅ Y),
  (CategoryTheory.WalkingIso.fromIso e).obj CategoryTheory.WalkingIso.one = Y
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.Localizations.comapFun_mk : ∀ {R M : Type u} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u} [inst_3 : CommRing S]
  {N : Type u} [inst_4 : AddCommGroup N] [inst_5 : Module S N] {σ : R →+* S} (f : M →ₛₗ[σ] N)
  (y : ↑(AlgebraicGeometry.PrimeSpectrum.Top S)) (a : M) (b : ↥(PrimeSpectrum.comap σ y).asIdeal.primeCompl),
  (AlgebraicGeometry.StructureSheaf.Localizations.comapFun f y) (LocalizedModule.mk a b) =
    LocalizedModule.mk (f a) ⟨σ ↑b, ⋯⟩
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReducePostconditionInductionMotive.eq_1 : ∀ {n : ℕ} (c_arr : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignment : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) (idx : ℕ)
  (res : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.ReducePostconditionInductionMotive c_arr assignment idx res =
    ((res = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty →
        ∀ (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool),
          (∀ (i : Fin c_arr.size), ↑i < idx → ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c_arr[i]) ∨
            ¬Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p assignment) ∧
      ∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)),
        res = Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit l →
          ∀ (p : Std.Tactic.BVDecide.LRAT.Internal.PosFin n → Bool),
            Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p assignment →
              (∃ i, ↑i < idx ∧ Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p c_arr[i]) →
                Std.Tactic.BVDecide.LRAT.Internal.Entails.eval p l)
-- Mathlib.Order.SuccPred.Tree
IsPredArchimedean.pred_findAtom : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : IsPredArchimedean α] [inst_3 : OrderBot α]
  [inst_4 : DecidableEq α] (r : α), Order.pred (IsPredArchimedean.findAtom r) = ⊥
-- Mathlib.Analysis.Distribution.TestFunction
/-- **Alias** of `FunLike.coe_neg`. -/
TestFunction.coe_neg : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Neg F] [inst_2 : Neg β]
  [IsNegApply F α β] (f : F), ⇑(-f) = -⇑f
-- Mathlib.CategoryTheory.Discrete.Basic
CategoryTheory.Discrete.opposite_functor_obj_as : ∀ (α : Type u₁) (X : (CategoryTheory.Discrete α)ᵒᵖ),
  ((CategoryTheory.Discrete.opposite α).functor.obj X).as = (Opposite.unop X).as
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_le_minKey!_erase : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    (compare t.minKey! (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey!).isLE = true
-- Mathlib.Algebra.Group.Hom.Defs
instCoeTCAddHomOfAddHomClass.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Add M] [inst_1 : Add N] [inst_2 : FunLike F M N]
  [inst_3 : AddHomClass F M N], instCoeTCAddHomOfAddHomClass = { coe := AddHomClass.toAddHom }
-- Mathlib.Algebra.Category.Grp.Ulift
AddCommGrpCat.uliftFunctorFullyFaithful.eq_1 : AddCommGrpCat.uliftFunctorFullyFaithful =
  {
    preimage := fun {X Y} f =>
      AddCommGrpCat.ofHom
        (AddEquiv.ulift.toAddMonoidHom.comp ((AddCommGrpCat.Hom.hom f).comp AddEquiv.ulift.symm.toAddMonoidHom)),
    map_preimage := @AddCommGrpCat.uliftFunctorFullyFaithful._proof_1,
    preimage_map := @AddCommGrpCat.uliftFunctorFullyFaithful._proof_2 }
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Set.natCard_mul_le : ∀ {M : Type u_2} [inst : Mul M] {s t : Set M} [IsCancelMul M], Nat.card ↑(s * t) ≤ Nat.card ↑s * Nat.card ↑t
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- Also known as the maximality axiom.  -/
CategoryTheory.GrothendieckTopology.top_mem : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (X : C), ⊤ ∈ J X
-- Mathlib.ModelTheory.Syntax
/-- The `Finset` of free variables used in a given formula.  -/
FirstOrder.Language.BoundedFormula.freeVarFinset : {L : FirstOrder.Language} → {α : Type u'} → [DecidableEq α] → {n : ℕ} → L.BoundedFormula α n → Finset α
-- Std.Data.ExtHashMap.Lemmas
/-- Simpler variant of `getElem?_filterMap` when `LawfulBEq` is available.  -/
Std.ExtHashMap.getElem?_filterMap' : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {f : α → β → Option γ} {k : α}, (Std.ExtHashMap.filterMap f m)[k]? = m[k]?.bind fun x => f k x
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.applySimpResultToFVarId : Lean.MVarId → Lean.FVarId → Lean.Meta.Simp.Result → Bool → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Batteries.Lean.Meta.UnusedNames
/-- Obtain a name `n` such that `n` is unused in the given local context and
`suggestion` is a prefix of `n`. This is similar to `getUnusedName` but uses
a different algorithm which may or may not be faster.
 -/
Lean.LocalContext.getUnusedUserName : Lean.LocalContext → Lean.Name → Lean.Name
-- Mathlib.MeasureTheory.MeasurableSpace.MeasurablyGenerated
MeasurableSet.Subtype.instInf : {α : Type u_1} → [inst : MeasurableSpace α] → Min (Subtype MeasurableSet)
-- Mathlib.MeasureTheory.Measure.Restrict
MeasureTheory.Measure.restrict_smul : ∀ {α : Type u_2} {_m0 : MeasurableSpace α} {R : Type u_7} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R) (μ : MeasureTheory.Measure α) (s : Set α),
  (c • μ).restrict s = c • μ.restrict s
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.View.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} {size : ℕ} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (k : α) (v : β k)
  (tree : Std.DTreeMap.Internal.Impl.Tree α β size),
  sizeOf { k := k, v := v, tree := tree } = 1 + sizeOf k + sizeOf v + sizeOf tree
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.coe_mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : Set α) (h : IsCompact s), ↑{ carrier := s, isCompact' := h } = s
-- Mathlib.CategoryTheory.Triangulated.HomologicalFunctor
CategoryTheory.Functor.instAdditiveOfIsHomological : ∀ {C : Type u_1} {A : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} A] (F : CategoryTheory.Functor C A)
  [inst_3 : CategoryTheory.Limits.HasZeroObject C] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  [inst_7 : CategoryTheory.Abelian A] [F.IsHomological], F.Additive
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If `f` is continuous on a compact set `K`, then it is integrable on any measurable subset
`s ⊆ K` of finite measure.  -/
ContinuousOn.integrableOn_of_subset_isCompact : ∀ {X : Type u_1} {E : Type u_6} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure X} {s : Set X} [OpensMeasurableSpace X] {K : Set X} {f : X → E},
  ContinuousOn f K → IsCompact K → MeasurableSet s → s ⊆ K → μ s ≠ ⊤ → MeasureTheory.IntegrableOn f s μ
-- Batteries.Data.List.Lemmas
List.findIdxNth_lt_length_iff : ∀ {α : Type u_1} {p : α → Bool} {n : ℕ} {xs : List α}, List.findIdxNth p xs n < xs.length ↔ n < List.countP p xs
-- Mathlib.Topology.Order.Compact
IsCompact.isGLB_sInf : ∀ {α : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α] [ClosedIicTopology α]
  {s : Set α}, IsCompact s → s.Nonempty → IsGLB s (sInf s)
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.HeapNode.rankTR.go.eq_1 : ∀ {α : Type u_1} (a : ℕ), Batteries.BinomialHeap.Imp.HeapNode.rankTR.go Batteries.BinomialHeap.Imp.HeapNode.nil a = a
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentColorParams.toJson : Lean.Lsp.DocumentColorParams → Lean.Json
-- Mathlib.NumberTheory.NumberField.InfinitePlace.TotallyRealComplex
NumberField.isTotallyReal_iff : ∀ (K : Type u_1) [inst : Field K], NumberField.IsTotallyReal K ↔ ∀ (v : NumberField.InfinitePlace K), v.IsReal
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.functor_map_ε_inverse_comp_counit_app_assoc : ∀ {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 D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorUnit D ⟶ Z),
  CategoryTheory.CategoryStruct.comp (e.functor.map (CategoryTheory.Functor.LaxMonoidal.ε e.inverse))
      (CategoryTheory.CategoryStruct.comp (e.counit.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η e.functor) h
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.instStateT : {m : Type u_1 → Type u_2} →
  {ρ : Type u_1} → [inst : Monad m] → [inst_1 : LawfulMonad m] → [MonadSatisfying m] → MonadSatisfying (StateT ρ m)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_toArray_rco : ∀ {m n : ℤ}, (m...=n).toArray = (m...n + 1).toArray
-- Init.Data.List.Monadic
List.anyM_cons : ∀ {m : Type → Type u_1} {α : Type u_2} [inst : Monad m] {p : α → m Bool} {x : α} {xs : List α},
  List.anyM p (x :: xs) = do
    let __do_lift ← p x
    if __do_lift = true then pure true else List.anyM p xs
-- Init.Data.Nat.Lemmas
/-- If a small natural number is divisible by a larger natural number,
the small number is zero.  -/
Nat.eq_zero_of_dvd_of_lt : ∀ {a b : ℕ}, a ∣ b → b < a → b = 0
-- Mathlib.Dynamics.SymbolicDynamics.Basic
/-- Finite support of the pattern.  -/
SymbolicDynamics.FullShift.Pattern.support : {A : Type u_1} → {G : Type u_2} → [inst : Inhabited A] → SymbolicDynamics.FullShift.Pattern A G → Finset G
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
AddCircle.homeomorphCircle.eq_1 : ∀ {T : ℝ} (hT : T ≠ 0),
  AddCircle.homeomorphCircle hT =
    (AddCircle.homeomorphAddCircle T (2 * Real.pi) hT AddCircle.homeomorphCircle._proof_1).trans
      AddCircle.homeomorphCircle'
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Structure.Fg.instCountable_embedding : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] (N : Type u_2) [inst_1 : L.Structure N] [Countable N]
  [h : FirstOrder.Language.Structure.FG L M], Countable (L.Embedding M N)
-- Lean.Compiler.InlineAttrs
Lean.Compiler.instHashableInlineAttributeKind.hash : Lean.Compiler.InlineAttributeKind → UInt64
-- Mathlib.Order.Partition.Finpartition
Finpartition.ne_bot : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {a : α} (P : Finpartition a) {b : α}, b ∈ P.parts → b ≠ ⊥
-- Init.Data.List.Sublist
List.Sublist.of_sublist_append_right : ∀ {α : Type u_1} {l l₁ l₂ : List α}, (∀ a ∈ l, a ∉ l₁) → l.Sublist (l₁ ++ l₂) → l.Sublist l₂
-- Init.Data.Nat.Div.Basic
Nat.modCore_eq_mod : ∀ (n m : ℕ), n.modCore m = n % m
-- Mathlib.Order.BoundedOrder.Basic
/-- **Alias** of the forward direction of `isTop_iff_eq_top`. -/
IsTop.eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsTop a → a = ⊤
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNat_of_lt : ∀ {n : ℕ}, n < UInt16.size → UInt16.toNat (OfNat.ofNat n) = n
-- Mathlib.Analysis.Convex.BetweenList
Function.Injective.list_wbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {l : List P} {f : P →ᵃ[R] P'},
  Function.Injective ⇑f → (List.Wbtw R (List.map (⇑f) l) ↔ List.Wbtw R l)
-- Mathlib.Order.Irreducible
SupIrred.finset_sup_eq : ∀ {ι : Type u_1} {α : Type u_2} [inst : SemilatticeSup α] {a : α} [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α},
  SupIrred a → s.sup f = a → ∃ i ∈ s, f i = a
-- Mathlib.Geometry.Manifold.Instances.Real
EuclideanHalfSpace.ext : ∀ {n : ℕ} [inst : NeZero n] (x y : EuclideanHalfSpace n), ↑x = ↑y → x = y
-- Mathlib.Topology.Semicontinuity.Defs
semicontinuousOn_univ_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {r : α → β → Prop},
  SemicontinuousOn r Set.univ ↔ Semicontinuous r
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.monMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategory (CategoryTheory.Mon C)
-- Plausible.Gen
Plausible.instBEqGenError.beq : Plausible.GenError → Plausible.GenError → Bool
-- Mathlib.LinearAlgebra.Pi
LinearEquiv.funUnique_apply : ∀ (ι : Type u_5) (R : Type u_6) (M : Type u_7) [inst : Unique ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], ⇑(LinearEquiv.funUnique ι R M) = Function.eval default
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Iso.symm_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C}, Function.Bijective CategoryTheory.Iso.symm
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_eq_getValueCast! : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
  [inst_2 : Inhabited (β a)] (h : Std.Internal.List.containsKey a l = true),
  Std.Internal.List.getValueCast a l h = Std.Internal.List.getValueCast! a l
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.sSup_simples_le : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSemisimpleModule R M]
  (N : Submodule R M), sSup {m | IsSimpleModule R ↥m ∧ m ≤ N} = N
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Real
ENNReal.measurable_of_measurable_nnreal_prod : ∀ {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace β} {x_1 : MeasurableSpace γ} {f : ENNReal × β → γ},
  (Measurable fun p => f (↑p.1, p.2)) → (Measurable fun x => f (⊤, x)) → Measurable f
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.mono : ∀ {α : Type u_1} {G H : SimpleGraph α} {n : ℕ} {s : Finset α}, G ≤ H → G.IsNClique n s → H.IsNClique n s
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.star_eq_inv' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M}, star = Inv.inv
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_inter_eq_size_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (∀ a ∈ m₂, a ∈ m₁) → (m₁ ∩ m₂).size = m₂.size
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.interSmallerFn.match_3.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Option ((a : α) × β a) → Sort u_3) →
      (x : Option ((a : α) × β a)) → ((kv' : (a : α) × β a) → motive (some kv')) → (Unit → motive none) → motive x
-- Aesop.Util.Basic
Aesop.compareArraySizeThenLex : {α : Type u_1} → (α → α → Ordering) → Array α → Array α → Ordering
-- Mathlib.Algebra.ContinuedFractions.Computation.Basic
_private.Mathlib.Algebra.ContinuedFractions.Computation.Basic.0.GenContFract.IntFractPair.stream.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.OptionT.wp_apply_eq : ∀ {m : Type u → Type z} {α Pred : Type u} {EPred : Type u_1} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] (x : OptionT m α)
  (post : α → Pred) (epost : EPost.Cons✝ Pred EPred),
  Std.Internal.Do.wp x post epost =
    Std.Internal.Do.wp x.run (Std.Internal.Do.EPost.Cons.pushOption post epost) epost.tail