mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
/-- `cyclotomic n R` can be expressed as a product in a fraction field of `R[X]`
using Möbius inversion.  -/
Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius : ∀ {n : ℕ} (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R],
  (algebraMap (Polynomial R) (RatFunc R)) (Polynomial.cyclotomic n R) =
    ∏ i ∈ n.divisorsAntidiagonal,
      (algebraMap (Polynomial R) (RatFunc R)) (Polynomial.X ^ i.2 - 1) ^ ArithmeticFunction.moebius i.1
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.abs_arg_le_pi_div_two_iff : ∀ {z : ℂ}, |z.arg| ≤ Real.pi / 2 ↔ 0 ≤ z.re
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_inv_le_iff_of_pos : ∀ {x y z : ℝ}, 0 ≤ x → 0 ≤ y → 0 < z → (x ^ z⁻¹ ≤ y ↔ x ≤ y ^ z)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instAddSubgroupClass : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G], AddSubgroupClass (OpenAddSubgroup G) G
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RioSlice.instToIterator : {α : Type u_1} →
  [inst : Ord α] →
    Std.ToIterator (Std.Slice (Std.DTreeMap.Internal.Unit.RioSliceData α)) Id
      (Std.Iterators.Types.Map (Std.DTreeMap.Internal.RxoIterator α fun x => Unit) Id Id (fun ⦃x⦄ => monadLift) fun b =>
        pure b.fst)
      α
-- Mathlib.Algebra.CharZero.AddMonoidHom
CharZero.of_addMonoidHom : ∀ {M : Type u_1} {N : Type u_2} [inst : AddCommMonoidWithOne M] [inst_1 : AddCommMonoidWithOne N] [CharZero M]
  (e : M →+ N), e 1 = 1 → Function.Injective ⇑e → CharZero N
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_minKey? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {km : α}, t.minKey? = some km → t.getKey? km = some km
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory_rightUnitor_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (a : B),
  (CategoryTheory.Bicategory.rightUnitor η).inv.as.app a = (CategoryTheory.Bicategory.rightUnitor (η.app a)).inv
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulEquiv.subsemigroupMap_symm_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (S : Subsemigroup M)
  (x : ↥(Subsemigroup.map (↑e) S)), ↑((e.subsemigroupMap S).symm x) = e.symm ↑x
