mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsAtom.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (K : ℝ) (S A : Finset G),
  Finset.IsAtom✝ K S A = MinimalFor (Finset.IsFragment✝ K S) Finset.card A
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_iff_exists_eventuallyEq : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {f : α → β} [Nonempty β],
  Filter.EventuallyConst f l ↔ ∃ c, f =ᶠ[l] fun x => c
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
/-- The morphism `ιIteration I κ` is a transfinite composition of shape
`κ.ord.ToType` of morphisms satisfying `(succStruct I κ).prop`.  -/
CategoryTheory.SmallObject.transfiniteCompositionOfShapeSuccStructPropιIteration : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (I : CategoryTheory.MorphismProperty C) →
      (κ : Cardinal.{w}) →
        [inst_1 : Fact κ.IsRegular] →
          [inst_2 : OrderBot κ.ord.ToType] →
            [inst_3 : I.IsCardinalForSmallObjectArgument κ] →
              (CategoryTheory.SmallObject.succStruct I κ).prop.TransfiniteCompositionOfShape κ.ord.ToType
                (CategoryTheory.SmallObject.ιIteration I κ)
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.DTreeMap.getEntryGE! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited (Sigma β)] → Std.DTreeMap α β cmp → α → (a : α) × β a
-- Init.Data.Fin.Lemmas
Fin.add_one_lt_iff : ∀ {n : ℕ} {k : Fin (n + 2)}, k + 1 < k ↔ k = Fin.last (n + 1)
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.InitializationOptions.mk : Option Bool → Option Lean.Lsp.LogConfig → Lean.Lsp.InitializationOptions
-- Lean.Syntax
/-- Check for a `Syntax.ident` of the given name anywhere in the tree.
This is usually a bad idea since it does not check for shadowing bindings,
but in the delaborator we assume that bindings are never shadowed.
 -/
