mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.NFA
NFA.acceptsFrom.eq_1 : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ), M.acceptsFrom S = {x | ∃ s ∈ M.accept, s ∈ M.evalFrom S x}
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.FunctorToTypes.map_comp_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z) (a : F.obj X),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.CategoryStruct.comp f g))) a =
    (CategoryTheory.ConcreteCategory.hom (F.map g)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) a)
-- Mathlib.Algebra.Algebra.Tower
IsScalarTower.of_algHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B), IsScalarTower R A B
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.support_eq_empty : ∀ {X : Type u_1} {a : FreeAbelianGroup X}, a.support = ∅ ↔ a = 0
-- Lean.Meta.Basic
/-- Set `mvarId` kind in the current metavariable context.
 -/
Lean.MVarId.setKind : Lean.MVarId → Lean.MetavarKind → Lean.MetaM Unit
-- Mathlib.Algebra.Ring.Defs
/-- A commutative ring is a ring with commutative multiplication.  -/
CommRing : Type u → Type u
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic_neg_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] (v : ↑(Metric.sphere 0 1)),
  ↑(stereographic ⋯) v = 0
-- Mathlib.Data.Multiset.Bind
Multiset.join_zero : ∀ {α : Type u_1}, Multiset.join 0 = 0
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that such a mapping exists, retrieves the largest key that is
less than or equal to the given key.
 -/
Std.ExtDTreeMap.getKeyLE : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → (k : α) → (∃ a ∈ t, (cmp a k).isLE = true) → α
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.instIsTriangularizableSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra'Forall : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] {b : P.Base} [inst_6 : Finite ι] [inst_7 : IsDomain R] [inst_8 : CharZero R]
  [inst_9 : DecidableEq ι] [inst_10 : Fintype ι],
  LieModule.IsTriangularizable R (↥(RootPairing.GeckConstruction.cartanSubalgebra' b)) (↥b.support ⊕ ι → R)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.minpolyGen_monic : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S),
  pb.minpolyGen.Monic
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.tensorKerInv.congr_simp : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f : N →ₗ[R] P) [inst_11 : Module.Flat R M], LinearMap.tensorKerInv S M f = LinearMap.tensorKerInv S M f
-- Lean.Server.CodeActions.Provider
/-- The nearest enclosing tactic is a tactic, with the given syntax stack.  -/
Lean.CodeAction.FindTacticResult.tactic : Lean.Syntax.Stack → Lean.CodeAction.FindTacticResult
-- Plausible.Gen
/-- Generate a random permutation of a given list.  -/
Plausible.Gen.permutationOf : {α : Type u} → (xs : List α) → Plausible.Gen { ys // xs.Perm ys }
-- Mathlib.Data.Finset.Lattice.Prod
Finset.sup'_inf_sup' : ∀ {α : Type u_2} {ι : Type u_5} {κ : Type u_6} [inst : DistribLattice α] {s : Finset ι} {t : Finset κ} (hs : s.Nonempty)
  (ht : t.Nonempty) (f : ι → α) (g : κ → α), s.sup' hs f ⊓ t.sup' ht g = (s ×ˢ t).sup' ⋯ fun i => f i.1 ⊓ g i.2
-- Init.Data.OfScientific.Basic
/-- Produces a value from the given mantissa, exponent sign, and decimal exponent. For the exponent
sign, `true` indicates a negative exponent.

 Examples:
 - `1.23` is syntax for `OfScientific.ofScientific (nat_lit 123) true (nat_lit 2)`
 - `121e100` is syntax for `OfScientific.ofScientific (nat_lit 121) false (nat_lit 100)`

 Note the use of `nat_lit`; there is no wrapping `OfNat.ofNat` in the resulting term.
 -/
OfScientific.ofScientific : {α : Type u} → [self : OfScientific α] → ℕ → Bool → ℕ → α
-- Init.Data.UInt.Basic
instShiftRightUInt32 : ShiftRight UInt32
-- Mathlib.Probability.Kernel.Invariance
/-- Reversibility (detailed balance) of a Markov kernel `κ` w.r.t. a measure `π`:
for all measurable sets `A B`, the mass flowing from `A` to `B` equals that from `B` to `A`.  -/
ProbabilityTheory.Kernel.IsReversible : {α : Type u_1} → {mα : MeasurableSpace α} → ProbabilityTheory.Kernel α α → MeasureTheory.Measure α → Prop
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.of_append_right : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w}, (p.append q).IsTrail → q.IsTrail
-- Mathlib.CategoryTheory.Monoidal.Subcategory
CategoryTheory.ObjectProperty.leftUnitor_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsMonoidal] (X : P.FullSubcategory),
  CategoryTheory.MonoidalCategoryStruct.leftUnitor X = P.isoMk (CategoryTheory.MonoidalCategoryStruct.leftUnitor X.obj)
