mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Defs
Finset.Iic.eq_1 : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α),
  Finset.Iic a = LocallyFiniteOrderBot.finsetIic a
-- Mathlib.Topology.NhdsWithin
nhdsNE_sup_pure : ∀ {α : Type u_1} [inst : TopologicalSpace α] (a : α), nhdsWithin a {a}ᶜ ⊔ pure a = nhds a
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.pos_of_isNat : ∀ {A : Type u_1} {e : A} {n : ℕ} [inst : Semiring A] [inst_1 : PartialOrder A] [IsOrderedRing A] [Nontrivial A],
  Mathlib.Meta.NormNum.IsNat e n → Nat.ble 1 n = true → 0 < e
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.vadd.eq_1 : ∀ {G : Type u_1} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [inst_3 : MeasurableConstVAdd G α] (c : G),
  MeasurableEquiv.vadd c = { toEquiv := AddAction.toPerm c, measurable_toFun := ⋯, measurable_invFun := ⋯ }
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.throwNonInternalizedExpr : {α : Type} → Lean.Expr → Lean.MetaM α
-- Init.Data.Range.Polymorphic.PRange
/-- A range of elements of `α` with closed lower and upper bounds.

`a...=b` is the range of all values greater than or equal to `a : α` and less than or
equal to `b : α`. This is notation for `Rcc.mk a b`.
 -/
Std.Rcc : Type u → Type u
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.exists_splitMany_inf_eq_filter_of_finite : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} [Finite ι] (s : Set (BoxIntegral.Prepartition I)),
  s.Finite →
    ∃ t,
      ∀ π ∈ s,
        π ⊓ BoxIntegral.Prepartition.splitMany I t =
          (BoxIntegral.Prepartition.splitMany I t).filter fun J => ↑J ⊆ π.iUnion
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.π_comp_eqToHom_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] {j j' : J} (hj : j = j') {Z : C}
  (h : F.obj j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j') h
-- Init.Prelude
Nat.lt_of_lt_of_le : ∀ {n m k : ℕ}, n < m → m ≤ k → n < k
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.instAdditiveTruncGT : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), (t.truncGT n).Additive
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- The normal subgroupoid generated by the set of arrows `X`  -/
CategoryTheory.Subgroupoid.generatedNormal : {C : Type u} → [inst : CategoryTheory.Groupoid C] → ((c d : C) → Set (c ⟶ d)) → CategoryTheory.Subgroupoid C
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionDisabled.toJson : Lean.Lsp.CodeActionDisabled → Lean.Json
-- Init.Data.Vector.Lemmas
Vector.back_append_left : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {ys : Vector α 0} [inst : NeZero n], (xs ++ ys).back = xs.back
-- Mathlib.Algebra.Group.Commute.Defs
Commute.pow_pow : ∀ {M : Type u_2} [inst : Monoid M] {a b : M}, Commute a b → ∀ (m n : ℕ), Commute (a ^ m) (b ^ n)
-- Mathlib.FieldTheory.Separable
Polynomial.exists_separable_of_irreducible : ∀ {F : Type u} [inst : Field F] (p : ℕ) [HF : CharP F p] {f : Polynomial F},
  Irreducible f → p ≠ 0 → ∃ n g, g.Separable ∧ (Polynomial.expand F (p ^ n)) g = f