-- Mathlib.Analysis.Normed.Group.Basic
NormedAddGroup.tendsto_nhds_nhds : ∀ {E : Type u_5} {F : Type u_6} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F} {x : E}
  {y : F}, Filter.Tendsto f (nhds x) (nhds y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x' : E), ‖-x' + x‖ < δ → ‖-f x' + y‖ < ε
-- Std.Do.PostCond
/-- Implication of exception assertions is defined as pointwise implication of the assertion for each
exception.

Unlike entailment (`ExceptConds.entails`), which is an ordinary proposition of type `Prop`,
implication of exception assertions is itself an exception assertion.
 -/
Std.Do.«term_→ₑ_» : Lean.TrailingParserDescr
-- Mathlib.RepresentationTheory.Homological.Resolution
Rep.standardComplex.d.eq_1 : ∀ (k : Type u) [inst : CommRing k] (G : Type u) (n : ℕ),
  Rep.standardComplex.d k G n =
    ((Finsupp.lift (MonoidAlgebra k (Fin n → G)) k (Fin (n + 1) → G)) fun g =>
        ∑ p, MonoidAlgebra.single (g ∘ p.succAbove) ((-1) ^ ↑p)) ∘ₗ
      ↑(MonoidAlgebra.coeffLinearEquiv k)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.Deriv
HasStrictDerivAt.map_nhds_eq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {f : 𝕜 → 𝕜} {f' a : 𝕜},
  HasStrictDerivAt f f' a → f' ≠ 0 → Filter.map f (nhds a) = nhds (f a)
-- Init.Control.Lawful.MonadAttach.Lemmas
MonadAttach.attach_bind_eq_pbind : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] {x : m α}
  {f : Subtype (MonadAttach.CanReturn x) → m β}, MonadAttach.attach x >>= f = MonadAttach.pbind x fun a ha => f ⟨a, ha⟩
-- Mathlib.FieldTheory.IsSepClosed
/-- If `k` is separably closed, `K / k` is a field extension, `L / k` is an intermediate field
which is separable, then `L` is equal to `k`. A corollary of `IsSepClosed.algebraMap_surjective`.  -/
IntermediateField.eq_bot_of_isSepClosed_of_isSeparable : ∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [IsSepClosed k] [inst_3 : Algebra k K]
  (L : IntermediateField k K) [Algebra.IsSeparable k ↥L], L = ⊥
-- Mathlib.Order.Filter.Basic
/-- Eta-expanded form of `Filter.EventuallyEq.const_smul` -/
Filter.EventuallyEq.fun_const_smul : ∀ {α : Type u} {β : Type v} {γ : Type u_2} [inst : SMul γ β] {f g : α → β} {l : Filter α},
  f =ᶠ[l] g → ∀ (c : γ), (fun i => c • f i) =ᶠ[l] fun i => c • g i
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_filterMap! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {γ : α → Type w} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} {k : α} [inst_1 : Inhabited (γ k)],
  t.WF → (Std.DTreeMap.Internal.Impl.filterMap! f t).get! k = ((t.get? k).bind (f k)).get!
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- **Alias** of `Set.inv_ofPred`. -/
Set.inv_setOf : ∀ {α : Type u_2} [inst : Inv α] (p : α → Prop), {x | p x}⁻¹ = {x | p x⁻¹}
-- Mathlib.Algebra.Star.Subalgebra
/-- If all elements of `s : Set A` commute pairwise and with elements of `star s`, then `adjoin R s`
is commutative.  -/
StarAlgebra.isMulCommutative_adjoin : ∀ (R : Type u_2) {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {s : Set A},
  (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) →
    (∀ a ∈ s, ∀ b ∈ s, a * star b = star b * a) → IsMulCommutative ↥(StarAlgebra.adjoin R s)
-- Lean.Meta.InferType
/-- Auxiliary function for instantiating the loose bound variables in `e` with `args[start...stop]`.
This function is similar to `instantiateRevRange`, but it applies beta-reduction when
we instantiate a bound variable with a lambda expression.

If `args` contains no lambda expressions, it is equivalent to `instantiateRevRange`, and in fact
it will call `instantiateRevRange` for efficiency.

Example: Given the term `#0 a`, and `start := 0, stop := 1, args := #[fun x => x]` the result is
`a` instead of `(fun x => x) a`.
This reduction is useful when we are inferring the type of eliminator-like applications.
For example, given `(n m : Nat) (f : Nat → Nat) (h : m = n)`,
the type of `Eq.subst (motive := fun x => f m = f x) h rfl`
is `motive n` which is `(fun (x : Nat) => f m = f x) n`.
This function reduces the new application to `f m = f n`.

We use this to implement `inferAppType`.
 -/
Lean.Expr.instantiateBetaRevRange : Lean.Expr → ℕ → ℕ → Array Lean.Expr → Lean.Expr
-- Mathlib.Combinatorics.SimpleGraph.Operations
SimpleGraph.instDecidableRelAdjEdge : {V : Type u_1} → (s t : V) → [DecidableEq V] → DecidableRel (SimpleGraph.edge s t).Adj
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.tensorHom_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  {X₁ Y₁ X₂ Y₂ : CategoryTheory.Arrow C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f g =
    CategoryTheory.CategoryStruct.comp
      ((fun {X₁ X₂} f X => (CategoryTheory.MonoidalCategory.Arrow.pushoutProduct.map f).app X) f X₂)
      ((fun X x x_1 f => (CategoryTheory.MonoidalCategory.Arrow.pushoutProduct.obj X).map f) Y₁ X₂ Y₂ g)
-- Mathlib.Tactic.MkIffOfInductiveProp
/-- `mkAndList [x1, x2, ...]` is defined as `x1 ∧ (x2 ∧ ...)`, or `True` if the list is empty.  -/
Mathlib.Tactic.MkIff.mkAndList : List Lean.Expr → Lean.Expr
-- Mathlib.Topology.EMetricSpace.Basic
EMetric.nontrivial_iff_nontrivialTopology : ∀ {α : Type u_2} [inst : EMetricSpace α], Nontrivial α ↔ NontrivialTopology α
-- Batteries.Tactic.Case
/-- The body of a `case ... | ...` tactic that's a tactic sequence (or hole).  -/
Batteries.Tactic.casePattTac : Lean.ParserDescr
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] (S : AddSubmonoid R) [inst_1 : AddOreLocalization.AddOreSet S] (X : Type u_2)
  [inst_2 : AddAction R X], AddOreLocalization S X = Quotient (AddOreLocalization.oreEqv S X)
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
/-- If `f` only depends on the variables up to rank `a` and `a ≤ b`, integrating `f` against
`partialTraj κ b c` does nothing.  -/
DependsOn.lmarginalPartialTraj_of_le : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} {a b : ℕ}
  {κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))}
  [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (c : ℕ) {f : ((n : ℕ) → X n) → ENNReal},
  Measurable f → DependsOn f ↑(Finset.Iic a) → a ≤ b → ProbabilityTheory.Kernel.lmarginalPartialTraj κ b c f = f
-- Mathlib.Logic.Equiv.Fin.Basic
/-- The equivalence induced by `a ↦ (a / n, a % n)` for nonzero `n`.
This is like `finProdFinEquiv.symm` but with `m` infinite.
See `Nat.div_mod_unique` for a similar propositional statement.  -/
Nat.divModEquiv : (n : ℕ) → [NeZero n] → ℕ ≃ ℕ × Fin n
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso_inv_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C] (X : CategoryTheory.Arrow C)
  {T : C} (t : CategoryTheory.Limits.IsTerminal T) {W : C},
  (CategoryTheory.MonoidalCategory.Arrow.PullbackHom.isTerminalIso X t).inv.right = ⋯.isoPullback.hom
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Commutative rings.
We expect to find a small number of rings in a given goal. Thus, using `Array` is fine here.
 -/
