mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.Internalize
/-- If type of `a` is a structure and is tagged with `[grind ext]` attribute,
propagate `a = ⟨a.1, ..., a.n⟩`

This function subsumes the `propagateUnitLike` function we used in the past.
Recall that the `propagateUnitLike` was added because `isDefEq` implements it,
and consequently the simplifier reduces terms of the form `a = ctor` to `True` using `eq_self`.
This `isDefEq` feature was negatively affecting `grind` until we added an
equivalent one here. For example, when splitting on a `match`-expression
using Unit-like types, equalities about these types were being reduced to `True`
by `simp` (i.e., in the `grind` preprocessor), and `grind` would never see
these facts.
 -/
_private.Lean.Meta.Tactic.Grind.Internalize.0.Lean.Meta.Grind.propagateEtaStruct : Lean.Expr → ℕ → Lean.Meta.Grind.GoalM Unit
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  {f : α → β → Bool} {k : α} {fallback : β} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.getD (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl k fallback =
    ((Std.DTreeMap.Internal.Impl.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Init.Data.Option.Lemmas
Option.pfilter_eq_filter : ∀ {α : Type u_1} {o : Option α} {p : α → Bool}, (o.pfilter fun a x => p a) = Option.filter p o
-- Mathlib.Analysis.Analytic.IteratedFDeriv
/-- The `n`-th iterated derivative of an analytic function is symmetric.  -/
ContDiffAt.iteratedFDeriv_comp_perm : ∀ {𝕜 : 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] {f : E → F}
  {x : E},
  ContDiffAt 𝕜 ⊤ f x →
    ∀ {n : ℕ} (v : Fin n → E) (σ : Equiv.Perm (Fin n)), (iteratedFDeriv 𝕜 n f x) (v ∘ ⇑σ) = (iteratedFDeriv 𝕜 n f x) v
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
/-- Let `result` be the result of evaluating proposition `p`, return a `.done` step where
the resulting expression is `True`(`False`) if `result is `true`(`false`), and the
proof is uses `Decidable p` and the auxiliary theorems `eq_true_of_decide`/`eq_false_of_decide`.
 -/
Lean.Meta.Simp.evalPropStep : Lean.Expr → Bool → Lean.Meta.SimpM Lean.Meta.Simp.Step
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_append_of_containsKey_right_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l' = false →
    Std.Internal.List.replaceEntry k v (l ++ l') = Std.Internal.List.replaceEntry k v l ++ l'
-- Std.Http.Server
/-- Returns a `Selector` that waits for the server to shut down.
 -/
Std.Http.Server.waitShutdownSelector : Std.Http.Server → Std.Async.Selector Unit
-- Mathlib.Algebra.Order.Module.Archimedean
FiniteArchimedeanClass.submodule_strictAnti : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M], StrictAnti (FiniteArchimedeanClass.submodule K)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- When `g` is a monomorphism, the kernel of `f ≫ g` is isomorphic to the kernel of `f`.
 -/
CategoryTheory.Limits.kernelCompMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y Z : C} →
        (f : X ⟶ Y) →
          (g : Y ⟶ Z) →
            [inst_2 : CategoryTheory.Limits.HasKernel f] →
              [inst_3 : CategoryTheory.Mono g] →
                CategoryTheory.Limits.kernel (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.Limits.kernel f
-- Mathlib.Algebra.Group.Action.Sigma
Sigma.instMulAction : {ι : Type u_1} →
  {M : Type u_2} → {α : ι → Type u_4} → {m : Monoid M} → [(i : ι) → MulAction M (α i)] → MulAction M ((i : ι) × α i)
-- Mathlib.Data.List.Iterate
List.iterate_eq_nil : ∀ {α : Type u_1} {f : α → α} {a : α} {n : ℕ}, List.iterate f a n = [] ↔ n = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_mul_apply_left : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : Group G] (x y : MonoidAlgebra R G) (g : G),
  (x * y).coeff g = x.coeff.sum fun h r => r * y.coeff (h⁻¹ * g)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.State.exprToNatStructId : Lean.Meta.Grind.Arith.Linear.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr ℕ
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.instR1Space : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  R1Space (MeasureTheory.FiniteMeasure Ω)
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.eval₂_intCastRingHom_X : ∀ {R : Type u_3} [inst : Ring R] (p : Polynomial ℤ) (f : Polynomial ℤ →+* R),
  Polynomial.eval₂ (Int.castRingHom R) (f Polynomial.X) p = f p
-- Init.Data.Dyadic.Round
Dyadic.le_roundUp : ∀ {x : Dyadic} {prec : ℤ}, x ≤ x.roundUp prec
-- Init.Data.Vector.Lemmas
Vector.flatMap_id' : ∀ {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n}, (xss.flatMap fun xs => xs) = xss.flatten
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.instInhabitedWalkingParallelPair.default : CategoryTheory.Limits.WalkingParallelPair
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.insertP.loop.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (b : α) (l r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (b : α) → (l r : List α) → motive (b :: l) r),
  (match b :: l, r with
    | [], r => h_1 r
    | b :: l, r => h_2 b l r) =
    h_2 b l r
-- Mathlib.Data.Multiset.Bind
Multiset.join_add : ∀ {α : Type u_1} (S T : Multiset (Multiset α)), (S + T).join = S.join + T.join
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.NumDenSameDeg.den_one : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubmonoidClass σ A] {𝒜 : ι → σ} (x : Submonoid A) [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι]
  [inst_5 : GradedRing 𝒜], ↑(HomogeneousLocalization.NumDenSameDeg.den 1) = 1
-- Mathlib.Order.Heyting.Basic
IsCompl.eq_hnot : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, IsCompl a b → a = ￢b
-- Mathlib.Algebra.Group.Defs
InvolutiveNeg.toNeg : {A : Type u_2} → [self : InvolutiveNeg A] → Neg A
-- Mathlib.Topology.MetricSpace.Bounded
/-- The diameter of a set is always nonnegative  -/
Metric.diam_nonneg : ∀ {α : Type u} {s : Set α} [inst : PseudoMetricSpace α], 0 ≤ Metric.diam s
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Dense.extend_of_ind : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {s : Set α} {f : ↑s → β} [T0Space β]
  (hs : Dense s), UniformContinuous f → ∀ (x : ↑s), hs.extend f ↑x = f x
-- Lean.Elab.Term.TermElabM
/-- Task for nested incrementality, if enabled for tactic.  -/
Lean.Elab.Tactic.TacticParsedSnapshotInner.inner? : {α : Type} → Lean.Elab.Tactic.TacticParsedSnapshotInner α → Option (Lean.Language.SnapshotTask α)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.isStackFor_iff_of_sieve_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {S : C}
  {R R' : CategoryTheory.Presieve S},
  CategoryTheory.Sieve.generate R = CategoryTheory.Sieve.generate R' → (F.IsStackFor R ↔ F.IsStackFor R')
-- Batteries.Tactic.Case
/-- `case' _ : t => tac` is similar to the `case _ : t => tac` tactic,
but it does not ensure the goal has been solved after applying `tac`,
nor does it admit the goal if `tac` failed.
Recall that `case` closes the goal using `sorry` when `tac` fails,
and the tactic execution is not interrupted.  -/
Batteries.Tactic.casePatt' : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_injective_left : ∀ {α : Type u_2} [inst : DistribLattice α] [inst_1 : LocallyFiniteOrder α] (a : α), Function.Injective (Finset.uIcc a)
-- Mathlib.Topology.Compactness.LocallyCompact
/-- A reformulation of the definition of locally compact space: In a locally compact space,
every open set containing `x` has a compact subset containing `x` in its interior.  -/
exists_compact_subset : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {x : X} {U : Set X},
  IsOpen U → x ∈ U → ∃ K, IsCompact K ∧ x ∈ interior K ∧ K ⊆ U
-- Lean.Linter.Init
Lean.Linter.LinterSetsState.mk.sizeOf_spec : ∀ (merged : Lean.Linter.LinterSets) (localEntries : Array (Lean.Name × Lean.NameSet)),
  sizeOf { merged := merged, localEntries := localEntries } = 1 + sizeOf merged + sizeOf localEntries
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_trim : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α), m.trim.trim = m.trim
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.WithUpperSet.toUpperSet_inj : ∀ {α : Type u_1} {a b : α}, Topology.WithUpperSet.toUpperSet a = Topology.WithUpperSet.toUpperSet b ↔ a = b
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
Nat.Partition.ofSym.eq_1 : ∀ {n : ℕ} {σ : Type u_1} (s : Sym σ n) [inst : DecidableEq σ],
  Nat.Partition.ofSym s =
    { parts := Multiset.map (fun a => Multiset.count a ↑s) (↑s).dedup, parts_pos := ⋯, parts_sum := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.minKeyD_modify : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {f : β → β},
      (Std.DTreeMap.Internal.Impl.Const.modify k f t).isEmpty = false →
        ∀ {fallback : α},
          (Std.DTreeMap.Internal.Impl.Const.modify k f t).minKeyD fallback =
            if compare (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback
-- Mathlib.MeasureTheory.Function.AEMeasurableSequence
aeSeq.mk_eq_fun_of_mem_aeSeqSet : ∀ {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {f : ι → α → β}
  {μ : MeasureTheory.Measure α} {p : α → (ι → β) → Prop} (hf : ∀ (i : ι), AEMeasurable (f i) μ) {x : α},
  x ∈ aeSeqSet hf p → ∀ (i : ι), AEMeasurable.mk (f i) ⋯ x = f i x
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.sInf_empty : sInf ∅ = 0
-- Mathlib.Data.Nat.PSub
Nat.ppred_zero : Nat.ppred 0 = none
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.monoidWithZero : MonoidWithZero Ordinal.{u_4}
-- Mathlib.Algebra.Lie.Weights.Chain
/-- This is the largest `n : ℕ` such that `i • α + β` is a weight for all `0 ≤ i ≤ n`.  -/
LieModule.chainTopCoeff : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {M : Type u_3} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      [IsAddTorsionFree R] →
                        [IsDomain R] →
                          [Module.IsTorsionFree R M] → [IsNoetherian R M] → (L → R) → LieModule.Weight R L M → ℕ
-- Mathlib.CategoryTheory.ObjectProperty.LimitsClosure
CategoryTheory.ObjectProperty.limitsClosure.below.of_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  {motive : (a : C) → P.limitsClosure J a → Prop} {X Y : C} (e : X ≅ Y) (hX : P.limitsClosure J X),
  CategoryTheory.ObjectProperty.limitsClosure.below hX →
    motive X hX → CategoryTheory.ObjectProperty.limitsClosure.below ⋯
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.map_mk_eq_bot_of_le : ∀ {R : Type u} [inst : Ring R] {I J : Ideal R} [inst_1 : J.IsTwoSided], I ≤ J → Ideal.map (Ideal.Quotient.mk J) I = ⊥
-- Mathlib.RingTheory.RingHom.Unramified
RingHom.FormallyUnramified.of_surjective : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  Function.Surjective ⇑f → f.FormallyUnramified
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_le_map_iff_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ⇑f → ∀ {S T : AddSubmonoid M}, AddSubmonoid.map f S ≤ AddSubmonoid.map f T ↔ S ≤ T
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
OrderIso.map_ciSup_set : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : ConditionallyCompleteLattice α]
  [inst_1 : ConditionallyCompleteLattice β] (e : α ≃o β) {s : Set γ} {f : γ → α},
  BddAbove (f '' s) → s.Nonempty → e (⨆ i, f ↑i) = ⨆ i, e (f ↑i)
-- Mathlib.Analysis.Analytic.CPolynomialDef
CPolynomialOn.mono : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E},
  CPolynomialOn 𝕜 f t → s ⊆ t → CPolynomialOn 𝕜 f s
-- Mathlib.CategoryTheory.Center.Basic
CategoryTheory.CatCenter.instSMulUnitsIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → SMul (CategoryTheory.CatCenter C)ˣ (X ≅ Y)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- A subfield `t` includes `closure s` if and only if it includes `s`.  -/
Subfield.closure_le : ∀ {K : Type u} [inst : DivisionRing K] {s : Set K} {t : Subfield K}, Subfield.closure s ≤ t ↔ s ⊆ ↑t
-- Init.Data.SInt.Bitwise
ISize.toInt64_and : ∀ (a b : ISize), (a &&& b).toInt64 = a.toInt64 &&& b.toInt64
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.Flat
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get?_inter_of_not_mem_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ ∩ m₂).get? k = none
-- Mathlib.Topology.Separation.Regular
/-- If the codomain of a closed embedding is a normal space, then so is the domain.  -/
Topology.IsClosedEmbedding.normalSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [NormalSpace Y] {f : X → Y},
  Topology.IsClosedEmbedding f → NormalSpace X
-- Init.Data.List.Lemmas
List.set_cons_zero : ∀ {α : Type u_1} {x : α} {xs : List α} {a : α}, (x :: xs).set 0 a = a :: xs
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
LipschitzWith.norm_compLp_sub_le : ∀ {α : Type u_1} {E : Type u_4} {F : Type u_5} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] {g : E → F} {c : NNReal} (hg : LipschitzWith c g)
  (g0 : g 0 = 0) (f f' : ↥(MeasureTheory.Lp E p μ)), ‖hg.compLp g0 f - hg.compLp g0 f'‖ ≤ ↑c * ‖f - f'‖
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The terminal object in `Factorisation f`, with the codomain of `f` as its midpoint.  -/
CategoryTheory.Factorisation.terminal : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.Factorisation f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.logMap_torsion_smul : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K)
  {ζ : (NumberField.RingOfIntegers K)ˣ},
  ζ ∈ NumberField.Units.torsion K → NumberField.mixedEmbedding.logMap (ζ • x) = NumberField.mixedEmbedding.logMap x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α (fun x => Unit) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {l : List α} {k fallback : α},
      k ∈ t → (Std.DTreeMap.Raw.Const.insertManyIfNewUnit t l).getKeyD k fallback = t.getKeyD k fallback
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- A linear isometric embedding of a normed `R`-module into another one.  -/
«term_→ₗᵢ[_]_» : Lean.TrailingParserDescr
-- Mathlib.NumberTheory.Cyclotomic.CyclotomicCharacter
modularCyclotomicCharacter.toFun.congr_simp : ∀ {L : Type u} [inst : CommRing L] [inst_1 : IsDomain L] (n : ℕ) [inst_2 : NeZero n] (g g_1 : L ≃+* L),
  g = g_1 → modularCyclotomicCharacter.toFun n g = modularCyclotomicCharacter.toFun n g_1
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_id : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R], MvPolynomial.bind₁ id = MvPolynomial.join₁
-- Mathlib.Algebra.Free
/-- Recursor on `FreeMagma` using `pure` instead of `of`.  -/
FreeMagma.recOnPure : {α : Type u} →
  {C : FreeMagma α → Sort l} →
    (x : FreeMagma α) → ((x : α) → C (pure x)) → ((x y : FreeMagma α) → C x → C y → C (x * y)) → C x
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Formula for `hurwitzZetaOdd` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version with absolute values)  -/
HurwitzZeta.hasSum_nat_hurwitzZetaOdd : ∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum
      (fun n => (↑(SignType.sign (↑n + a)) / ↑|↑n + a| ^ s - ↑(SignType.sign (↑n + 1 - a)) / ↑|↑n + 1 - a| ^ s) / 2)
      (HurwitzZeta.hurwitzZetaOdd (↑a) s)