-- Mathlib.Analysis.Complex.Order
Complex.pos_iff : ∀ {z : ℂ}, 0 < z ↔ 0 < z.re ∧ 0 = z.im
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic
CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeFun : CategoryTheory.Limits.PreservesLimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (CategoryTheory.forget (Type u))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.coe_toMonoidHom : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (f : A →ₜ* B), f.toMonoidHom = ↑f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.FunDecl.mk : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.FVarId →
    Lean.Name →
      Array (Lean.Compiler.LCNF.Param pu) → Lean.Expr → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.FunDecl pu
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
/-- Construct a pseudofunctor from an oplax functor whose `mapId` and `mapComp` are isomorphisms.  -/
CategoryTheory.Pseudofunctor.mkOfOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        (F : CategoryTheory.OplaxFunctor B C) → F.PseudoCore → CategoryTheory.Pseudofunctor B C
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- A first quadrant cohomological spectral sequence has differentials
given by the vector `(r, 1 - r)` on the `r`th page.  -/
CategoryTheory.CohomologicalSpectralSequenceNat : (C : Type u_1) → [inst : CategoryTheory.Category.{u_3, u_1} C] → [CategoryTheory.Abelian C] → ℤ → Type (max u_1 u_3)
-- Mathlib.Combinatorics.Quiver.ReflQuiver
/-- `Vᵒᵖ` reverses the direction of all arrows of `V`.  -/
CategoryTheory.ReflQuiver.opposite : {V : Type u_1} → [CategoryTheory.ReflQuiver V] → CategoryTheory.ReflQuiver Vᵒᵖ
-- Mathlib.Topology.ClusterPt
Filter.HasBasis.clusterPt_iff_frequently' : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {ι : Sort u_3} {p : ι → Prop} {s : ι → Set X} {F : Filter X},
  F.HasBasis p s → (ClusterPt x F ↔ ∀ (i : ι), p i → ∃ᶠ (x : X) in nhds x, x ∈ s i)
-- Mathlib.Topology.Semicontinuity.Defs
upperSemicontinuousWithinAt_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : Preorder β] {f : α → β} {s : Set α} {x : α},
  UpperSemicontinuousWithinAt f s x ↔ ∀ (y : β), f x < y → ∀ᶠ (x' : α) in nhdsWithin x s, f x' < y
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody
NumberField.mixedEmbedding.convexBodySumFun.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.convexBodySumFun x = ∑ w, ↑w.mult * (NumberField.mixedEmbedding.normAtPlace w) x
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.ofPred_top`. -/
Set.setOf_top : ∀ {α : Type u}, {_x | ⊤} = Set.univ
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromTarget.op : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C)
  (Q : CategoryTheory.MorphismProperty C) [P.InheritedFromTarget Q], P.op.InheritedFromSource Q.op
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.toQ_lt : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] [inst_1 : LE α] [inst_2 : LT α] [Std.LawfulOrderLT α]
  [inst_4 : Std.IsPreorder α] [inst_5 : Lean.Grind.OrderedAdd α] {a b : α}, ↑a < ↑b ↔ a < b
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coeIdeal_injective : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_3} [inst_1 : Field K] [inst_2 : Algebra R K] [IsFractionRing R K],
  Function.Injective fun I => ↑I
-- Lean.Meta.Instances
Lean.Meta.DefaultInstanceEntry.priority : Lean.Meta.DefaultInstanceEntry → ℕ
-- Mathlib.Data.PNat.Prime
PNat.gcd_mul_lcm : ∀ (n m : ℕ+), n.gcd m * n.lcm m = n * m
-- Mathlib.Combinatorics.Matroid.Constructions
Matroid.freeOn_indep : ∀ {α : Type u_1} {E I : Set α}, I ⊆ E → (Matroid.freeOn E).Indep I
-- Mathlib.Order.Circular
sbtw_irrefl_right : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b : α}, ¬sbtw a b b
-- Mathlib.GroupTheory.Torsion
/-- **Alias** of `IsMulTorsion.exponentExists`.

---

The group exponent exists for any bounded torsion group.  -/
IsTorsion.exponentExists : ∀ {G : Type u_1} [inst : Group G], IsMulTorsion G → (Set.range fun g => orderOf g).Finite → Monoid.ExponentExists G
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.mk.inj : ∀ {n : ℕ} {blocks : List ℕ} {blocks_pos : ∀ {i : ℕ}, i ∈ blocks → 0 < i} {blocks_sum : blocks.sum = n}
  {blocks_1 : List ℕ} {blocks_pos_1 : ∀ {i : ℕ}, i ∈ blocks_1 → 0 < i} {blocks_sum_1 : blocks_1.sum = n},
  { blocks := blocks, blocks_pos := blocks_pos, blocks_sum := blocks_sum } =
      { blocks := blocks_1, blocks_pos := blocks_pos_1, blocks_sum := blocks_sum_1 } →
    blocks = blocks_1
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries_nilpotencyClass`. -/
upperCentralSeries_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G],
  Subgroup.upperCentralSeries G (Group.nilpotencyClass G) = ⊤
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
/-- The coefficients of the characteristic polynomial are signed sums of principal minors.
Specifically, the (n-k)-th coefficient of the characteristic polynomial of M equals
`(-1)^k` times the sum of all k×k principal minors of M.  -/
Matrix.charpoly_coeff_eq_sum_minors : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  ∀ k ≤ Fintype.card n,
    M.charpoly.coeff (Fintype.card n - k) =
      (-1) ^ k * ∑ s ∈ Finset.powersetCard k Finset.univ, (M.submatrix Subtype.val Subtype.val).det
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.mul_apply : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (f g : CentroidHom α) (a : α), (f * g) a = f (g a)
-- Mathlib.Computability.RecursiveIn
ComputableIn₂.recursiveIn₂ : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β] [inst_2 : Primcodable σ]
  {f : α → β → σ} {O : Set (ℕ →. ℕ)}, ComputableIn₂ O f → RecursiveIn₂ O fun a => ↑(f a)