Lean.Meta.Grind.Arith.CommRing.State.rings : Lean.Meta.Grind.Arith.CommRing.State → Array Lean.Meta.Grind.Arith.CommRing.CommRing
-- Mathlib.Probability.Kernel.Defs
/-- A kernel is a Markov kernel if every measure in its image is a probability measure.  -/
ProbabilityTheory.IsMarkovKernel : {α : Type u_1} →
  {β : Type u_2} → {mα : MeasurableSpace α} → {mβ : MeasurableSpace β} → ProbabilityTheory.Kernel α β → Prop
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.all_keys : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [LawfulHashable α] [EquivBEq α] {p : α → Bool}, (↑m).keys.all p = (↑m).all fun a x => p a
-- Mathlib.Order.SuccPred.Basic
WithTop.instSuccOrder.eq_1 : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [inst_2 : (a : α) → Decidable (Order.succ a = a)],
  WithTop.instSuccOrder =
    {
      succ := fun x =>
        match x with
        | none => ⊤
        | some a => if Order.succ a = a then ⊤ else ↑(Order.succ a),
      le_succ := ⋯, max_of_succ_le := ⋯, succ_le_of_lt := ⋯ }
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
map_extChartAt_nhdsWithin_eq_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {s : Set M} [inst_5 : ChartedSpace H M] (x : M),
  Filter.map (↑(extChartAt I x)) (nhdsWithin x s) =
    nhdsWithin (↑(extChartAt I x) x) (↑(extChartAt I x) '' ((extChartAt I x).source ∩ s))