-- Mathlib.MeasureTheory.Function.Piecewise
IndexedPartition.aestronglyMeasurable_piecewise : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {s : ι → Set α} {f : ι → α → β}
  {μ : MeasureTheory.Measure α} [Countable ι] (hs : IndexedPartition s),
  (∀ (i : ι), MeasurableSet (s i)) →
    ∀ [inst_2 : TopologicalSpace β],
      (∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.AEStronglyMeasurable (hs.piecewise f) μ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.succ_le_simplex_fst_iff : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d} {l : Fin d},
  SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ →
    ∀ (i : Fin (d + 1)), k.succ ≤ (x.cast hd).simplex.1 i ↔ l.succ ≤ i
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.mem_vadd_finset : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α} {x : β},
  x ∈ a +ᵥ s ↔ ∃ y ∈ s, a +ᵥ y = x
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip
Std.IterM.zip_eq_intermediateZip : ∀ {α₁ α₂ β₁ β₂ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α₁ m β₁] (it₁ : Std.IterM m β₁)
  (it₂ : Std.IterM m β₂), it₁.zip it₂ = Std.IterM.Intermediate.zip it₁ none it₂
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.isApplicable : Lean.Elab.Term.MutualClosure.Replacement → Lean.Expr → Bool
-- Mathlib.Topology.Constructions
/-- **Alias** of `Pi.induced_domRestrict_sUnion`. -/
Pi.induced_restrict_sUnion : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (𝔖 : Set (Set ι)),
  TopologicalSpace.induced (⋃₀ 𝔖).domRestrict Pi.topologicalSpace =
    ⨅ S ∈ 𝔖, TopologicalSpace.induced S.domRestrict Pi.topologicalSpace
