mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.FoelnerFilter
isFoelner_iff_tendsto : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : Group G]
  [inst_2 : MulAction G X] {ι : Type u_3} (l : Filter ι) (F : ι → Set X),
  IsFoelner G μ l F ↔ Filter.Tendsto F l (maxFoelner G μ)
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.instFiniteResidueFieldAtPrimeFiber : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] (p : Ideal R) [inst_4 : p.IsPrime] (q : Ideal (p.Fiber S)) [inst_5 : q.IsPrime],
  Module.Finite p.ResidueField (Localization.AtPrime q)
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_rcc : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Rcc.Sliceable.mkSlice xs lo...=hi) = (List.drop lo (List.take (hi + 1) xs)).toArray
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.getEntryLE.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Ord α] (k : α)
  (motive : (x : Std.DTreeMap.Internal.Impl α fun x => β) → x.Ordered → (∃ a ∈ x, (compare a k).isLE = true) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true)
  (h_1 :
    (x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
      (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, (compare a k).isLE = true) →
        motive Std.DTreeMap.Internal.Impl.leaf x he)
  (h_2 :
    (size : ℕ) →
      (ky : α) →
        (y : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, (compare a k).isLE = true) →
                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he),
  (match Std.DTreeMap.Internal.Impl.leaf, x, he with
    | Std.DTreeMap.Internal.Impl.leaf, x, he => h_1 x he
    | Std.DTreeMap.Internal.Impl.inner size ky y l r, ho, he => h_2 size ky y l r ho he) =
    h_1 x he
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.sInf_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Set (Subalgebra R A)), Subalgebra.toSubmodule (sInf S) = sInf (⇑Subalgebra.toSubmodule '' S)
-- Init.Data.List.MinMaxIdx
List.getElem_maxIdxOn : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {f : α → β}
  {xs : List α} (h : xs ≠ []), xs[List.maxIdxOn f xs h] = List.maxOn f xs h
-- Mathlib.Data.Nat.Bits
Nat.bodd_succ : ∀ (n : ℕ), n.succ.bodd = !n.bodd
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.semanticTokensProvider? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.SemanticTokensOptions
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.Finite.toFinset_vsub : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : VSub α β] {s t : Set β} (hs : s.Finite) (ht : t.Finite)
  (hf : optParam (s -ᵥ t).Finite ⋯), hf.toFinset = hs.toFinset -ᵥ ht.toFinset
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_iterate_pred : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι} [NoMinOrder ι] (n : ℕ), toZ i0 (Order.pred^[n] i0) = -↑n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.size_ofList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l → (Std.DHashMap.Raw.ofList l).size = l.length
-- Mathlib.CategoryTheory.Action.Basic
/-- **Alias** of `Action.actionPUnitEquivalence`.

---

Actions/representations of the trivial monoid are just objects in the ambient category.  -/
Action.actionPunitEquivalence : {V : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} V] → Action V PUnit.{u_3 + 1} ≌ V
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.impImpSimp.injEq : ∀ (x : Lean.Name) (p : Mathlib.Tactic.ITauto.Proof) (x_1 : Lean.Name) (p_1 : Mathlib.Tactic.ITauto.Proof),
  (Mathlib.Tactic.ITauto.Proof.impImpSimp x p = Mathlib.Tactic.ITauto.Proof.impImpSimp x_1 p_1) = (x = x_1 ∧ p = p_1)
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.pattern.injEq : ∀ (stx stx_1 : Lean.Term),
  (Aesop.Frontend.BuilderOption.pattern stx = Aesop.Frontend.BuilderOption.pattern stx_1) = (stx = stx_1)
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.to_normal : ∀ {F : Type u_1} {inst : Field F} {E : Type u_2} {inst_1 : Field E} {inst_2 : Algebra F E} [self : IsGalois F E],
  Normal F E
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {H : LieSubalgebra R L} (α χ : ↥H → R) (p q : ℤ) [inst_7 : LieRing.IsNilpotent ↥H],
  LieModule.genWeightSpace M (p • α + χ) = ⊥ →
    ∀ {x : L},
      x ∈ LieAlgebra.rootSpace H (-α) →
        ∀ {y : M}, y ∈ LieModule.genWeightSpaceChain M α χ p q → ⁅x, y⁆ ∈ LieModule.genWeightSpaceChain M α χ p q
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.NormalExpr.brecOn.go : {motive : Mathlib.Tactic.BicategoryLike.NormalExpr → Sort u} →
  (t : Mathlib.Tactic.BicategoryLike.NormalExpr) →
    ((t : Mathlib.Tactic.BicategoryLike.NormalExpr) → Mathlib.Tactic.BicategoryLike.NormalExpr.below t → motive t) →
      motive t ×' Mathlib.Tactic.BicategoryLike.NormalExpr.below t