-- Mathlib.RingTheory.QuotSMulTop
/-- The action of the functor `QuotSMulTop r` on morphisms.  -/
QuotSMulTop.map : {R : Type u_2} →
  [inst : CommRing R] →
    (r : R) →
      {M : Type u_1} →
        {M' : Type u_3} →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup M'] →
                [inst_4 : Module R M'] → (M →ₗ[R] M') →ₗ[R] QuotSMulTop r M →ₗ[R] QuotSMulTop r M'
-- Mathlib.MeasureTheory.VectorMeasure.Basic
/-- Non-measurable sets have measure zero  -/
MeasureTheory.VectorMeasure.not_measurable' : ∀ {α : Type u_3} [inst : MeasurableSpace α] {M : Type u_4} [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  (self : MeasureTheory.VectorMeasure α M) ⦃i : Set α⦄, ¬MeasurableSet i → self.measureOf' i = 0
-- Mathlib.FieldTheory.CardinalEmb
_private.Mathlib.FieldTheory.CardinalEmb.0.Field.Emb.Cardinal.«term_⁺» : Lean.TrailingParserDescr
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.findIdx.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) → ((n : ℕ) → motive [] n) → ((a : α) → (l : List α) → (n : ℕ) → motive (a :: l) n) → motive x x_1
-- Init.Data.SInt.Lemmas
Int8.ofInt_mul : ∀ (a b : ℤ), Int8.ofInt (a * b) = Int8.ofInt a * Int8.ofInt b
-- Mathlib.FieldTheory.IsAlgClosed.Classification
/-- Two uncountable algebraically closed fields of characteristic zero are isomorphic
if they have the same cardinality.  -/
IsAlgClosed.ringEquiv_of_equiv_of_charZero : ∀ {K : Type u} {L : Type v} [inst : Field K] [inst_1 : Field L] [IsAlgClosed K] [IsAlgClosed L] [CharZero K]
  [CharZero L], Cardinal.aleph0 < Cardinal.mk K → Nonempty (K ≃ L) → Nonempty (K ≃+* L)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [IsLieAbelian M] (E : LieAlgebra.Extension R M L) {s : L →ₗ[R] E.L},
  Function.LeftInverse ⇑E.proj ⇑s → ∀ (x : E.L) (y : ↥E.proj.ker), ⁅s (E.proj x), y⁆ = ⁅x, y⁆
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGELTδLT_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (a b : ℤ) (X : C),
  (t.truncGELTδLT a b).app X =
    CategoryTheory.CategoryStruct.comp ((t.truncGEδLT a).app ((t.truncLT b).obj X))
      ((CategoryTheory.shiftFunctor C 1).map ((t.truncLT a).map ((t.truncLTι b).app X)))
-- Init.Data.Range.Polymorphic.UInt
UInt16.instLawfulHasSize : Std.Rxc.LawfulHasSize UInt16
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps
/-- Abbreviation for `eqToHom` that accepts points in a topological space  -/
ContinuousMap.Homotopy.hcast : {X : TopCat} → {x₀ x₁ : ↑X} → x₀ = x₁ → (FundamentalGroupoid.fromTop x₀ ⟶ FundamentalGroupoid.fromTop x₁)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTGE_map_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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 : ℤ) {X Y : C} (φ : X ⟶ Y), ((t.triangleLTGE n).map φ).hom₂ = φ
-- Lean.Meta.Tactic.UnifyEq
Lean.Meta.UnifyEqResult : Type
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.mem_sSup_of_mem : ∀ {G : Type u_1} [inst : AddGroup G] {S : Set (AddSubgroup G)} {s : AddSubgroup G},
  s ∈ S → ∀ {x : G}, x ∈ s → x ∈ sSup S
