mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Instances.Icc
/-- **Alias** of `contMDiff_subtypeVal_Icc`.

---

The inclusion map from of a closed segment to `ℝ` is smooth in the manifold sense.  -/
contMDiff_subtype_coe_Icc : ∀ {x y : ℝ} [h : Fact (x < y)] {n : WithTop ℕ∞},
  ContMDiff (modelWithCornersEuclideanHalfSpace 1) (modelWithCornersSelf ℝ ℝ) n fun z => ↑z
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
Finsupp.linearCombination_smul : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] {α' : Type u_7} {v : α → M} [inst_4 : Module R S]
  [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {w : α' → S},
  (Finsupp.linearCombination R fun i => w i.2 • v i.1) =
    ↑R (Finsupp.linearCombination S v) ∘ₗ
      Finsupp.mapRange.linearMap (Finsupp.linearCombination R w) ∘ₗ ↑(Finsupp.curryLinearEquiv R)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.natCast_natAbs_norm : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (x : GaussianInt), ↑(Zsqrtd.norm x).natAbs = ↑(Zsqrtd.norm x)
-- Init.Prelude
/-- `a ^ b` computes `a` to the power of `b` where `a` and `b` both have the same type.  -/
HomogeneousPow.pow : {α : Type u} → [self : HomogeneousPow α] → α → α → α
-- Init.Data.BitVec.Lemmas
BitVec.msb_rotateRight : ∀ {r w : ℕ} {x : BitVec w}, (x.rotateRight r).msb = x.getMsbD ((w - r % w) % w)
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_comm : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι)
  (t : Finset κ) (f : ι → κ → M),
  (s.expect fun i => t.expect fun j => f i j) = t.expect fun j => s.expect fun i => f i j
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictAnti.const_add : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
  [AddLeftStrictMono α], StrictAnti f → ∀ (c : α), StrictAnti fun x => c + f x
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- The determinant of a matrix, as a monoid homomorphism.  -/
Matrix.detMonoidHom : {n : Type u_2} →
  [inst : DecidableEq n] → [inst_1 : Fintype n] → {R : Type v} → [inst_2 : CommRing R] → Matrix n n R →* R
-- Mathlib.Topology.Order.Basic
/-- The topology is generated by open intervals `Set.Ioi _` and `Set.Iio _`.  -/
OrderTopology.topology_eq_generate_intervals : ∀ {α : Type u_1} {t : TopologicalSpace α} {inst : Preorder α} [self : OrderTopology α], t = Preorder.topology α
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
/-- A version of `linearIndependent_le_span` for `Finset`.  -/
linearIndependent_le_span_finset : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [StrongRankCondition R]
  {ι : Type u_2} (v : ι → M),
  LinearIndependent R v → ∀ (w : Finset M), Submodule.span R ↑w = ⊤ → Cardinal.mk ι ≤ ↑w.card
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.instHasDimensionLEObjSimplexCategoryMk : ∀ (n : ℕ), (SSet.stdSimplex.obj { len := n }).HasDimensionLE n
-- Mathlib.LinearAlgebra.Matrix.PosDef
/-- For an invertible matrix `U`, `star U * x * U` is positive semi-definite iff `x` is.
This works on any ⋆-ring with a partial order.

See `IsUnit.star_left_conjugate_nonneg_iff` for a similar statement for star-ordered rings.  -/
Matrix.IsUnit.posSemidef_star_left_conjugate_iff : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [inst_3 : Fintype n]
  [inst_4 : DecidableEq n] {U x : Matrix n n R}, IsUnit U → ((star U * x * U).PosSemidef ↔ x.PosSemidef)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_prod : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R] {ι : Type u_3}
  {P : ι → MvPolynomial σ R} {s : Finset ι}, (∀ i ∈ s, P i ≠ 0) → m.degree (∏ i ∈ s, P i) = ∑ i ∈ s, m.degree (P i)
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.symbolPrioExt : Lean.SimpleScopedEnvExtension Lean.Meta.Grind.SymbolPriorityEntry Lean.Meta.Grind.SymbolPriorities
-- Mathlib.Order.Filter.Prod
Filter.EventuallyLE.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} [inst : LE γ] [inst_1 : LE δ] {la : Filter α}
  {fa ga : α → γ},
  fa ≤ᶠ[la] ga → ∀ {lb : Filter β} {fb gb : β → δ}, fb ≤ᶠ[lb] gb → Prod.map fa fb ≤ᶠ[la ×ˢ lb] Prod.map ga gb