-- Mathlib.CategoryTheory.Subobject.WellPowered
/-- Being well-powered is preserved by equivalences.  -/
CategoryTheory.wellPowered_congr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) [inst_2 : CategoryTheory.LocallySmall.{w, v, u₁} C] [inst_3 : CategoryTheory.LocallySmall.{w, v₂, u₂} D],
  CategoryTheory.WellPowered.{w, v, u₁} C ↔ CategoryTheory.WellPowered.{w, v₂, u₂} D
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.constVAdd_apply : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [inst_3 : IsIsometricVAdd G X] (c : G) (x : X), (IsometryEquiv.constVAdd c) x = c +ᵥ x
-- Batteries.CodeAction.Attr
Batteries.CodeAction.mkTacticSeqCodeAction.unsafe_impl_2 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Batteries.CodeAction.TacticSeqCodeAction
-- Mathlib.MeasureTheory.Measure.AddContent
/-- If an `AddContent` is σ-subadditive on a semi-ring of sets, then it is σ-additive.  -/
MeasureTheory.addContent_iUnion_eq_tsum_of_disjoint_of_addContent_iUnion_le : ∀ {α : Type u_1} {C : Set (Set α)} {m : MeasureTheory.AddContent ENNReal C},
  MeasureTheory.IsSetSemiring C →
    (∀ (f : ℕ → Set α),
        (∀ (i : ℕ), f i ∈ C) →
          ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) ≤ ∑' (i : ℕ), m (f i)) →
      ∀ (f : ℕ → Set α),
        (∀ (i : ℕ), f i ∈ C) → ⋃ i, f i ∈ C → Pairwise (Function.onFun Disjoint f) → m (⋃ i, f i) = ∑' (i : ℕ), m (f i)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_preimage_le : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (f : R →+* S) (s : Set S),
  Subring.closure (⇑f ⁻¹' s) ≤ Subring.comap f (Subring.closure s)
-- Lean.Meta.Tactic.Simp.Types
/-- "Compose" the two given simplification procedures. We use the following semantics.
- If `f` produces `done` or `visit`, then return `f`'s result.
- If `f` produces `continue`, then apply `g` to new expression returned by `f`.

See `Simp.Step` type.
 -/
Lean.Meta.Simp.andThen : Lean.Meta.Simp.Simproc → Lean.Meta.Simp.Simproc → Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Group.End
Equiv.Perm.subtypePerm_mul : ∀ {α : Type u_4} {p : α → Prop} (f g : Equiv.Perm α) (hf : ∀ (x : α), p (f x) ↔ p x) (hg : ∀ (x : α), p (g x) ↔ p x),
  f.subtypePerm hf * g.subtypePerm hg = (f * g).subtypePerm ⋯
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- `LinearMap.inr` as an isometry.  -/
QuadraticMap.Isometry.inr : {R : Type u_2} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {P : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R P] → (Q₁ : QuadraticMap R M₁ P) → (Q₂ : QuadraticMap R M₂ P) → Q₂ →qᵢ Q₁.prod Q₂
-- Mathlib.Data.ENat.Basic
ENat.natCast_lt_of_coe_top_le_withTop : ∀ {N : WithTop ℕ∞}, ↑⊤ ≤ N → ∀ (n : ℕ), ↑n < N
-- Mathlib.LinearAlgebra.Trace
Matrix.trace_map : ∀ {K : Type u_6} {m : Type u_7} {n : Type u_8} [inst : Field K] [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] {F : Type u_9} [inst_5 : EquivLike F (Matrix m m K) (Matrix n n K)]
  [AlgEquivClass F K (Matrix m m K) (Matrix n n K)] (f : F) (x : Matrix m m K), (f x).trace = x.trace
-- Init.Omega.Constraint
/-- Apply a function to both the lower bound and upper bound.  -/
Lean.Omega.Constraint.map : Lean.Omega.Constraint → (ℤ → ℤ) → Lean.Omega.Constraint
-- Mathlib.Algebra.Category.CoalgCat.ComonEquivalence
CoalgCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap : ∀ {R : Type u} [inst : CommRing R] {M : Type u} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Coalgebra R M],
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CoalgCat.of R M)).hom.toCoalgHom'.toLinearMap =
    ↑(TensorProduct.lid R M)
-- Mathlib.Topology.Constructions
IsClosed.preimage_val : ∀ {X : Type u} [inst : TopologicalSpace X] {s t : Set X}, IsClosed t → IsClosed (Subtype.val ⁻¹' t)
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic
ProbabilityTheory.IsGaussianProcess.comp_right : ∀ {S : Type u_1} {T : Type u_2} {Ω : Type u_3} {E : Type u_4} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  {X : T → Ω → E} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [inst_3 : NormedSpace ℝ E]
  [SecondCountableTopology E],
  ProbabilityTheory.IsGaussianProcess X P → ∀ (f : S → T), ProbabilityTheory.IsGaussianProcess (X ∘ f) P
-- Mathlib.Logic.Basic
/-- `Fact.out` contains the unwrapped witness for the fact represented by the instance of
`Fact p`.  -/
Fact.out : ∀ {p : Prop} [self : Fact p], p
-- Mathlib.Order.Cover
Set.Ioc_eq_singleton_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b c : α}, Set.Ioc b a = {c} ↔ a = c ∧ b ⋖ a
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_le : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Multiset α} {a : α}, a ∈ s → s.inf ≤ a
-- Lean.Meta.InferType
/-- Returns `true` iff `type` is `Prop` or `As → Prop`.
 -/