-- Mathlib.GroupTheory.OrderOfElement
IsOfFinAddOrder.nsmul_inj_mod : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G},
  IsOfFinAddOrder x → ∀ {n m : ℕ}, n • x = m • x ↔ n % addOrderOf x = m % addOrderOf x
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.instInhabited : {α : Type u} → {le : α → α → Bool} → Inhabited (Batteries.BinomialHeap α le)
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.exists_subset_restrict_nonpos' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i : Set α},
  MeasurableSet i →
    s i < 0 →
      (¬∀ (n : ℕ),
            ¬MeasureTheory.VectorMeasure.restrict s
                  (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i l) ≤
                MeasureTheory.VectorMeasure.restrict 0
                  (i \ ⋃ l, ⋃ (_ : l < n), MeasureTheory.SignedMeasure.restrictNonposSeq✝ s i l)) →
        ∃ j,
          MeasurableSet j ∧
            j ⊆ i ∧ MeasureTheory.VectorMeasure.restrict s j ≤ MeasureTheory.VectorMeasure.restrict 0 j ∧ s j < 0
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_ofReal_atTop : Filter.Tendsto ENNReal.ofReal Filter.atTop (nhds ⊤)
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.right_bot_eq_right_quot : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), DoubleCoset.Quotient ↑H ↑⊥ = Quotient (QuotientGroup.rightRel H)
-- Mathlib.Algebra.Quandle
Rack.instGroupEnvelGroup : (R : Type u_1) → [inst : Rack R] → Group (Rack.EnvelGroup R)
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
csSup_sub : ∀ {M : Type u_1} [inst : ConditionallyCompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M]
  {s t : Set M}, s.Nonempty → BddAbove s → t.Nonempty → BddBelow t → sSup (s - t) = sSup s - sInf t
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that the tree map is not empty, retrieves the largest key.
 -/
Std.ExtDTreeMap.maxKey : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → t ≠ ∅ → α
-- Mathlib.Order.Filter.TendstoCofinite
Finsupp.mapDomain_tendstoCofinite : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [Filter.TendstoCofinite f], Filter.TendstoCofinite (Finsupp.mapDomain f)
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.forall_mem_support_invtSubmodule_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] [P.IsReduced] (q : Submodule R M),
  (∀ i ∈ b.support, q ∈ Module.End.invtSubmodule ↑(P.reflection i)) ↔
    ∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.reflection i)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.isAddCommutative : ∀ {I : Type u} {f : I → Type v₁} [inst : (i : I) → Add (f i)] [∀ (i : I), IsAddCommutative (f i)],
  IsAddCommutative ((i : I) → f i)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.one_beq_eq_ite : ∀ {b : Bool} {a : BitVec 1}, ((1#1 == a) == b) = (a == bif b then 1#1 else 0#1)
-- Mathlib.Algebra.BigOperators.NatAntidiagonal
Finset.Nat.sum_antidiagonal_succ' : ∀ {N : Type u_2} [inst : AddCommMonoid N] {n : ℕ} {f : ℕ × ℕ → N},
  ∑ p ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), f p =
    f (n + 1, 0) + ∑ p ∈ Finset.HasAntidiagonal.antidiagonal n, f (p.1, p.2 + 1)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.ofSubsingleton_self : ∀ {R : Type u_1} (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Subsingleton M], LinearEquiv.ofSubsingleton M M = LinearEquiv.refl R M
-- Mathlib.Topology.Algebra.MulAction
OrderDual.instContinuousSMul_right : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : SMul M X]
  [ContinuousSMul M X], ContinuousSMul M Xᵒᵈ
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIoo_eq_union : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.uIoo a b = Set.Ioo a b ∪ Set.Ioo b a
-- Mathlib.Combinatorics.Additive.Dissociation
/-- A set is dissociated iff all its finite subsets have different products.

This is an analog of linear independence in a vector space, but with the "scalars" restricted to
`0` and `±1`.  -/
MulDissociated : {α : Type u_1} → [CommGroup α] → Set α → Prop
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosed
/-- A thickened indicator is integrable.  -/
MeasureTheory.integrable_thickenedIndicator : ∀ {Ω : Type u_2} {mΩ : MeasurableSpace Ω} [inst : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] (F : Set Ω) {δ : ℝ} (δ_pos : 0 < δ),
  MeasureTheory.Integrable (fun ω => ↑((thickenedIndicator δ_pos F) ω)) μ