-- Init.Core
Function.const_comp : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} {c : γ}, Function.const β c ∘ f = Function.const α c
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonRefInfo : Lean.FromJson Lean.Lsp.RefInfo
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_sum`. -/
ContinuousLinearMap.coe_sum : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] [inst_8 : ContinuousAdd M₂] {ι : Type u_9}
  (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂), ↑(∑ d ∈ t, f d) = ∑ d ∈ t, ↑(f d)
-- Mathlib.ModelTheory.Semantics
/-- A term `t` with variables indexed by `α` can be evaluated by giving a value to each variable.  -/
FirstOrder.Language.Term.realize : {L : FirstOrder.Language} → {M : Type w} → [L.Structure M] → {α : Type u'} → (α → M) → L.Term α → M
-- Mathlib.Order.RelIso.Basic
RelEmbedding.coe_toMap : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (f : α ↪ β), ⇑(RelEmbedding.toMap r f) = ⇑f
-- Mathlib.Algebra.Star.Unitary
Unitary.instNegSubtypeMemSubmonoidUnitary : {R : Type u_1} → [inst : Ring R] → [inst_1 : StarRing R] → Neg ↥(unitary R)
-- Init.Data.Fin.Lemmas
Fin.val_eq_zero : ∀ (a : Fin 1), ↑a = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp},
  t.Equiv Std.DTreeMap.empty ↔ t.isEmpty = true
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `M'` is a localized module and `g` is a linear map `M → M''` such that all scalar multiplication
by `s : S` is invertible, then there is a linear map `M' → M''`.
 -/