-- Mathlib.Data.Multiset.Replicate
Multiset.le_count_iff_replicate_le : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α} {n : ℕ},
  n ≤ Multiset.count a s ↔ Multiset.replicate n a ≤ s
-- Aesop.Builder.Constructors
Aesop.RuleBuilder.constructorsCore : Lean.InductiveVal →
  Option Aesop.IndexingMode →
    Lean.Meta.TransparencyMode → Lean.Meta.TransparencyMode → Aesop.PhaseSpec → Lean.MetaM Aesop.LocalRuleSetMember
-- Mathlib.CategoryTheory.DifferentialObject
/-- An isomorphism of differential objects gives an isomorphism of the underlying objects.  -/
CategoryTheory.DifferentialObject.isoApp : {S : Type u_1} →
  [inst : AddMonoidWithOne S] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.HasShift C S] →
            {X Y : CategoryTheory.DifferentialObject S C} → (X ≅ Y) → (X.obj ≅ Y.obj)
-- Mathlib.Topology.Maps.Basic
/-- Preimage of a dense set under an open map is dense.  -/
Dense.preimage : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y},
  Dense s → IsOpenMap f → Dense (f ⁻¹' s)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.comp_whisker_left : ∀ {B : Type u} [inst : Quiver B] {a b c d : B} (f : CategoryTheory.FreeBicategory.Hom a b)
  (g : CategoryTheory.FreeBicategory.Hom b c) {h h' : CategoryTheory.FreeBicategory.Hom c d}
  (η : CategoryTheory.FreeBicategory.Hom₂ h h'),
  CategoryTheory.FreeBicategory.Rel (CategoryTheory.FreeBicategory.Hom₂.whisker_left (f.comp g) η)
    ((CategoryTheory.FreeBicategory.Hom₂.associator f g h).vcomp
      ((CategoryTheory.FreeBicategory.Hom₂.whisker_left f (CategoryTheory.FreeBicategory.Hom₂.whisker_left g η)).vcomp
        (CategoryTheory.FreeBicategory.Hom₂.associator_inv f g h')))
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanOrder.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : Inhabited M], MulArchimedeanOrder.instInhabited = { default := MulArchimedeanOrder.of default }
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The functor induced by a composition is the composition of the functors they induce.  -/
CategoryTheory.FreeGroupoid.mapComp : {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] →
            (φ : CategoryTheory.Functor C D) →
              (φ' : CategoryTheory.Functor D E) →
                CategoryTheory.FreeGroupoid.map (φ.comp φ') ≅
                  (CategoryTheory.FreeGroupoid.map φ).comp (CategoryTheory.FreeGroupoid.map φ')
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.pow_vle_pow_of_vle_one : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : ValuativeRel R] {a : R}, a ≤ᵥ 1 → ∀ {n m : ℕ}, n ≤ m → a ^ m ≤ᵥ a ^ n
-- Mathlib.Analysis.Convex.Segment
openSegment_subset_Ioo : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder E] [IsOrderedCancelAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulStrictMono 𝕜 E] {x y : E},
  x < y → openSegment 𝕜 x y ⊆ Set.Ioo x y
-- Batteries.Tactic.Trans
/-- Internal definition for `trans` tactic. Either a binary relation or a non-dependent
arrow.  -/
Batteries.Tactic.TransRelation : Type
-- Mathlib.Topology.Compactness.LocallyCompact
/-- If `f` is a topology inducing map with a locally compact codomain and a locally closed range,
then the domain of `f` is a locally compact space.  -/
Topology.IsInducing.locallyCompactSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [LocallyCompactSpace Y]
  {f : X → Y}, Topology.IsInducing f → IsLocallyClosed (Set.range f) → LocallyCompactSpace X
-- Mathlib.GroupTheory.NoncommCoprod
MonoidHom.noncommCoprod.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)),
  f.noncommCoprod g comm = { toFun := fun mn => f mn.1 * g mn.2, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.coe_cardSuppLTAddSubgroup : ∀ (Γ : Type u_1) (R : Type u_2) (κ : Cardinal.{u_1}) [inst : PartialOrder Γ] [inst_1 : AddGroup R]
  [hκ : Fact (Cardinal.aleph0 ≤ κ)], ↑(HahnSeries.cardSuppLTAddSubgroup Γ R κ) = {x | x.cardSupp < κ}
-- Lean.ScopedEnvExtension
_private.Lean.ScopedEnvExtension.0.Lean.ScopedEnvExtension.setDelimitsLocal.go : {σ : Type} → ℕ → List (Lean.ScopedEnvExtension.State σ) → List (Lean.ScopedEnvExtension.State σ)
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.ofFixingSubgroup_of_eq_apply : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {hst : s = t}
  (x : ↥(SubMulAction.ofFixingSubgroup M s)), ↑((SubMulAction.ofFixingSubgroup_of_eq M hst) x) = ↑x
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.BasicMeasure.mk.injEq : ∀ (toTerminationMeasure : Lean.Elab.TerminationMeasure) (natFn : Lean.Expr)
  (toTerminationMeasure_1 : Lean.Elab.TerminationMeasure) (natFn_1 : Lean.Expr),
  ({ toTerminationMeasure := toTerminationMeasure, natFn := natFn } =
      { toTerminationMeasure := toTerminationMeasure_1, natFn := natFn_1 }) =
    (toTerminationMeasure = toTerminationMeasure_1 ∧ natFn = natFn_1)
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- A `MulEquiv` `φ` between two monoids `M` and `N` induces a `MulEquiv` between
a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`.
See `MonoidHom.submonoidMap` for a variant for `MonoidHom`s.  -/
MulEquiv.submonoidMap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] → [inst_1 : MulOneClass N] → (e : M ≃* N) → (S : Submonoid M) → ↥S ≃* ↥(Submonoid.map e S)
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.toTopologicalSpace_mono : ∀ {α : Type ua} {u₁ u₂ : UniformSpace α}, u₁ ≤ u₂ → u₁.toTopologicalSpace ≤ u₂.toTopologicalSpace
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.toAddSubsemigroup'_closure : ∀ {A : Type u_5} [inst : Add A] (S : Set (Multiplicative A)),
  Subsemigroup.toAddSubsemigroup' (Subsemigroup.closure S) = AddSubsemigroup.closure (⇑Multiplicative.ofAdd ⁻¹' S)
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.enum_inj : ∀ {α : Type u} {r : α → α → Prop} [inst : IsWellOrder α r] {o₁ o₂ : ↑(Set.Iio (Ordinal.type r))},
  (Ordinal.enum r) o₁ = (Ordinal.enum r) o₂ ↔ o₁ = o₂