-- Mathlib.Algebra.Lie.Derivation.Basic
LieDerivation.instFunLike : {R : Type u_1} →
  {L : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] → [inst_6 : LieModule R L M] → FunLike (LieDerivation R L M) L M
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop.0.Std.IterM.findSomeM?.match_1.eq_2 : ∀ {γ : Type u_1} (motive : Option γ → Sort u_2) (fx : γ) (h_1 : Unit → motive none) (h_2 : (fx : γ) → motive (some fx)),
  (match some fx with
    | none => h_1 ()
    | some fx => h_2 fx) =
    h_2 fx
-- Mathlib.Topology.Homeomorph.Defs
/-- Homeomorphism between `X` and `Y`, also called topological isomorphism  -/
«term_≃ₜ_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Noetherian
CategoryTheory.Artinian.toEssentiallySmall : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Artinian C],
  CategoryTheory.EssentiallySmall.{u_2, v_1, u_1} C
-- Init.Prelude
/-- Decides whether two 16-bit unsigned integers are equal. Usually accessed via the
`DecidableEq UInt16` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `UInt16.decEq 123 123 = .isTrue rfl`
 * `(if (6 : UInt16) = 7 then "yes" else "no") = "no"`
 * `show (7 : UInt16) = 7 by decide`
 -/
UInt16.decEq : (a b : UInt16) → Decidable (a = b)
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_dvd_normEDS_two_mul : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), normEDS b c d k ∣ normEDS b c d (2 * k)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.sup_torsionBySet_ideal_eq_torsionBySet_inf : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (P Q : Ideal R)
  {hc : P ⊔ Q = ⊤}, Submodule.torsionBySet R M ↑P ⊔ Submodule.torsionBySet R M ↑Q = Submodule.torsionBySet R M ↑(P ⊓ Q)
-- Mathlib.LinearAlgebra.TensorAlgebra.Basic
TensorAlgebra.ι_eq_algebraMap_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (x : M)
  (r : R), (TensorAlgebra.ι R) x = (algebraMap R (TensorAlgebra R M)) r ↔ x = 0 ∧ r = 0
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.frequently_atTop' : ∀ {α : Type u_3} [inst : Preorder α] [IsDirectedOrder α] {p : α → Prop} [Nonempty α] [NoMaxOrder α],
  (∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b > a, p b
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.charpoly_nilpotent_tfae : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.Finite R M] [inst_5 : Module.Free R M] [IsNoetherian R M] (φ : Module.End R M),
  [IsNilpotent φ, LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M, ∀ (m : M), ∃ n, (φ ^ n) m = 0,
      (LinearMap.charpoly φ).natTrailingDegree = Module.finrank R M].TFAE