-- Mathlib.Topology.Separation.Basic
eventually_ne_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {a b : X}, a ≠ b → ∀ᶠ (x : X) in nhds a, x ≠ b
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow.congr_simp : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A] (a a_1 : A),
  a = a_1 → ∀ (y y_1 : NNReal), y = y_1 → CFC.nnrpow a y = CFC.nnrpow a_1 y_1
-- Mathlib.CategoryTheory.Generator.Preadditive
CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (G : C),
  CategoryTheory.IsSeparator G ↔ (CategoryTheory.preadditiveCoyonedaObj G).Faithful
-- Mathlib.Data.Set.Constructions
FiniteInter.mk : ∀ {α : Type u_1} {S : Set (Set α)},
  Set.univ ∈ S → (∀ ⦃s : Set α⦄, s ∈ S → ∀ ⦃t : Set α⦄, t ∈ S → s ∩ t ∈ S) → FiniteInter S
-- Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage
Function.Semiconj.preimage_dynEntourage : ∀ {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (U : Set (Y × Y)) (n : ℕ),
      Prod.map φ φ ⁻¹' Dynamics.dynEntourage T U n = Dynamics.dynEntourage S (Prod.map φ φ ⁻¹' U) n
-- Mathlib.Algebra.Order.Monoid.Lex
OrderMonoidHom.fstₗ_comp_inlₗ : ∀ (α : Type u_1) (β : Type u_2) [inst : Monoid α] [inst_1 : PartialOrder α] [inst_2 : Monoid β] [inst_3 : Preorder β],
  (OrderMonoidHom.fstₗ α β).comp (OrderMonoidHom.inlₗ α β) = OrderMonoidHom.id α
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.coconeOfPreserves_pt_right : ∀ {J : Type w} [inst : CategoryTheory.Category.{w', w} J] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  {B : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃}
  [inst_3 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T}
  (F : CategoryTheory.Functor J (CategoryTheory.Comma L R))
  [inst_4 : CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L]
  {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁)
  (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))),
  (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.right = c₂.pt
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.notMem_of_notMem_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {S : Set E} {s : E},
  s ∉ IntermediateField.adjoin F S → s ∉ S
-- Mathlib.Topology.Algebra.Group.Basic
tendsto_inv_nhdsLT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousInv H] {a : H}, Filter.Tendsto Inv.inv (nhdsWithin a (Set.Iio a)) (nhdsWithin a⁻¹ (Set.Ioi a⁻¹))
-- Lean.Message
Lean.MessageData.ofWidget.injEq : ∀ (a : Lean.Widget.WidgetInstance) (a_1 : Lean.MessageData) (a_2 : Lean.Widget.WidgetInstance) (a_3 : Lean.MessageData),
  (Lean.MessageData.ofWidget a a_1 = Lean.MessageData.ofWidget a_2 a_3) = (a = a_2 ∧ a_1 = a_3)
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.comp.congr_simp : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q Q_1 : Algebra.Generators S T ι'),
  Q = Q_1 → ∀ (P P_1 : Algebra.Generators R S ι), P = P_1 → Q.comp P = Q_1.comp P_1
-- Mathlib.Topology.Instances.TrivSqZeroExt
TrivSqZeroExt.hasSum_snd : ∀ {α : Type u_1} {R : Type u_3} (M : Type u_4) [inst : TopologicalSpace R] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid R] [inst_3 : AddCommMonoid M] {f : α → TrivSqZeroExt R M} {a : TrivSqZeroExt R M},
  HasSum f a → HasSum (fun x => (f x).snd) a.snd
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.whiskeringEquivalence_inverse : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (e : K ≌ J),
  (CategoryTheory.Limits.Cocone.whiskeringEquivalence e).inverse =
    (CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
      (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv)
-- Mathlib.Topology.Algebra.Group.Basic
Homeomorph.subRight_apply : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalAddGroup G] (x b : G),
  (Homeomorph.subRight x) b = b - x