IsLocalizedModule.lift : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M' : Type u_3} →
          {M'' : Type u_4} →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid M'] →
                [inst_3 : AddCommMonoid M''] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module R M'] →
                      [inst_6 : Module R M''] →
                        (f : M →ₗ[R] M') →
                          [IsLocalizedModule S f] →
                            (M →ₗ[R] M'') → (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → M' →ₗ[R] M''
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.coverage_toPrecoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.MorphismProperty C)
  [inst_1 : P.IsStableUnderBaseChange] [inst_2 : P.HasPullbacks], P.coverage.toPrecoverage = P.precoverage
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.optimalGHDist.congr_simp : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  GromovHausdorff.optimalGHDist✝ X Y = GromovHausdorff.optimalGHDist✝ X Y
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_rotateRight : ∀ {w n m : ℕ} {x : BitVec w},
  (x.rotateRight m).getMsbD n =
    (decide (n < w) && if n < m % w then x.getMsbD ((w + n - m % w) % w) else x.getMsbD (n - m % w))
-- Mathlib.Tactic.Module
/-- Given an expression `M` representing a type which is an `AddCommMonoid` and a module over *two*
semirings `R₁` and `R₂`, find the "bigger" of the two semirings.  That is, we assume that it will
turn out to be the case that either (1) `R₁` is an `R₂`-algebra and the `R₂` scalar action on `M` is
induced from `R₁`'s scalar action on `M`, or (2) vice versa; we return the semiring `R₁` in the
first case and `R₂` in the second case.

Moreover, given expressions representing particular scalar multiplications of `R₁` and/or `R₂` on
`M` (a `List (R₁ × M)`, a `List (R₂ × M)`, a pair `(r, x) : R₂ × M`), bump these up to the "big"
ring by applying the algebra-map where needed.  -/
Mathlib.Tactic.Module.qNF.matchRings : {v : Lean.Level} →
  {M : Q(Type v)} →
    {iM : Q(AddCommMonoid «$M»)} →
      {u₁ : Lean.Level} →
        {R₁ : Q(Type u₁)} →
          {iR₁ : Q(Semiring «$R₁»)} →
            (iRM₁ : Q(Module «$R₁» «$M»)) →
              {u₂ : Lean.Level} →
                {R₂ : Q(Type u₂)} →
                  (iR₂ : Q(Semiring «$R₂»)) →
                    (iRM₂ : Q(Module «$R₂» «$M»)) →
                      (l₁ : Mathlib.Tactic.Module.qNF R₁ M) →
                        (l₂ : Mathlib.Tactic.Module.qNF R₂ M) →
                          (r : Q(«$R₂»)) →
                            (x : Q(«$M»)) →
                              Lean.MetaM
                                ((u : Lean.Level) ×
                                  (R : Q(Type u)) ×
                                    (iR : Q(Semiring «$R»)) ×
                                      (x_1 : Q(Module «$R» «$M»)) ×
                                        ((l₁' : Mathlib.Tactic.Module.qNF R M) ×
                                            have a := l₁.toNF;
                                            have a_1 := l₁'.toNF;
                                            Q(«$a_1».eval = «$a».eval)) ×
                                          ((l₂' : Mathlib.Tactic.Module.qNF R M) ×
                                              have a := l₂.toNF;
                                              have a_1 := l₂'.toNF;
                                              Q(«$a_1».eval = «$a».eval)) ×
                                            (r' : Q(«$R»)) × Q(«$r'» • «$x» = «$r» • «$x»))
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.continuum_mul_ofNat : ∀ {n : ℕ} [inst : n.AtLeastTwo], Cardinal.continuum * OfNat.ofNat n = Cardinal.continuum
-- Mathlib.Topology.Category.Born
Born.str : (self : Born) → Bornology self.carrier
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
spanPoints.eq_1 : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] (s : Set P), spanPoints k s = {p | ∃ p₁ ∈ s, ∃ v ∈ vectorSpan k s, p = v +ᵥ p₁}
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addZeroClass : {α : Type u} → [AddZeroClass α] → AddZeroClass (WithBot α)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_union_le_size_add_size : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∪ t₂).size ≤ t₁.size + t₂.size
-- Mathlib.Algebra.Group.Subgroup.Defs
NegMemClass.mk : ∀ {S : Type u_3} {G : outParam (Type u_4)} [inst : Neg G] [inst_1 : SetLike S G],
  (∀ {s : S} {x : G}, x ∈ s → -x ∈ s) → NegMemClass S G
-- Init.Data.Array.Lemmas
Array.map_id_fun : ∀ {α : Type u_1}, Array.map id = id
-- Mathlib.NumberTheory.ClassNumber.Finite
/-- If the `R`-integral element `a : S` has coordinates `< y` with respect to some basis `b`,
its norm is strictly less than `normBound abv b * y ^ dim S`.  -/
ClassGroup.norm_lt : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra R S] (abv : AbsoluteValue R ℤ) {ι : Type u_5} [inst_4 : DecidableEq ι] [inst_5 : Fintype ι]
  (bS : Module.Basis ι R S) {T : Type u_6} [inst_6 : Ring T] [inst_7 : LinearOrder T] [IsStrictOrderedRing T] (a : S)
  {y : T},
  (∀ (k : ι), ↑(abv ((bS.repr a) k)) < y) →
    ↑(abv ((Algebra.norm R) a)) < ↑(ClassGroup.normBound abv bS) * y ^ Fintype.card ι