-- Mathlib.Data.ENat.Defs
instTopENat : Top ℕ∞
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.ext : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupNorm E}, (∀ (x : E), p x = q x) → p = q
-- Mathlib.Logic.Function.Iterate
Function.Semiconj.iterate_left : ∀ {α : Type u} {f : α → α} {g : ℕ → α → α},
  (∀ (n : ℕ), Function.Semiconj f (g n) (g (n + 1))) → ∀ (n k : ℕ), Function.Semiconj f^[n] (g k) (g (n + k))
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint and such that `A.toSubalgebra ⊔ B.toSubalgebra = ⊤`,
then any `F`-basis of `A` is also a `B`-basis of `E`.
Note that the condition `A.toSubalgebra ⊔ B.toSubalgebra = ⊤` is equivalent to
`A ⊔ B = ⊤` in many cases, see `IntermediateField.sup_toSubalgebra_of_isAlgebraic_right` and similar
results.
 -/
IntermediateField.LinearDisjoint.basisOfBasisLeft : {F : Type u} →
  {E : Type v} →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          {A B : IntermediateField F E} →
            A.LinearDisjoint ↥B →
              A.toSubalgebra ⊔ B.toSubalgebra = ⊤ → {ι : Type u_1} → Module.Basis ι F ↥A → Module.Basis ι (↥B) E
-- Mathlib.Algebra.Module.FinitePresentation
instFinitePresentationFinsupp : ∀ {R : Type u_1} [inst : Ring R] {ι : Type u_2} [Finite ι], Module.FinitePresentation R (ι →₀ R)
-- Lean.Elab.Tactic.Omega.Frontend
/-- Add an integer equality to the `Problem`.

We solve equalities as they are discovered, as this often results in an earlier contradiction.
 -/
Lean.Elab.Tactic.Omega.MetaProblem.addIntEquality : Lean.Elab.Tactic.Omega.MetaProblem →
  Lean.Expr → Lean.Expr → Lean.Elab.Tactic.Omega.OmegaM Lean.Elab.Tactic.Omega.MetaProblem
-- Mathlib.Data.NNRat.Defs
/-- It sometimes happens that a `@[simp]` lemma declared early in the library can be proved by `simp`
using later, more general simp lemmas. In that case, the following reasons might be arguments for
the early lemma to be tagged `@[simp high]` (rather than `@[simp, nolint simpNF]` or
un-`@[simp]`ed):
1. There is a significant portion of the library which needs the early lemma to be available via
  `simp` and which doesn't have access to the more general lemmas.
2. The more general lemmas have more complicated typeclass assumptions, causing rewrites with them
  to be slower.
 -/
LibraryNote.specialised_high_priority_simp_lemma : Batteries.Util.LibraryNote
-- Mathlib.RingTheory.PowerSeries.GaussNorm
PowerSeries.gaussNorm_add_le_max : ∀ {R : Type u_1} [inst : Semiring R] (v : R → ℝ) (c : ℝ) (f g : PowerSeries R),
  0 ≤ c →
    (∀ (a : R), v a ≥ 0) →
      (∀ (x y : R), v (x + y) ≤ max (v x) (v y)) →
        PowerSeries.HasGaussNorm v c f →
          PowerSeries.HasGaussNorm v c g →
            PowerSeries.gaussNorm v c (f + g) ≤ max (PowerSeries.gaussNorm v c f) (PowerSeries.gaussNorm v c g)
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderConjugate.inv_inv : ∀ {a b : NNReal}, 0 < a → 0 < b → a + b = 1 → a⁻¹.HolderConjugate b⁻¹
-- Mathlib.Topology.Constructions.SumProd
Continuous.uncurry_right : ∀ {X : Type u} {Y : Type v} {Z : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y → Z} (y : Y), Continuous (Function.uncurry f) → Continuous fun a => f a y
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getCast.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a k : α) (v : β k)
  (es : Std.DHashMap.Internal.AssocList α β)
  (h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.AssocList.cons k v es) = true),
  Std.DHashMap.Internal.AssocList.getCast a (Std.DHashMap.Internal.AssocList.cons k v es) h =
    if hka : (k == a) = true then cast ⋯ v else Std.DHashMap.Internal.AssocList.getCast a es ⋯