-- Mathlib.Data.Num.Basic
/-- Division of `PosNum`  -/
PosNum.div' : PosNum → PosNum → Num
-- Mathlib.SetTheory.Cardinal.Finite
ENat.card_eq_top : ∀ {α : Type u_1}, ENat.card α = ⊤ ↔ Infinite α
-- Lean.Environment
Lean.ConstantKind.ctor.sizeOf_spec : sizeOf Lean.ConstantKind.ctor = 1
-- Mathlib.GroupTheory.Congruence.Basic
AddCon.comapQuotientEquivOfSurj_symm_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (c : AddCon M) {f : N →+ M}
  (hf : Function.Surjective ⇑f) (x : N), (c.comapQuotientEquivOfSurj f hf).symm ↑(f x) = ↑x
-- Init.Data.UInt.Lemmas
USize.sub_neg : ∀ {a b : USize}, a - -b = a + b
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.mul_sub_right_left_iff : ∀ {R : Type u_1} [inst : CommRing R] {x y z : R}, IsRelPrime (z * y - x) y ↔ IsRelPrime x y
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_iInf : ∀ {ι : Sort u_1} {R : Type u_2} [inst : NonAssocSemiring R] (S : ι → Subsemiring Rᵐᵒᵖ), (iInf S).unop = ⨅ i, (S i).unop
-- Init.Data.Vector.Lemmas
Vector.getElem_flatten : ∀ {β : Type u_1} {m n : ℕ} {xss : Vector (Vector β m) n} {i : ℕ} (hi : i < n * m), xss.flatten[i] = xss[i / m][i % m]
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.Hom.ext_iff : ∀ {A B : Semigrp} {x y : A.Hom B}, x = y ↔ x.hom' = y.hom'
-- Mathlib.Order.Interval.Finset.Floor
Int.cast_mem_Ico_iff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a b : α} {n : ℤ},
  ↑n ∈ Set.Ico a b ↔ n ∈ Finset.Ico ⌈a⌉ ⌈b⌉
-- Init.Data.UInt.Lemmas
USize.ofNat_uInt16ToNat : ∀ (n : UInt16), USize.ofNat n.toNat = n.toUSize
-- Mathlib.GroupTheory.Coset.Defs
QuotientGroup.mk.eq_1 : ∀ {α : Type u_1} [inst : Group α] {s : Subgroup α} (a : α), ↑a = Quotient.mk'' a
-- Mathlib.Geometry.RingedSpace.Basic
/-- The type of Ringed spaces, as an abbreviation for `SheafedSpace CommRingCat`.  -/
AlgebraicGeometry.RingedSpace : Type (max (u + 1) (v + 1))
-- Mathlib.Analysis.Seminorm
/-- Seminorm-balls containing the origin are absorbent.  -/
Seminorm.absorbent_closedBall : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ} {x : E}, p x < r → Absorbent 𝕜 (p.closedBall x r)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_algebraMap : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : CommRing R],
  ⇑(algebraMap R (QuaternionAlgebra R c₁ c₂ c₃)) = QuaternionAlgebra.coe
-- Mathlib.Data.Matrix.Mul
Matrix.mulVec_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n]
  [inst_2 : DistribSMul R α] [SMulCommClass R α α] (M : Matrix m n α) (b : R) (v : n → α),
  M.mulVec (b • v) = b • M.mulVec v
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.unbounded_range_of_le_iSup : ∀ {α β : Type u} (r : α → α → Prop) [inst : IsWellOrder α r] (f : β → α),
  Ordinal.type r ≤ ⨆ i, (Ordinal.typein r).toRelEmbedding (f i) → Set.Unbounded r (Set.range f)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsion_gc : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  GaloisConnection Submodule.annihilator fun I => Submodule.torsionBySet R M ↑(OrderDual.ofDual I)