-- Mathlib.Data.Nat.Dist
Nat.dist_eq_max_sub_min : ∀ {i j : ℕ}, i.dist j = max i j - min i j
-- Init.Data.UInt.Lemmas
UInt16.toNat_toUInt64 : ∀ (x : UInt16), x.toUInt64.toNat = x.toNat
-- Mathlib.Data.EReal.Operations
EReal.coe_add_top : ∀ (x : ℝ), ↑x + ⊤ = ⊤
-- Mathlib.AlgebraicGeometry.IdealSheaf.IrreducibleComponent
AlgebraicGeometry.Scheme.instIrreducibleSpaceCarrierCarrierCommRingCatIrreducibleComponent : ∀ (X : AlgebraicGeometry.Scheme) (Z : Set ↥X) (hZ : Z ∈ irreducibleComponents ↥X)
  [inst : AlgebraicGeometry.IsNoetherian X], IrreducibleSpace ↥(X.irreducibleComponent Z hZ)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_of_mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  l.contains k = false → k ∈ Std.DTreeMap.Const.insertManyIfNewUnit t l → k ∈ t
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.cobounded_sets : ∀ {α : Type u} [self : PseudoMetricSpace α], (Bornology.cobounded α).sets = {s | ∃ C, ∀ x ∈ sᶜ, ∀ y ∈ sᶜ, dist x y ≤ C}
-- Mathlib.Topology.Covering.Basic
/-- If `x` is evenly covered by `f`, then we can construct a trivialization of `f` at `x`.  -/
IsEvenlyCovered.toTrivialization : {E : Type u_1} →
  {X : Type u_2} →
    [inst : TopologicalSpace E] →
      [inst_1 : TopologicalSpace X] →
        {f : E → X} →
          {I : Type u_3} →
            [inst_2 : TopologicalSpace I] →
              {x : X} → [Nonempty I] → IsEvenlyCovered f x I → Bundle.Trivialization (↑(f ⁻¹' {x})) f
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- A codiscrete category is equivalent to its opposite category.  -/
CategoryTheory.Codiscrete.oppositeEquivalence : (A : Type u_1) → (CategoryTheory.Codiscrete A)ᵒᵖ ≌ CategoryTheory.Codiscrete A
-- Mathlib.Data.Analysis.Filter
/-- Construct a realizer for the sup of two filters  -/
Filter.Realizer.sup : {α : Type u_1} → {f g : Filter α} → f.Realizer → g.Realizer → (f ⊔ g).Realizer
-- Lean.Compiler.IR.CompilerM
_private.Lean.Compiler.IR.CompilerM.0.Lean.IR.exportIREntries.unsafe_7 : Array (Option Lean.PkgId) → Array Lean.EnvExtensionEntry
-- Init.Prelude
/-- The conditional function.

`cond c x y` is the same as `if c then x else y`, but optimized for a Boolean condition rather than
a decidable proposition. It can also be written using the notation `bif c then x else y`.

Just like `ite`, `cond` is declared `@[macro_inline]`, which causes applications of `cond` to be
unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and
only the selected branch is evaluated.
 -/
cond : {α : Sort u} → Bool → α → α → α
-- Mathlib.Analysis.Normed.Lp.lpHolder
/-- The natural pairing between `lp E p` and `lp F q` (for Hölder conjugate `p q : ℝ≥0∞`) with
values in a space `H` induced by a family of bilinear maps `B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H`.

This is given by `∑' i, B (e i) (f i)`.

In the special case when `B := (NormedSpace.inclusionInDoubleDual 𝕜 E).flip`, which is
definitionally the same as `B := ContinuousLinearMap.id 𝕜 (E →L[𝕜] 𝕜)`, this is the natural map
`lp (fun _ ↦ StrongDual 𝕜 E) p →L[𝕜] StrongDual 𝕜 (lp E q)`.
 -/
lp.dualPairing : {ι : Type u_1} →
  {𝕜 : Type u_2} →
    {E : ι → Type u_3} →
      {F : ι → Type u_4} →
        [inst : RCLike 𝕜] →
          [inst_1 : (i : ι) → NormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : (i : ι) → NormedAddCommGroup (F i)] →
                [inst_4 : (i : ι) → NormedSpace 𝕜 (F i)] →
                  (p q : ENNReal) →
                    {H : Type u_6} →
                      [inst_5 : NormedAddCommGroup H] →
                        [inst_6 : NormedSpace 𝕜 H] →
                          [CompleteSpace H] →
                            [inst_8 : Fact (1 ≤ p)] →
                              [inst_9 : Fact (1 ≤ q)] →
                                [p.HolderConjugate q] →
                                  (B : (i : ι) → E i →L[𝕜] F i →L[𝕜] H) →
                                    {K : NNReal} → (∀ (i : ι), ‖B i‖ ≤ ↑K) → ↥(lp E p) →L[𝕜] ↥(lp F q) →L[𝕜] H
-- Mathlib.Combinatorics.Quiver.SingleObj
_private.Mathlib.Combinatorics.Quiver.SingleObj.0.Quiver.SingleObj.listToPath.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (h_1 : Unit → motive []) (h_2 : (a : α) → (l : List α) → motive (a :: l)),
  (match [] with
    | [] => h_1 ()
    | a :: l => h_2 a l) =
    h_1 ()
-- Init.Data.SInt.Basic
instReprAtomInt8 : ReprAtom Int8
-- Mathlib.Algebra.Order.Module.Defs
SMulPosMono.lift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : SMul α β] [inst_4 : SMul α γ] (f : β → γ) [inst_5 : Zero β] [inst_6 : Zero γ] [SMulPosMono α γ],
  (∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂) → (∀ (a : α) (b : β), f (a • b) = a • f b) → f 0 = 0 → SMulPosMono α β
-- Init.Data.UInt.Lemmas
USize.toUInt64_ofBitVec : ∀ {b : BitVec System.Platform.numBits}, { toBitVec := b }.toUInt64 = { toBitVec := BitVec.setWidth 64 b }
-- Mathlib.Order.Interval.Set.UnorderedInterval
Monotone.mapsTo_uIcc : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Lattice β] {f : α → β} {a b : α},
  Monotone f → Set.MapsTo f (Set.uIcc a b) (Set.uIcc (f a) (f b))
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.monotone_strictMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (F : CategoryTheory.Functor C D), Monotone fun P => P.strictMap F
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.mk : {α : Type u} →
  [toSemiring : Lean.Grind.Semiring α] →
    [toNeg : Neg α] →
      [toSub : Sub α] →
        [intCast : IntCast α] →
          [zsmul : SMul ℤ α] →
            (∀ (a : α), -a + a = 0) →
              (∀ (a b : α), a - b = a + -b) →
                (∀ (i : ℤ) (a : α), -i • a = -(i • a)) →
                  autoParam (∀ (n : ℕ) (a : α), ↑n • a = n • a) Lean.Grind.Ring.zsmul_natCast_eq_nsmul._autoParam →
                    autoParam (∀ (n : ℕ), ↑(OfNat.ofNat n) = OfNat.ofNat n) Lean.Grind.Ring.intCast_ofNat._autoParam →
                      autoParam (∀ (i : ℤ), ↑(-i) = -↑i) Lean.Grind.Ring.intCast_neg._autoParam → Lean.Grind.Ring α
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxKeyD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) (size : ℕ) (k : α)
  (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (x : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : α) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_2 size k v l x
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `lt_mul_of_inv_mul_lt`.

---

**Alias** of the forward direction of `inv_mul_lt_iff_lt_mul`. -/
lt_mul_of_inv_mul_lt_left : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, b⁻¹ * a < c → a < b * c
-- Init.Data.Slice.Array.Lemmas
Array.start_toSubarray : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, (xs.toSubarray lo hi).start = min lo (min hi xs.size)
-- Mathlib.Data.Finset.SMulAntidiagonal
/-- `Finset.VAddAntidiagonal hs ht a` is the set of all pairs of an element in `s`
and an element in `t` whose vector addition yields `a`, but its construction requires proofs that
`s` and `t` are well-ordered.  -/
Finset.VAddAntidiagonal : {G : Type u_1} →
  {P : Type u_2} →
    [inst : VAdd G P] → {s : Set G} → {t : Set P} → (a : P) → (s.vaddAntidiagonal t a).Finite → Finset (G × P)
-- Mathlib.Tactic.MinImports
/-- `getSyntaxNodeKinds stx` takes a `Syntax` input `stx` and returns the `NameSet` of all the
`SyntaxNodeKinds` and all the identifiers contained in `stx`.  -/
Mathlib.Command.MinImports.getSyntaxNodeKinds : Lean.Syntax → Lean.NameSet
-- Mathlib.RingTheory.Localization.Away.Basic
IsLocalization.away_of_isIdempotentElem_of_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {e : R},
  IsIdempotentElem e →
    (∀ (x y : R), (algebraMap R S) x = (algebraMap R S) y ↔ e * x = e * y) →
      Function.Surjective ⇑(algebraMap R S) → IsLocalization.Away e S
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.addAction.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : AddMonoid α] [inst_1 : AddAction α β],
  Set.addAction = { toVAdd := Set.vadd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Init.Data.Order.LemmasExtra
Std.instTransOrdOfLawfulOrderOrdOfIsPreorder : ∀ {α : Type u} [inst : Ord α] [inst_1 : LE α] [Std.LawfulOrderOrd α] [Std.IsPreorder α], Std.TransOrd α
-- Mathlib.Data.Finmap
Finmap.replace.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (b : β a) (s : Finmap β),
  Finmap.replace a b s = s.liftOn (fun t => (AList.replace a b t).toFinmap) ⋯
-- Mathlib.RingTheory.Ideal.Prod
Ideal.prod_top_top : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S], ⊤.prod ⊤ = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_mono : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.IsSplitMono CategoryTheory.Limits.biprod.inl
-- Std.Data.TreeMap.Raw.Basic
/-- Compares two tree maps using Boolean equality on keys and values.