-- Mathlib.Data.ZMod.Basic
ZMod.intCast_eq_intCast_iff : ∀ (a b : ℤ) (c : ℕ), ↑a = ↑b ↔ a ≡ b [ZMOD ↑c]
-- Lean.Meta.Instances
Lean.Meta.instToFormatInstanceEntry : Std.ToFormat Lean.Meta.InstanceEntry
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.instIsScalarTowerTensorProduct_2 : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B], IsScalarTower S B (TensorProduct R S Ω[A⁄R])
-- Lean.Elab.Do.Basic
/-- Whether the continuation of a `do` element is duplicable. Saying `nonDuplicable` is always safe;
`duplicable` allows for more optimizations.
 -/
Lean.Elab.Do.DoElemContKind : Type
-- Mathlib.Order.Lattice
Function.Injective.semilatticeInf.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Min α] [inst_1 : LE α] [inst_2 : LT α] [inst_3 : SemilatticeInf β] (f : α → β)
  (hf_inj : Function.Injective f) (le : ∀ {x y : α}, f y ≤ f x ↔ y ≤ x) (lt : ∀ {x y : α}, f y < f x ↔ y < x)
  (map_sup : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b),
  Function.Injective.semilatticeInf f hf_inj le lt map_sup =
    { toPartialOrder := Function.Injective.partialOrder f hf_inj ⋯ ⋯, inf := fun a b => a ⊓ b, inf_le_left := ⋯,
      inf_le_right := ⋯, le_inf := ⋯ }
-- Init.Data.Fin.Lemmas
Fin.castLE_mk : ∀ (i n m : ℕ) (hn : i < n) (h : n ≤ m), Fin.castLE h ⟨i, hn⟩ = ⟨i, ⋯⟩
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.mconv_eq_withDensity_mlconvolution_rnDeriv : ∀ {G : Type u_3} [inst : Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {ν₁ ν₂ : MeasureTheory.Measure G}
  [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ],
  ν₁.AbsolutelyContinuous μ →
    ν₂.AbsolutelyContinuous μ →
      ν₁.mconv ν₂ = μ.withDensity (MeasureTheory.mlconvolution (ν₁.rnDeriv μ) (ν₂.rnDeriv μ) μ)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.instReprDecl.repr : {α : Type} → [Repr α] → Std.Sat.AIG.Decl α → ℕ → Std.Format
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.instIsStableUnderShiftLeftOrthogonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) {M : Type u_1}
  [inst_1 : AddGroup M] [inst_2 : CategoryTheory.HasShift C M] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C]
  [P.IsStableUnderShift M], P.leftOrthogonal.IsStableUnderShift M
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.IsIsolated.bot : ∀ {V : Type u} {v : V}, ⊥.IsIsolated v
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.length_pure : ∀ {α : Type u_2} [inst : AddCommGroup α] [inst_1 : PartialOrder α] (a : α), (NonemptyInterval.pure a).length = 0
-- Mathlib.Topology.Baire.Lemmas
/-- Baire theorem: a countable intersection of dense open sets is dense. Formulated here with
an index set which is a countable type.  -/
dense_iInter_of_isOpen : ∀ {X : Type u_1} {ι : Sort u_3} [inst : TopologicalSpace X] [BaireSpace X] [Countable ι] {f : ι → Set X},
  (∀ (i : ι), IsOpen (f i)) → (∀ (i : ι), Dense (f i)) → Dense (⋂ s, f s)