Lean.Meta.isPropFormerType : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.brecOn.go : {V : Type u} →
  [inst : Quiver V] →
    {a : V} →
      {motive : (a_1 : V) → Quiver.Path a a_1 → Sort u_1} →
        {a_1 : V} →
          (t : Quiver.Path a a_1) →
            ((a_2 : V) → (t : Quiver.Path a a_2) → Quiver.Path.below t → motive a_2 t) →
              motive a_1 t ×' Quiver.Path.below t
-- Std.Data.DHashMap.Raw
_private.Std.Data.DHashMap.Raw.0.Std.DHashMap.Raw.Const.insertMany.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ (α × β)]
  (m : Std.DHashMap.Raw α fun x => β) (l : ρ),
  Std.DHashMap.Raw.Const.insertMany m l =
    if h : 0 < m.buckets.size then ↑↑(Std.DHashMap.Internal.Raw₀.Const.insertMany ⟨m, h⟩ l) else m
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited (Topology.WithUpperSet α)
-- Mathlib.Order.Basic
exists_le_of_linear : ∀ {α : Type u_2} [inst : LinearOrder α] (a b : α), ∃ c ≤ a, c ≤ b
-- Mathlib.Analysis.Analytic.Inverse
/-- The left inverse of a formal multilinear series, where the `n`-th term is defined inductively
in terms of the previous ones to make sure that `(leftInv p i) ∘ p = id`. For this, the linear term
`p₁` in `p` should be invertible. In the definition, `i` is a linear isomorphism that should
coincide with `p₁`, so that one can use its inverse in the construction. The definition does not
use that `i = p₁`, but proofs that the definition is well-behaved do.

The `n`-th term in `q ∘ p` is `∑ qₖ (p_{j₁}, ..., p_{jₖ})` over `j₁ + ... + jₖ = n`. In this
expression, `qₙ` appears only once, in `qₙ (p₁, ..., p₁)`. We adjust the definition so that this
term compensates the rest of the sum, using `i⁻¹` as an inverse to `p₁`.

These formulas only make sense when the constant term `p₀` vanishes. The definition we give is
general, but it ignores the value of `p₀`.
 -/
FormalMultilinearSeries.leftInv : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type u_3} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] →
                FormalMultilinearSeries 𝕜 E F → (E ≃L[𝕜] F) → E → FormalMultilinearSeries 𝕜 F E
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.PollSources.headerTimeout : {α β : Type} → Std.Http.Server.Connection.PollSources✝ α β → Option Std.Time.Timestamp
-- Mathlib.Order.Category.OmegaCompletePartialOrder
ωCPO.instHasProducts : CategoryTheory.Limits.HasProducts ωCPO
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
/-- Product rule for Lie brackets: given two vector fields `V` and `W` on `M` and a function
`f : M → 𝕜`, we have `[V, f • W] = (df V) • W + f • [V, W]`.
 -/
VectorField.mlieBracket_smul_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {V W : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E] {f : M → 𝕜},
  MDiffAt f x →
    (MDiffAt fun x => ⟨x, W x⟩) x →
      VectorField.mlieBracket I V (f • W) x = (d% f x) (V x) • W x + f x • VectorField.mlieBracket I V W x
-- Mathlib.CategoryTheory.Types.Monomorphisms
CategoryTheory.Types.instIsStableUnderCoproductsMonomorphismsType : CategoryTheory.MorphismProperty.IsStableUnderCoproducts.{u_1, u, u + 1}
  (CategoryTheory.MorphismProperty.monomorphisms (Type u))