-- Std.Do.Triple.SpecLemmas
_private.Std.Do.Triple.SpecLemmas.0.Std.Do.PredTrans.pushExcept.match_1.eq_1 : ∀ {α ε : Type u_1} (motive : Except ε α → Sort u_2) (a : α) (h_1 : (a : α) → motive (Except.ok a))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.ok a with
    | Except.ok a => h_1 a
    | Except.error e => h_2 e) =
    h_1 a
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.empty : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X}, Convexity.IsStarConvexSet R x ∅
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_pow : ∀ {m : Type u_1} [inst : DecidableEq m] [inst_1 : Fintype m] {R : Type v} [inst_2 : CommRing R] (M : Matrix m m R)
  (n : ℕ), (M ^ n).det = M.det ^ n
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.instIsFiniteTypeOfIsFinitePresentation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] (M : SheafOfModules R)
  [M.IsFinitePresentation], M.IsFiniteType
-- Mathlib.RingTheory.Etale.Basic
/-- An `R`-algebra `A` is formally etale iff "for every `R`-algebra `B`,
every square-zero ideal `I : Ideal B` and `f : A →ₐ[R] B ⧸ I`, there exists
a unique lift `A →ₐ[R] B`".
 -/
Algebra.FormallyEtale.iff_comp_bijective : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallyEtale R A ↔
    ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp
-- Mathlib.Algebra.Group.Prod
Prod.isUnit_iff : ∀ {M : Type u_3} {N : Type u_4} [inst : Monoid M] [inst_1 : Monoid N] {x : M × N}, IsUnit x ↔ IsUnit x.1 ∧ IsUnit x.2
-- Mathlib.Lean.Meta.RefinedDiscrTree.Lookup
_private.Mathlib.Lean.Meta.RefinedDiscrTree.Lookup.0.Lean.Meta.RefinedDiscrTree.PartialMatch.mk.inj : ∀ {keys : List Lean.Meta.RefinedDiscrTree.Key} {score : ℕ} {trie : Lean.Meta.RefinedDiscrTree.TrieIndex}
  {treeStars : Std.HashMap ℕ (List Lean.Meta.RefinedDiscrTree.Key)} {keys_1 : List Lean.Meta.RefinedDiscrTree.Key}
  {score_1 : ℕ} {trie_1 : Lean.Meta.RefinedDiscrTree.TrieIndex}
  {treeStars_1 : Std.HashMap ℕ (List Lean.Meta.RefinedDiscrTree.Key)},
  { keys := keys, score := score, trie := trie, treeStars := treeStars } =
      { keys := keys_1, score := score_1, trie := trie_1, treeStars := treeStars_1 } →
    keys = keys_1 ∧ score = score_1 ∧ trie = trie_1 ∧ treeStars = treeStars_1
-- Mathlib.Topology.JacobsonSpace
closure_closedPoints : ∀ {X : Type u_1} [inst : TopologicalSpace X] [JacobsonSpace X], closure (closedPoints X) = Set.univ
-- Mathlib.Algebra.Category.ModuleCat.Images
/-- The categorical image of a morphism in `ModuleCat R` agrees with the linear algebraic range.  -/
ModuleCat.imageIsoRange : {R : Type u} →
  [inst : Ring R] →
    {G H : ModuleCat R} → (f : G ⟶ H) → CategoryTheory.Limits.image f ≅ ModuleCat.of R ↥(ModuleCat.Hom.hom f).range
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_revPerm_Ioc : ∀ {n : ℕ} (i j : Fin n), Finset.map (Equiv.toEmbedding Fin.revPerm) (Finset.Ioc i j) = Finset.Ico j.rev i.rev
-- Lean.Meta.Tactic.Simp.Main
/-- Return true if `e` is of the form `Char.ofNat n` where `n` is a kernel Nat literals.  -/
Lean.Meta.Simp.isCharLit : Lean.Expr → Bool