-- Mathlib.RingTheory.Valuation.Integers
Valuation.instAlgebraSubtypeMemSubringInteger : {R : Type u} →
  {Γ₀ : Type v} →
    [inst : CommRing R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → (v : Valuation R Γ₀) → Algebra (↥v.integer) R
-- Mathlib.Topology.List
List.Vector.tendsto_insertIdx : ∀ {α : Type u_1} [inst : TopologicalSpace α] {n : ℕ} {i : Fin (n + 1)} {a : α} {l : List.Vector α n},
  Filter.Tendsto (fun p => List.Vector.insertIdx p.1 i p.2) (nhds a ×ˢ nhds l) (nhds (List.Vector.insertIdx a i l))
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.distinguished_iff_of_isZero₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  CategoryTheory.Limits.IsZero T.obj₂ →
    (T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔ CategoryTheory.IsIso T.mor₃)
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- The functor `Under.forget X : Under X ⥤ C` has a left adjoint given by `costar X`.

Note that the binary coproducts assumption is necessary: the existence of a left adjoint to
`Under.forget X` is equivalent to the existence of each binary coproduct `X ⨿ -`.  -/
CategoryTheory.Under.costarAdjForget : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] →
        CategoryTheory.Under.costar X ⊣ CategoryTheory.Under.forget X
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonResolveSupport.fromJson : Lean.Json → Except String Lean.Lsp.ResolveSupport
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.toFinset_vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] (a : α) (s : Set β) [inst_2 : Fintype ↑s]
  [inst_3 : Fintype ↑(a +ᵥ s)], (a +ᵥ s).toFinset = a +ᵥ s.toFinset
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.map_subtype_commutator : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), Subgroup.map H.subtype (commutator ↥H) = ⁅H, H⁆
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.Num.gcdAux.match_1.eq_2 : ∀ (motive : ℕ → Num → Num → Sort u_1) (n : ℕ) (b : Num) (h_1 : (x b : Num) → motive 0 x b)
  (h_2 : (n : ℕ) → (b : Num) → motive n.succ Num.zero b) (h_3 : (n : ℕ) → (a b : Num) → motive n.succ a b),
  (match n.succ, Num.zero, b with
    | 0, x, b => h_1 x b
    | n.succ, Num.zero, b => h_2 n b
    | n.succ, a, b => h_3 n a b) =
    h_2 n b
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_ofDual : ∀ {α : Type u_1} [inst : Preorder α] {x y : αᵒᵈ},
  Set.Ico (OrderDual.ofDual y) (OrderDual.ofDual x) = ⇑OrderDual.toDual ⁻¹' Set.Ioc x y
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.liftMagma_symm_apply : ∀ (R : Type u_1) {A : Type u_4} {M : Type u_7} [inst : Semiring R] [inst_1 : Mul M]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : Module R A] [inst_4 : IsScalarTower R A A]
  [inst_5 : SMulCommClass R A A] (F : MonoidAlgebra R M →ₙₐ[R] A),
  (MonoidAlgebra.liftMagma R).symm F = F.toMulHom.comp (MonoidAlgebra.ofMagma R M)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.mkIso_hom_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (e : ρ.Equiv σ), Rep.Hom.hom (Rep.mkIso e).hom = ↑e
-- Mathlib.Algebra.Field.Subfield.Basic
_private.Mathlib.Algebra.Field.Subfield.Basic.0.Subfield.commClosure_eq_closure : ∀ {K : Type u} [inst : Field K] {s : Set K}, Subfield.commClosure✝ s = Subfield.closure s
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.instFunLikeElemForall : {S : Type u_1} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] → {X : Type u_2} → [inst_2 : Fintype X] → FunLike (↑(stdSimplex S X)) X S
-- Std.Data.TreeSet.Raw.Basic
/-- Creates a new empty tree set. It is also possible and recommended to
use the empty collection notations `∅` and `{}` to create an empty tree set. `simp` replaces
`empty` with `∅`.
 -/
Std.TreeSet.Raw.merge : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
/-- Given a finite cyclic group `G` generated by `g : G` and a `k`-linear `G`-representation `A`,
this is the periodic chain complex in `Rep k G` given by
`0 ⟶ A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A --N--> A ⟶ ...` where `N` is the norm map.
Its cohomology is the group cohomology of `A`.  -/
Rep.FiniteCyclicGroup.moduleCatCochainComplex : {k G : Type u} →
  [inst : CommRing k] → [inst_1 : CommGroup G] → [Fintype G] → Rep.{u_1, u, u} k G → G → CochainComplex (ModuleCat k) ℕ
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.leftUnitor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasTerminal C] (P : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct (⊤_ C) P],
  (CategoryTheory.Limits.prod.leftUnitor P).hom = CategoryTheory.Limits.prod.snd
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_add : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Add R] (a b : QuaternionAlgebra R c₁ c₂ c₃), (a + b).imK = a.imK + b.imK
-- Mathlib.Order.Lattice
/-- **Alias** of the reverse direction of `inf_eq_right`. -/
inf_of_le_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, b ≤ a → a ⊓ b = b
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin.neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜}, derivWithin (-f) s x = -derivWithin f s x
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.toLp.congr_simp : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} (f f_1 : MeasureTheory.SimpleFunc α E) (e_f : f = f_1)
  (hf : MeasureTheory.MemLp (⇑f) p μ), f.toLp hf = f_1.toLp ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.sumNodes_eq_sumNodes_T_iff : ∀ {n : ℕ} {c : ℕ → ℝ},
  (∀ i ≤ n, 0 < (-1) ^ i * c i) →
    ∀ {P : Polynomial ℝ},
      P.degree ≤ ↑n →
        (∀ x ∈ Set.Icc (-1) 1, |Polynomial.eval x P| ≤ 1) →
          (Polynomial.Chebyshev.sumNodes n c P = Polynomial.Chebyshev.sumNodes n c (Polynomial.Chebyshev.T ℝ ↑n) ↔
            P = Polynomial.Chebyshev.T ℝ ↑n)