Returns `true` if the maps contain the same key-value pairs, `false` otherwise.
 -/
Std.TreeMap.Raw.beq : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [BEq β] → Std.TreeMap.Raw α β cmp → Std.TreeMap.Raw α β cmp → Bool
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.subset_closure : ∀ {M : Type u_1} [inst : Add M] {s : Set M}, s ⊆ ↑(AddSemigroupIdeal.closure s)
-- Lean.Message
Lean.MessageData.withNamingContext.inj : ∀ {a : Lean.NamingContext} {a_1 : Lean.MessageData} {a_2 : Lean.NamingContext} {a_3 : Lean.MessageData},
  Lean.MessageData.withNamingContext a a_1 = Lean.MessageData.withNamingContext a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Lean.Parser.Syntax
Lean.Parser.Syntax.sepBy : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Construct a morphism between categorical coproducts from a family of morphisms between the
factors.  -/
CategoryTheory.Limits.Sigma.map' : {β : Type w} →
  {α : Type w₂} →
    {C : Type u} →
      [inst : CategoryTheory.Category.{v, u} C] →
        {f : α → C} →
          {g : β → C} →
            [inst_1 : CategoryTheory.Limits.HasCoproduct f] →
              [inst_2 : CategoryTheory.Limits.HasCoproduct g] → (p : α → β) → ((a : α) → f a ⟶ g (p a)) → (∐ f ⟶ ∐ g)
-- Lean.Parser.Extra
Lean.Parser.scientificLit.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.UniformSpace.Defs
lift'_comp_uniformity : ∀ {α : Type ua} [inst : UniformSpace α], ((uniformity α).lift' fun s => s.comp s) = uniformity α