-- Lean.Declaration
Lean.ConstantInfo.isTheorem : Lean.ConstantInfo → Bool
-- Mathlib.Topology.Category.UniformSpace
CpltSepUniformSpace.instFunLike : (X : CpltSepUniformSpace) → (Y : CpltSepUniformSpace) → FunLike { f // UniformContinuous f } X.α Y.α
-- Mathlib.Algebra.Order.Module.HahnEmbedding
HahnEmbedding.ArchimedeanStrata.mk.inj : ∀ {K : Type u_1} {inst : DivisionRing K} {inst_1 : LinearOrder K} {inst_2 : IsOrderedRing K} {inst_3 : Archimedean K}
  {M : Type u_2} {inst_4 : AddCommGroup M} {inst_5 : LinearOrder M} {inst_6 : IsOrderedAddMonoid M}
  {inst_7 : Module K M} {inst_8 : IsOrderedModule K M} {stratum : FiniteArchimedeanClass M → Submodule K M}
  {disjoint_ball_stratum : ∀ (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (stratum c)}
  {ball_sup_stratum_eq :
    ∀ (c : FiniteArchimedeanClass M),
      FiniteArchimedeanClass.ball K c ⊔ stratum c = FiniteArchimedeanClass.closedBall K c}
  {stratum_1 : FiniteArchimedeanClass M → Submodule K M}
  {disjoint_ball_stratum_1 : ∀ (c : FiniteArchimedeanClass M), Disjoint (FiniteArchimedeanClass.ball K c) (stratum_1 c)}
  {ball_sup_stratum_eq_1 :
    ∀ (c : FiniteArchimedeanClass M),
      FiniteArchimedeanClass.ball K c ⊔ stratum_1 c = FiniteArchimedeanClass.closedBall K c},
  { stratum := stratum, disjoint_ball_stratum := disjoint_ball_stratum, ball_sup_stratum_eq := ball_sup_stratum_eq } =
      { stratum := stratum_1, disjoint_ball_stratum := disjoint_ball_stratum_1,
        ball_sup_stratum_eq := ball_sup_stratum_eq_1 } →
    stratum = stratum_1
-- Init.Data.BitVec.Lemmas
BitVec.lt_one_iff : ∀ {w : ℕ} {x : BitVec w}, 0 < w → (x < 1#w ↔ x = 0#w)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso.eq_1 : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso C =
    CategoryTheory.NatIso.ofComponents
      (fun F => CategoryTheory.LaxMonoidalFunctor.isoOfComponents (fun x => F.mapIso (CategoryTheory.eqToIso ⋯)) ⋯ ⋯ ⋯)
      ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- A vertex lies on its median.  -/
Affine.Simplex.point_mem_median : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.points i ∈ s.median i
-- Mathlib.RingTheory.DedekindDomain.Different
dvd_differentIdeal_of_not_isSeparable : ∀ (A : Type u_1) {B : Type u_3} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [inst_4 : IsDedekindDomain A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B]
  [inst_7 : Module.Finite A B] [Algebra.IsSeparable (FractionRing A) (FractionRing B)] {p : Ideal A} [p.IsMaximal],
  p ≠ ⊥ →
    ∀ (P : Ideal B) [P.IsMaximal] [inst_11 : P.LiesOver p],
      ¬Algebra.IsSeparable (A ⧸ p) (B ⧸ P) → P ∣ differentIdeal A B
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_pow_le : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {n : ℕ}, (p ^ n).degrees ≤ n • p.degrees
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
/-- The medial is the simplex formed by centroids on all faces.  -/
Affine.Simplex.medial : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_3} →
      [inst : DivisionRing k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : AddTorsor V P] → {n : ℕ} → [NeZero n] → [CharZero k] → Affine.Simplex k P n → Affine.Simplex k P n
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientGroup.instNorm.eq_1 : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S : Subgroup M},
  QuotientGroup.instNorm = { norm := ⇑QuotientGroup.groupSeminorm }
-- Mathlib.Analysis.Calculus.Deriv.Shift
/-- Translation in the domain does not change the derivative.  -/
HasDerivAt.comp_add_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} (x a : 𝕜),
  HasDerivAt f f' (x + a) → HasDerivAt (fun x => f (x + a)) f' x
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_3.eq_7 : ∀ (motive : Lean.Expr → Sort u_1) (x : Lean.Expr)
  (h_1 : (name : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const name us))
  (h_2 : (f x : Lean.Expr) → motive (f.app x))
  (h_3 :
    (binderName : Lean.Name) →
      (ty body : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName ty body binderInfo))
  (h_4 : Unit → motive (Lean.Expr.sort Lean.Level.zero)) (h_5 : (a : Lean.Level) → motive (Lean.Expr.sort a.succ))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (x : Lean.Expr) → motive x),
  (∀ (name : Lean.Name) (us : List Lean.Level), x = Lean.Expr.const name us → False) →
    (∀ (f x_2 : Lean.Expr), x = f.app x_2 → False) →
      (∀ (binderName : Lean.Name) (ty body : Lean.Expr) (binderInfo : Lean.BinderInfo),
          x = Lean.Expr.forallE binderName ty body binderInfo → False) →
        (x = Lean.Expr.sort Lean.Level.zero → False) →
          (∀ (a : Lean.Level), x = Lean.Expr.sort a.succ → False) →
            (∀ (u : Lean.Level), x = Lean.Expr.sort u → False) →
              (match x with
                | Lean.Expr.const name us => h_1 name us
                | f.app x => h_2 f x
                | Lean.Expr.forallE binderName ty body binderInfo => h_3 binderName ty body binderInfo
                | Lean.Expr.sort Lean.Level.zero => h_4 ()
                | Lean.Expr.sort a.succ => h_5 a
                | Lean.Expr.sort u => h_6 u
                | x => h_7 x) =
                h_7 x
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.interSmallerFn.match_3.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} (motive : Option ((a : α) × β a) → Sort u_3)
  (h_1 : (kv' : (a : α) × β a) → motive (some kv')) (h_2 : Unit → motive none),
  (match none with
    | some kv' => h_1 kv'
    | none => h_2 ()) =
    h_2 ()