-- Mathlib.Tactic.GrindAttrs
/-- `compactness` is a simple tactic that tries various lemmas to prove that a set is compact.
It is implemented using `grind`, and has the same configuration options as `grind`.

Use `grind only [compactness, closedness]` instead if you want to prove that the closure of sets are
compact.

It also exists as a grind attribute, and can be combined with other grind attributes using
`grind only [compactness, ...]`.
 -/
tacticCompactness?_ : Lean.ParserDescr
-- Lean.PrettyPrinter.Delaborator.Basic
_private.Lean.PrettyPrinter.Delaborator.Basic.0.Lean.PrettyPrinter.Delaborator.addFieldInfo.mkFieldInfo : Lean.Name → Lean.Name → Lean.Syntax → Lean.Expr → Lean.PrettyPrinter.Delaborator.DelabM Lean.Elab.FieldInfo
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.cardSupp_div_le : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : AddCommGroup Γ] [inst_2 : IsOrderedAddMonoid Γ]
  [inst_3 : Field R] (x y : HahnSeries Γ R), (x / y).cardSupp ≤ x.cardSupp * max Cardinal.aleph0 y.cardSupp
-- Plausible.Functions
Plausible.TotalFunction.instRepr : (α : Type u) → (β : Type v) → [Repr α] → [Repr β] → Repr (Plausible.TotalFunction α β)
-- Mathlib.Topology.MetricSpace.Bounded
/-- If two sets intersect, the diameter of the union is bounded by the sum of the diameters.  -/
Metric.diam_union' : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α] {t : Set α},
  (s ∩ t).Nonempty → Metric.diam (s ∪ t) ≤ Metric.diam s + Metric.diam t
-- Lean.Meta.Hint
/-- The span at which this suggestion should apply. This allows a single hint to suggest modifications
at different locations. If `span?` is not specified, then the syntax reference provided to
`MessageData.hint` will be used.
 -/
Lean.Meta.Hint.Suggestion.span? : Lean.Meta.Hint.Suggestion → Option Lean.Syntax
-- Mathlib.Algebra.Algebra.Basic
IsCancelMulZero.of_faithfulSMul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  [IsCancelMulZero A], IsCancelMulZero R
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.IsLocallyDirected.openCover_X : ∀ {J : Type w} [inst : CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme)
  [inst_1 : ∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)]
  [inst_2 : (F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [inst_3 : Quiver.IsThin J]
  [inst_4 : Small.{u, w} J] (a : J), (AlgebraicGeometry.Scheme.IsLocallyDirected.openCover F).X a = F.obj a
-- Mathlib.Order.KrullDimension
Order.coheight_le_of_krullDim_preimage_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : PartialOrder β] {m : ℕ} (f : α →o β),
  (∀ (x : β), Order.krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m) → ∀ (x : α), Order.coheight x ≤ (↑m + 1) * Order.coheight (f x) + ↑m
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) (nonempty : s.Nonempty) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj),
  (Bundle.Pretrivialization.codExtend hs nonempty e).source = e.source
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffOn.restrict_scalars : ∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} {𝕜' : Type u_3} [inst_5 : NontriviallyNormedField 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜']
  [inst_7 : NormedSpace 𝕜' E] [IsScalarTower 𝕜 𝕜' E] [inst_9 : NormedSpace 𝕜' F] [IsScalarTower 𝕜 𝕜' F],
  ContDiffOn 𝕜' n f s → ContDiffOn 𝕜 n f s
-- Mathlib.RingTheory.Ideal.Defs
Ideal.zero_mem : ∀ {α : Type u} [inst : Semiring α] (I : Ideal α), 0 ∈ I