Lean.Syntax.hasIdent : Lean.Name → Lean.Syntax → Bool
-- Init.Data.SInt.Lemmas
Int16.succ_mul : ∀ {a b : Int16}, (a + 1) * b = a * b + b
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.tsum_eq_zero_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [CanonicallyOrderedAdd α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  Summable f → (∑' (i : ι), f i = 0 ↔ ∀ (x : ι), f x = 0)
-- Mathlib.Order.KrullDimension
Order.krullDim_orderDual : ∀ {α : Type u_1} [inst : Preorder α], Order.krullDim αᵒᵈ = Order.krullDim α
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The (exact) short complex attached to the kernel fork `kf`.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            CategoryTheory.Abelian.SpectralObject C ι →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq' : κ) →
                            κ →
                              (i₀' i₀ i₁ i₂ i₃ : ι) →
                                i₀' = data.i₀ r' pq' ⋯ →
                                  i₀ = data.i₀ r pq' ⋯ →
                                    i₁ = data.i₁ pq' →
                                      i₂ = data.i₂ pq' →
                                        i₃ = data.i₃ r pq' ⋯ →
                                          (n₀ n₁ n₂ : ℤ) →
                                            n₁ = data.deg pq' →
                                              autoParam (n₀ + 1 = n₁)
                                                  CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_1 →
                                                autoParam (n₁ + 1 = n₂)
                                                    CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.kfSc._auto_3 →
                                                  CategoryTheory.ShortComplex C
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- If `f` is a nonarchimedean additive group seminorm on `α` and `x y : α` are such that
`f x ≠ f y`, then `f (x + y) = max (f x) (f y)`.  -/
IsNonarchimedean.add_eq_max_of_ne : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] {F : Type u_2} {α : Type u_3} [inst_2 : AddGroup α]
  [inst_3 : FunLike F α R] [AddGroupSeminormClass F α R] {f : F},
  IsNonarchimedean ⇑f → ∀ {x y : α}, f x ≠ f y → f (x + y) = max (f x) (f y)
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.dart_fst_mem_support_of_mem_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {d : G.Dart}, d ∈ p.darts → d.toProd.1 ∈ p.support
-- Mathlib.AlgebraicGeometry.Cover.Open
/-- Given any open cover `𝓤`, this is an affine open cover which refines it.
The morphism in the category of open covers which proves that this is indeed a refinement, see
`AlgebraicGeometry.Scheme.OpenCover.fromAffineRefinement`.
 -/
AlgebraicGeometry.Scheme.OpenCover.affineRefinement : {X : AlgebraicGeometry.Scheme} → X.OpenCover → X.AffineOpenCover
-- Init.Control.Except
/-- Transforms exceptions using the function `f`.

This is the `ExceptT` version of `Except.mapError`.
 -/
ExceptT.adapt : {ε : Type u} → {m : Type u → Type v} → [Monad m] → {ε' α : Type u} → (ε → ε') → ExceptT ε m α → ExceptT ε' m α
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.success.injEq : ∀ (a a_1 : Array LeanSearchClient.SearchResult),
  (LeanSearchClient.LoogleResult.success a = LeanSearchClient.LoogleResult.success a_1) = (a = a_1)
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.prodRight_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] (B : Type u_6)
  (C : Type u_7) [inst_7 : Semiring B] [inst_8 : Semiring C] [inst_9 : Algebra R B] [inst_10 : Algebra R C] (a : A)
  (x : B × C), (Algebra.TensorProduct.prodRight R S A B C) (a ⊗ₜ[R] x) = (a ⊗ₜ[R] x.1, a ⊗ₜ[R] x.2)
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.instSubsingletonElemForall : ∀ {S : Type u_1} [inst : Semiring S] [inst_1 : PartialOrder S] {X : Type u_2} [inst_2 : Fintype X] [Subsingleton X],
  Subsingleton ↑(stdSimplex S X)
-- Mathlib.Order.BoundedOrder.Basic
OrderTop.instSubsingleton : ∀ {α : Type u} [inst : PartialOrder α], Subsingleton (OrderTop α)
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.intValuation_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {r : R} (v : IsDedekindDomain.HeightOneSpectrum R),
  v.intValuation r = v.intValuationDef r
-- Init.Notation
/-- `#reduce <expression>` reduces the expression `<expression>` to its normal form. This
involves applying reduction rules until no further reduction is possible.

By default, proofs and types within the expression are not reduced. Use modifiers
`(proofs := true)`  and `(types := true)` to reduce them.
Recall that propositions are types in Lean.

**Warning:** This can be a computationally expensive operation,
especially for complex expressions.

Consider using `#eval <expression>` for simple evaluation/execution
of expressions.
 -/
Lean.reduceCmd : Lean.ParserDescr
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.Context : (Type → Type) → Type
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.uniformSpace_eq_bot : ∀ {α : Type ua} {u : UniformSpace α}, u = ⊥ ↔ SetRel.id ∈ uniformity α
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.ext_iff : ∀ {p n : ℕ} {R : Type u_1} {x y : TruncatedWittVector p n R},
  x = y ↔ ∀ (i : Fin n), TruncatedWittVector.coeff i x = TruncatedWittVector.coeff i y
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.equivListRowLens_apply_coe : ∀ (μ : YoungDiagram), ↑(YoungDiagram.equivListRowLens μ) = μ.rowLens
-- Mathlib.NumberTheory.Modular
/-- First Fundamental Domain Lemma: Any `z : ℍ` can be moved to `𝒟` by an element of
`SL(2,ℤ)`  -/
ModularGroup.exists_smul_mem_fd : ∀ (z : UpperHalfPlane), ∃ g, g • z ∈ ModularGroup.fd
-- Mathlib.Data.Num.Lemmas
Num.zneg_toZNumNeg : ∀ (n : Num), -n.toZNumNeg = n.toZNum
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the left whiskering `f ◁ η`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.whiskerLeftM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂ → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.CategoryTheory.Comma.Arrow
/-- Given `X : Arrow T`, this is the morphism `X.left ⟶ X.right`.  -/
CategoryTheory.Arrow.hom : {T : Type u} → [inst : CategoryTheory.Category.{v, u} T] → (X : CategoryTheory.Arrow T) → X.left ⟶ X.right
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.coconeOfIsLeftKanExtension_pt : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] (c : CategoryTheory.Limits.Cocone F),
  (F'.coconeOfIsLeftKanExtension α c).pt = c.pt
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixedPoints_fixingSubgroup : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (F : IntermediateField K L) [hGKL : IsGaloisGroup G K L]
  [Finite G], FixedPoints.intermediateField ↥(fixingSubgroup G ↑F) = F
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.alter_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β},
  Std.ExtDHashMap.Const.alter m k f = ∅ ↔ (m = ∅ ∨ m.size = 1 ∧ k ∈ m) ∧ f (Std.ExtDHashMap.Const.get? m k) = none