-- Init.Data.List.TakeDrop
List.drop_length : ∀ {α : Type u_1} {l : List α}, List.drop l.length l = []
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- **Alias** of `Subgroup.val_finsetProd`. -/
Subgroup.val_finset_prod : ∀ {ι : Type u_3} {G : Type u_4} [inst : CommGroup G] (H : Subgroup G) (f : ι → ↥H) (s : Finset ι),
  ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Init.Data.List.Monadic
List.filterMapM_cons : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {a : α} {l : List α} [inst : Monad m] [LawfulMonad m]
  {f : α → m (Option β)},
  List.filterMapM f (a :: l) = do
    let __do_lift ← f a
    match __do_lift with
      | none => List.filterMapM f l
      | some b => do
        let __do_lift ← List.filterMapM f l
        pure (b :: __do_lift)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_rotateRightAux_of_ge : ∀ {w : ℕ} {x : BitVec w} {r i : ℕ}, i ≥ r → (x.rotateRightAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - r))
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.instInhabitedAlt.default : {σ : Type} → [Inhabited σ] → Lean.Elab.Term.Do.Alt σ
-- Lean.Parser.Basic
Lean.Parser.decimalNumberFn : String.Pos.Raw → optParam Bool true → Lean.Parser.ParserContext → Lean.Parser.ParserState → Lean.Parser.ParserState
-- Init.Data.SInt.Lemmas
Int32.lt_of_le_of_ne : ∀ {a b : Int32}, a ≤ b → a ≠ b → a < b
-- Init.Data.Int.DivMod.Lemmas
Int.mul_tmod_mul_of_pos : ∀ {a : ℤ} (b c : ℤ), 0 < a → (a * b).tmod (a * c) = a * b.tmod c