-- Mathlib.Data.Multiset.Interval
Multiset.uIcc_eq : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Multiset α),
  Finset.uIcc s t =
    Finset.map Multiset.equivDFinsupp.symm.toEmbedding (Finset.uIcc (Multiset.toDFinsupp s) (Multiset.toDFinsupp t))
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_mapId_inv_toNatTrans_app : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] (D_1 : CategoryTheory.Cat)
  (x : CategoryTheory.Join (↑D_1) D),
  ((CategoryTheory.Join.pseudofunctorLeft D).mapId D_1).inv.toNatTrans.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)
-- Mathlib.Order.TypeTags
WithTop.recTopCoe.eq_2 : ∀ {α : Type u_1} {C : WithTop α → Sort u_2} (bot : C ⊤) (coe : (a : α) → C ↑a) (a : α),
  WithTop.recTopCoe bot coe (some a) = coe a
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Iic_mul_Iio_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [MulLeftStrictMono α]
  [MulRightStrictMono α] [inst_5 : LocallyFiniteOrderBot α] (a b : α), Finset.Iic a * Finset.Iio b ⊆ Finset.Iio (a * b)
-- Init.Data.Int.Order
Int.zero_lt_neg_iff : ∀ {a : ℤ}, 0 < -a ↔ a < 0
-- Mathlib.Algebra.Group.Defs
/-- Multiplication by a natural number.
Set this to `nsmulRec` unless `Module` diamonds are possible.  -/
NSMul.nsmul : {M : Type u} → [self : NSMul M] → ℕ → M → M
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- Also see `Finset.prod_ite_mem_eq`  -/
Finset.prod_eq_prod_extend : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] (f : ↥s → M),
  ∏ x, f x = ∏ x ∈ s, Function.extend Subtype.val f 1 x
-- Mathlib.CategoryTheory.Abelian.Basic
/-- Suppose `f` and `g` are two morphisms with a common domain and suppose we have written `g` as
an epimorphism followed by a monomorphism. If `f` factors through the epi part of this
factorization, then any pushout of `g` along `f` is a monomorphism.  -/
CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [CategoryTheory.Limits.HasPushouts C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g₁ : X ⟶ W) [CategoryTheory.Epi g₁]
  (g₂ : W ⟶ Z) [CategoryTheory.Mono g₂],
  CategoryTheory.CategoryStruct.comp g₁ g₂ = g →
    ∀ (f' : W ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f' = f →
        ∀ (t : CategoryTheory.Limits.PushoutCocone f g) (ht : CategoryTheory.Limits.IsColimit t),
          CategoryTheory.Mono t.inl
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
ContinuousSup.measurableSup : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] {mγ : MeasurableSpace γ} [BorelSpace γ] [inst_2 : Max γ] [ContinuousSup γ],
  MeasurableSup γ
-- Init.Data.SInt.Lemmas
Int32.toInt_eq_toNatClampNeg : ∀ {a : Int32}, 0 ≤ a → a.toInt = ↑a.toNatClampNeg
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.trans_apply : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (e₁ : M ≃* N)
  (e₂ : N ≃* P) (m : M), (e₁.trans e₂) m = e₂ (e₁ m)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.ofSeq_le_ofSeq : ∀ {f g : ℕ → ℝ}, Hyperreal.ofSeq f ≤ Hyperreal.ofSeq g ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), f n ≤ g n
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_symm_of_mem_maximalAtlas : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) → e ∈ StructureGroupoid.maximalAtlas M G → ChartedSpace.LiftPropOn Q (↑e.symm) e.target
-- Std.Data.TreeSet.Raw.WF
Std.TreeSet.Raw.WF.empty : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.TreeSet.Raw.empty.WF
-- Mathlib.Algebra.Group.Submonoid.Finite
AddSubmonoid.pi_mem_of_single_mem : ∀ {η : Type u_1} {f : η → Type u_2} [inst : (i : η) → AddZeroClass (f i)] {S : Type u_3}
  [inst_1 : SetLike S ((i : η) → f i)] [AddSubmonoidClass S ((i : η) → f i)] [Finite η] [inst_4 : DecidableEq η] {H : S}
  (x : (i : η) → f i), (∀ (i : η), Pi.single i (x i) ∈ H) → x ∈ H