-- Mathlib.Data.ENNReal.Inv
ENNReal.div_pos_iff : ∀ {a b : ENNReal}, 0 < a / b ↔ a ≠ 0 ∧ b ≠ ⊤
-- Batteries.Data.List.Count
List.idxToSigmaCount.congr_simp : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : ReflBEq α] (xs : List α) (i i_1 : Fin xs.length),
  i = i_1 → xs.idxToSigmaCount i = xs.idxToSigmaCount i_1
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegalCore.spineToSimplex_succ : ∀ {X : SSet} (h : (n : ℕ) → X.StrictSegalCore n) {n : ℕ} (p : X.Path (n + 1)),
  SSet.StrictSegalCore.spineToSimplex h p =
    (h n).concat (p.arrow 0) (SSet.StrictSegalCore.spineToSimplex h (p.interval 1 n ⋯)) ⋯
-- Mathlib.Order.Filter.SmallSets
Filter.HasBasis.smallSets : ∀ {α : Type u_1} {ι : Sort u_3} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → l.smallSets.HasBasis p fun i => 𝒫 s i
-- Mathlib.LinearAlgebra.FreeModule.PID
Module.free_of_finite_type_torsion_free' : ∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [IsPrincipalIdealRing R] [IsDomain R] [Module.Finite R M] [Module.IsTorsionFree R M], Module.Free R M
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- Construct a subgroup from a nonempty set that is closed under subtraction  -/
AddSubgroup.ofSub : {G : Type u_1} → [inst : AddGroup G] → (s : Set G) → s.Nonempty → (∀ x ∈ s, ∀ y ∈ s, x + -y ∈ s) → AddSubgroup G
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.HasAntitoneBasis.comp_strictMono : ∀ {α : Type u_3} {l : Filter α} {s : ℕ → Set α},
  l.HasAntitoneBasis s → ∀ {φ : ℕ → ℕ}, StrictMono φ → l.HasAntitoneBasis (s ∘ φ)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSliceData.treeMap : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RicSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E}, MeromorphicAt f x → MeromorphicAt (-f) x
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normal_inf_normal : ∀ {G : Type u_1} [inst : Group G] (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal], (H ⊓ K).Normal
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.toRingHom_mapAlgHom : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} (M : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Monoid M] (f : A →ₐ[R] B),
  ↑(MonoidAlgebra.mapAlgHom M f) = MonoidAlgebra.mapRingHom M f.toRingHom
-- Mathlib.RingTheory.Support
IsLocalizedModule.exists_subsingleton_away : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  {M' : Type u_5} [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] (l : M →ₗ[R] M') (p : Ideal R) [inst_6 : p.IsPrime]
  [IsLocalizedModule p.primeCompl l] [Subsingleton M'], ∃ f ∉ p, Subsingleton (LocalizedModule.Away f M)
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.mkCoinductiveAux₁.eq_def : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {P Q : CochainComplex V ℕ} (e : P ⟶ Q) (zero : P.X 1 ⟶ Q.X 0) (one : P.X 2 ⟶ Q.X 1)
  (comm_one :
    e.f 1 = CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) + CategoryTheory.CategoryStruct.comp (P.d 1 2) one)
  (succ :
    (n : ℕ) →
      (p :
          (f : P.X (n + 1) ⟶ Q.X n) ×'
            (f' : P.X (n + 2) ⟶ Q.X (n + 1)) ×'
              e.f (n + 1) =
                CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) +
                  CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f') →
        (f'' : P.X (n + 3) ⟶ Q.X (n + 2)) ×'
          e.f (n + 2) =
            CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) +
              CategoryTheory.CategoryStruct.comp (P.d (n + 2) (n + 3)) f'')
  (x : ℕ),
  Homotopy.mkCoinductiveAux₁ e zero one comm_one succ x =
    match x with
    | 0 => ⟨zero, ⟨one, comm_one⟩⟩
    | 1 => ⟨one, ⟨(succ 0 ⟨zero, ⟨one, comm_one⟩⟩).fst, ⋯⟩⟩
    | n.succ.succ =>
      ⟨(Homotopy.mkCoinductiveAux₁ e zero one comm_one succ (n + 1)).snd.fst,
        ⟨(succ (n + 1) (Homotopy.mkCoinductiveAux₁ e zero one comm_one succ (n + 1))).fst, ⋯⟩⟩
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.IsTorsionQuot.mono_left : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} {I J K : Ideal A},
  I ≤ J → F.IsTorsionQuot I K → F.IsTorsionQuot J K
-- Mathlib.Combinatorics.Graph.Simple
/-- Construct a simple graph from a graph.  -/
Graph.toSimpleGraph : {α : Type u_1} → {β : Type u_2} → (G : Graph α β) → SimpleGraph ↑G.vertexSet
-- Init.System.IO
/-- Creates an IO action that will invoke `fn` if and when it is executed, returning the result.
 -/
IO.lazyPure : {α : Type} → (Unit → α) → IO α
-- Mathlib.Order.Monotone.Basic
/-- If `α` is a nonempty preorder with no minimal or maximal elements, then there exists a strictly
antitone function `f : ℤ → α`.  -/
Int.exists_strictAnti : ∀ (α : Type u) [inst : Preorder α] [Nonempty α] [NoMinOrder α] [NoMaxOrder α], ∃ f, StrictAnti f
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- The continuous semilinear map obtained by applying a continuous semilinear map at a given
vector.

This is the continuous version of `LinearMap.applyₗ`.  -/
ContinuousLinearMap.apply : (𝕜 : Type u_1) →
  {E : Type u_4} →
    (Fₗ : Type u_7) →
      [inst : SeminormedAddCommGroup E] →
        [inst_1 : SeminormedAddCommGroup Fₗ] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 E] → [inst_4 : NormedSpace 𝕜 Fₗ] → E →L[𝕜] (E →L[𝕜] Fₗ) →L[𝕜] Fₗ
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.ext : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  {f g : Convexity.ConvexSpace.AffineMap R X Y}, ⇑f = ⇑g → f = g
-- Mathlib.Order.Filter.Pointwise
Filter.NeBot.of_vadd_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {f : Filter α} {g : Filter β}, (f +ᵥ g).NeBot → g.NeBot
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.id_apply : ∀ {α : Type u_2} [inst : NonAssocSemiring α] [inst_1 : Preorder α] (a : α), (OrderRingHom.id α) a = a
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.map_addU : ∀ {F : Type u} {K : Type v} [inst : Field F] [inst_1 : Field K] (f : F →+* K) (P Q : Fin 3 → F),
  WeierstrassCurve.Jacobian.addU (⇑f ∘ P) (⇑f ∘ Q) = f (WeierstrassCurve.Jacobian.addU P Q)
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go.match_1.splitter : (motive : Lean.Level → Lean.Level → Sort u_1) →
  (u v : Lean.Level) →
    ((x : Lean.Level) → motive x Lean.Level.zero) →
      ((u v₁ v₂ : Lean.Level) → motive u (v₁.max v₂)) →
        ((u₁ u₂ v : Lean.Level) →
            (v = Lean.Level.zero → False) → (∀ (v₁ v₂ : Lean.Level), v = v₁.max v₂ → False) → motive (u₁.max u₂) v) →
          ((a u₂ v : Lean.Level) →
              (v = Lean.Level.zero → False) → (∀ (v₁ v₂ : Lean.Level), v = v₁.max v₂ → False) → motive (a.imax u₂) v) →
            ((u v : Lean.Level) → motive u.succ v.succ) →
              ((x x_1 : Lean.Level) →
                  (x_1 = Lean.Level.zero → False) →
                    (∀ (v₁ v₂ : Lean.Level), x_1 = v₁.max v₂ → False) →
                      (∀ (u₁ u₂ : Lean.Level), x = u₁.max u₂ → False) →
                        (∀ (a u₂ : Lean.Level), x = a.imax u₂ → False) →
                          (∀ (u v : Lean.Level), x = u.succ → x_1 = v.succ → False) → motive x x_1) →
                motive u v
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.isInducing_toContinuousMap : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B], Topology.IsInducing ContinuousAddMonoidHom.toContinuousMap
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β}, List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (t.insertMany l)[k']? = some v
-- Mathlib.Algebra.MonoidAlgebra.Division
/-- **Alias** of `AddMonoidAlgebra.support_coeff_divOf`. -/
AddMonoidAlgebra.support_divOf : ∀ {k : Type u_1} {G : Type u_2} [inst : Semiring k] [inst_1 : AddCommMonoid G] [inst_2 : IsCancelAdd G] (g : G)
  (x : AddMonoidAlgebra k G), (x.divOf g).coeff.support = x.coeff.support.preimage (fun x => g + x) ⋯
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
Unitization.val_inv_unitsFstOne_mulEquiv_quasiregular_symm_apply_coe : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (x : (PreQuasiregular A)ˣ),
  ↑(↑((Unitization.unitsFstOne_mulEquiv_quasiregular R).symm x))⁻¹ = 1 + ↑(PreQuasiregular.equiv.symm ↑x⁻¹)
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.insertMany.eq_1 : ∀ {α : Type u} {β : Type v} {ρ : Type w} [inst : ForIn Id ρ (α × β)] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => β) (l : ρ),
  Std.DHashMap.Internal.Raw₀.Const.insertMany m l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun x __s =>
            let r := __s;
            match x with
            | (a, b) =>
              have r := ⟨(↑r).insert a b, ⋯⟩;
              pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => β) → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => β} {a : α} {b : β}, P m'' → P (m''.insert a b)) →
              P m → P m' } :=
        __s
      pure r).run
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.biUnionPrepartition_tag : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J),
  (π.biUnionPrepartition πi).tag = fun J => π.tag (π.biUnionIndex πi J)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.floor_zero : ⌊0⌋ₑ = 0
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft_obj_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E), ((CategoryTheory.Functor.whiskeringLeft C D E).obj F).obj G = F.comp G
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEquiv_functor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} (e : β ≃ γ),
  (CategoryTheory.GradedObject.comapEquiv C e).functor = CategoryTheory.GradedObject.comap C ⇑e.symm
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- `seminormFromBounded' f` preserves `0`.  -/
seminormFromBounded_zero : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ}, f 0 = 0 → seminormFromBounded' f 0 = 0
-- Mathlib.Topology.Sets.VietorisTopology
TopologicalSpace.vietoris.instCompactSpaceSet : ∀ {α : Type u_1} [inst : TopologicalSpace α] [CompactSpace α], CompactSpace (Set α)
-- Lean.Meta.Sym.Arith.Poly
_private.Lean.Meta.Sym.Arith.Poly.0.Lean.Grind.CommRing.Poly.maxDegreeOf.go : Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Poly → ℕ → ℕ
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.injective_comp_of_pairwise_adj : ∀ {V : Type u} {G : SimpleGraph V} {ι : Type u_1} {α : Type u_2} (C : G.Coloring α) (f : ι → V),
  (Pairwise fun i j => G.Adj (f i) (f j)) → Function.Injective (⇑C ∘ f)
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {D : Type u'} {inst_1 : CategoryTheory.Category.{v', u'} D}
  {F G : CategoryTheory.Functor C D} {A : CategoryTheory.Functor C (Type w)} {x y : F.HomObj G A}, x = y ↔ x.app = y.app
-- Mathlib.Topology.Defs.Filter
/-- Notation for the filter of punctured right neighborhoods of a point.  -/
Topology.nhdsGT : Lean.ParserDescr
-- Mathlib.CategoryTheory.Presentable.Presheaf
CategoryTheory.Presheaf.instIsCardinalLocallyPresentableFunctorOppositeOfHasPullbacks : ∀ {A : Type u'} [inst : CategoryTheory.Category.{v', u'} A] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.IsCardinalLocallyPresentable A κ] [CategoryTheory.Limits.HasPullbacks A] (C : Type w)
  [inst_4 : CategoryTheory.SmallCategory C],
  CategoryTheory.IsCardinalLocallyPresentable (CategoryTheory.Functor Cᵒᵖ A) κ
-- Init.Data.Float.Model.Format.Basic
/-- The position of the most significant digit, where the unit digit corresponds to `1`.
So, for example, `1.0b` has total exponent `1`, `0.1b` has total exponent `0`,
`0.01b` has total exponent `-1`, and so on.
 -/
Float.Model.totalExponent : ℕ → ℤ → ℤ
-- Mathlib.Data.Finsupp.ToDFinsupp
DFinsupp.toFinsupp_zero : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Zero M] [inst_2 : (m : M) → Decidable (m ≠ 0)],
  DFinsupp.toFinsupp 0 = 0
-- Mathlib.FieldTheory.IntermediateField.Algebraic
IntermediateField.rank_eq_rank_subalgebra : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L),
  Module.rank K ↥F.toSubalgebra = Module.rank K ↥F