mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearIsometryEquiv.nnnorm_toContinuousLinearMap : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] [NontrivialTopology E] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_7 : RingHomInvPair σ₁₂ σ₂₁] [inst_8 : RingHomInvPair σ₂₁ σ₁₂] [inst_9 : RingHomIsometric σ₁₂]
  (e : E ≃ₛₗᵢ[σ₁₂] F), ‖↑↑e‖₊ = 1
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.toIdeal_iInf : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜] {κ : Sort u_4}
  (s : κ → HomogeneousIdeal 𝒜), (⨅ i, s i).toIdeal = ⨅ i, (s i).toIdeal
-- Std.Do.WP.SimpLemmas
Std.Do.WP.get_EStateM : ∀ {ε σ : Type u_1} {Q : Std.Do.PostCond σ (Std.Do.PostShape.except ε (Std.Do.PostShape.arg σ Std.Do.PostShape.pure))},
  (Std.Do.wp MonadStateOf.get).apply Q = fun s => Q.1 s s
-- Init.Control.State
/-- Fails with a recoverable error. The state is rolled back on error recovery.
 -/
StateT.failure : {σ : Type u} → {m : Type u → Type v} → [Alternative m] → {α : Type u} → StateT σ m α
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Fractional operation is a finite unordered collection of D^m → D possibly with duplicates.  -/
FractionalOperation : Type u_3 → ℕ → Type u_3
-- Lean.Elab.Term.TermElabM
_private.Lean.Elab.Term.TermElabM.0.Lean.Elab.Term.FixedTermElabRefPointed : NonemptyType
-- Mathlib.Order.Filter.IsBounded
Filter.isBoundedUnder_iff_eventually_bddBelow : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {f : Filter β} {u : β → α},
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) f u ↔ ∃ s, BddBelow (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `DifferentiableOn.mul` -/
DifferentiableOn.fun_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {𝔸 : Type u_5} [inst_3 : NormedRing 𝔸] [inst_4 : NormedAlgebra 𝕜 𝔸]
  {a b : E → 𝔸}, DifferentiableOn 𝕜 a s → DifferentiableOn 𝕜 b s → DifferentiableOn 𝕜 (fun i => a i * b i) s
-- Mathlib.NumberTheory.NumberField.Units.Regulator
NumberField.Units.basisOfIsMaxRank_fundSystem : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.Units.basisOfIsMaxRank ⋯ =
    Module.Basis.ofZLatticeBasis ℝ (NumberField.Units.unitLattice K) (NumberField.Units.basisUnitLattice K)
-- Mathlib.Order.Filter.Subsingleton
/-- A filter is a subsingleton iff it is equal to `⊥` or to `pure a` for some `a`.  -/
Filter.subsingleton_iff_bot_or_pure : ∀ {α : Type u_1} {l : Filter α}, l.Subsingleton ↔ l = ⊥ ∨ ∃ a, l = pure a
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.limplies_insert : ∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  Std.Tactic.BVDecide.LRAT.Internal.Limplies (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (f.insert c) f
-- Init.Data.Vector.Attach
Vector.unattach_mk : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {xs : Array { x // p x }} {h : xs.size = n},
  (Vector.mk xs h).unattach = Vector.mk xs.unattach ⋯
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_inj : ∀ {z w : Complex.UnitDisc}, ↑z = ↑w ↔ z = w
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.isoAdd'_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {A : Type u_4} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] {a b c ab bc abc : A}
  (ea : (CategoryTheory.shiftFunctor C a).comp F ≅ F.comp (CategoryTheory.shiftFunctor D a))
  (eb : (CategoryTheory.shiftFunctor C b).comp F ≅ F.comp (CategoryTheory.shiftFunctor D b))
  (ec : (CategoryTheory.shiftFunctor C c).comp F ≅ F.comp (CategoryTheory.shiftFunctor D c)) (hab : a + b = ab)
  (hbc : b + c = bc) (h : a + b + c = abc),
  CategoryTheory.Functor.CommShift.isoAdd' ⋯ (CategoryTheory.Functor.CommShift.isoAdd' hab ea eb) ec =
    CategoryTheory.Functor.CommShift.isoAdd' ⋯ ea (CategoryTheory.Functor.CommShift.isoAdd' hbc eb ec)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.ExactFunctor.whiskeringRight_obj_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 : D ⥤ₑ E) (X : C ⥤ₑ D),
  (((CategoryTheory.ExactFunctor.whiskeringRight C D E).obj F).obj X).obj = X.obj.comp F.obj
-- Mathlib.Topology.MetricSpace.HausdorffDimension
/-- **Alias** of `dimH_countable`. -/
Set.Countable.dimH_zero : ∀ {X : Type u_2} [inst : EMetricSpace X] {s : Set X}, s.Countable → dimH s = 0
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.symm : ∀ {p q : ENNReal} [hpq : p.HolderConjugate q], q.HolderConjugate p
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- A complex inner product implies a real inner product. This cannot be an instance since it
creates a diamond with `PiLp.innerProductSpace` because `re (sum i, ⟪x i, y i⟫)` and
`sum i, re ⟪x i, y i⟫` are not defeq.  -/
InnerProductSpace.complexToReal : {G : Type u_4} → [inst : SeminormedAddCommGroup G] → [InnerProductSpace ℂ G] → InnerProductSpace ℝ G
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.normSq_denom_ne_zero : ∀ (g : GL (Fin 2) ℝ) {z : ℂ}, z.im ≠ 0 → Complex.normSq (UpperHalfPlane.denom g z) ≠ 0
-- Mathlib.Topology.Category.LightProfinite.Basic
instFullLightDiagramProfiniteLightDiagramToProfinite : lightDiagramToProfinite.Full
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The L-series of the convolution product `f ⍟ g` of two sequences `f` and `g`
equals the product of their L-series, assuming both L-series converge.  -/
LSeries_convolution' : ∀ {f g : ℕ → ℂ} {s : ℂ},
  LSeriesSummable f s → LSeriesSummable g s → LSeries (LSeries.convolution f g) s = LSeries f s * LSeries g s
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_transpose : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : (i : o) → Matrix (m' i) (n' i) α),
  (Matrix.blockDiagonal' M).transpose = Matrix.blockDiagonal' fun k => (M k).transpose
-- Mathlib.RingTheory.TensorProduct.Basic
Algebra.TensorProduct.includeLeft_apply : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : CommSemiring S] [inst_6 : Algebra S A]
  [inst_7 : SMulCommClass R S A] (a : A), Algebra.TensorProduct.includeLeft a = a ⊗ₜ[R] 1
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RicSliceData.mk.injEq : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (treeMap : Std.DTreeMap.Internal.Impl α β) (range : Std.Ric α)
  (treeMap_1 : Std.DTreeMap.Internal.Impl α β) (range_1 : Std.Ric α),
  ({ treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 }) =
    (treeMap = treeMap_1 ∧ range = range_1)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int8.maxValueSealed : Int8
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.x_sub_y_dvd_pow_lem : ∀ (y2 y1 y0 yn1 yn0 xn1 xn0 ay a2 : ℤ),
  (a2 * yn1 - yn0) * ay + y2 - (a2 * xn1 - xn0) = y2 - a2 * y1 + y0 + a2 * (yn1 * ay + y1 - xn1) - (yn0 * ay + y0 - xn0)
-- Mathlib.Data.Tree.Basic
/-- The height - length of the longest path from the root - of a binary tree  -/
BinaryTree.height : {α : Type u} → BinaryTree α → ℕ
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` preserves the limit of shape `J` if it creates these limits and `D` has them.  -/
CategoryTheory.preservesLimitOfShape_of_createsLimitsOfShape_and_hasLimitsOfShape : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C D)
  [CategoryTheory.CreatesLimitsOfShape J F] [CategoryTheory.Limits.HasLimitsOfShape J D],
  CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAt.property : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] {H : Type u_7}
  [inst_5 : TopologicalSpace H] {G : Type u_9} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M]
  {N : Type u_13} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (h : Manifold.IsImmersionAt I J n f x),
  Manifold.LiftSourceTargetPropertyAt I J n f x (Manifold.ImmersionAtProp h.complement I J M N)
-- Mathlib.Analysis.Complex.UpperHalfPlane.FunctionsBoundedAtInfty
UpperHalfPlane.tendsto_smul_atImInfty : ∀ {g : GL (Fin 2) ℝ}, ↑g 1 0 = 0 → Filter.Tendsto (fun τ => g • τ) UpperHalfPlane.atImInfty UpperHalfPlane.atImInfty
-- Mathlib.Order.Bounds.Image
/-- A monotone map sends a greatest element of a set to a greatest element of its
image.  -/
Monotone.map_isGreatest : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Monotone f → ∀ {a : α} {s : Set α}, IsGreatest s a → IsGreatest (f '' s) (f a)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.id_f₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  (CategoryTheory.ShortComplex.SnakeInput.Hom.id S).f₁ = CategoryTheory.CategoryStruct.id S.L₁
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `FunLike.coe_smul`. -/
ProbabilityTheory.Kernel.coe_nsmul : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `AddMonoidAlgebra.coeff_one_zero`. -/
AddMonoidAlgebra.coeff_zero_zero : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : Zero M], (AddMonoidAlgebra.coeff 1) 0 = 1
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_toSlice : ∀ {s : String}, s.toSlice.isEmpty = s.isEmpty
-- Std.Internal.UV.UDP
/-- Receives data from an UDP socket. `size` is for the maximum bytes to receive. The promise resolves
when some data is available or an error occurs. If the socket has not been previously bound with `bind`,
it is automatically bound to `0.0.0.0` (all interfaces) with a random port.
 -/
Std.Internal.UV.UDP.Socket.getPeerName : Std.Internal.UV.UDP.Socket → IO Std.Net.SocketAddress
-- Std.Time.Time.Unit.Minute
Std.Time.Minute.instDecidableLeOrdinal : {x y : Std.Time.Minute.Ordinal} → Decidable (x ≤ y)
-- Lean.Meta.Tactic.Grind.PP
_private.Lean.Meta.Tactic.Grind.PP.0.Lean.Meta.Grind.Result.cast.sizeOf_spec : sizeOf Lean.Meta.Grind.Result.cast✝ = 1
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.coe_preOmega : ⇑Ordinal.preOmega = Ordinal.enumOrd {x | x.IsInitial}
-- Init.Data.Iterators.Basic
/-- Asserts that a certain output value could plausibly be emitted by the given iterator in its next
step.
 -/
Std.Iter.IsPlausibleOutput : {α β : Type w} → [Std.Iterator α Id β] → Std.Iter β → β → Prop
-- Init.Data.Array.Find
Array.find?_eq_getElem?_findIdx : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.find? p xs = xs[Array.findIdx p xs]?
-- Lean.Declaration
Lean.Declaration.mutualDefnDecl.inj : ∀ {defns defns_1 : List Lean.DefinitionVal},
  Lean.Declaration.mutualDefnDecl defns = Lean.Declaration.mutualDefnDecl defns_1 → defns = defns_1
-- Std.Http.Server.Config
/-- Maximum length of chunk extension value (default: 256 bytes)
 -/
Std.Http.Config.maxChunkExtValueLength : Std.Http.Config → ℕ
-- Mathlib.Topology.Instances.CantorSet
quarter_mem_preCantorSet : ∀ (n : ℕ), 1 / 4 ∈ preCantorSet n
-- Mathlib.Order.InitialSeg
_private.Mathlib.Order.InitialSeg.0.collapseF.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder β s] (f : r ↪r s),
  collapseF✝ f =
    IsWellFounded.fix r fun a IH =>
      have H := ⋯;
      ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩
-- Lean.Level
Lean.Level.mkNaryMax : List Lean.Level → Lean.Level
-- Mathlib.Topology.LocallyFinite
locallyFinite_sum : ∀ {ι : Type u_1} {ι' : Type u_2} {X : Type u_4} [inst : TopologicalSpace X] {f : ι ⊕ ι' → Set X},
  LocallyFinite f ↔ LocallyFinite (f ∘ Sum.inl) ∧ LocallyFinite (f ∘ Sum.inr)
-- Mathlib.GroupTheory.MonoidLocalization.Away
AddLocalization.Away.negSelf.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] (x : M), AddLocalization.Away.negSelf x = AddLocalization.mk 0 ⟨x, ⋯⟩
-- Mathlib.RingTheory.PowerSeries.Trunc
PowerSeries.trunc_C : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ) (a : R), (PowerSeries.trunc (n + 1)) (PowerSeries.C a) = Polynomial.C a
-- Lean.Meta.LitValues
/-- Return `some i` if `e` `OfNat.ofNat`-application encoding a rational, or `Neg.neg`-application of one,
or a division.
 -/
Lean.Meta.getRatValue? : Lean.Expr → Lean.MetaM (Option ℚ)
-- Mathlib.Algebra.Field.IsField
/-- Fields are commutative.  -/
IsField.mul_comm : ∀ {R : Type u} [inst : Semiring R], IsField R → ∀ (x y : R), x * y = y * x
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.zeroLocus_pow : ∀ {R : Type u} [inst : CommSemiring R] (I : Ideal R) {n : ℕ},
  n ≠ 0 → PrimeSpectrum.zeroLocus ↑(I ^ n) = PrimeSpectrum.zeroLocus ↑I
-- Mathlib.CategoryTheory.Category.Pairwise
_private.Mathlib.CategoryTheory.Category.Pairwise.0.CategoryTheory.instFintypePairwise.match_5.eq_1 : ∀ (ι : Type u_1) (motive : CategoryTheory.Pairwise ι → Sort u_2) (a : ι)
  (h_1 : (a : ι) → motive (CategoryTheory.Pairwise.single a))
  (h_2 : (a a_1 : ι) → motive (CategoryTheory.Pairwise.pair a a_1)),
  (match CategoryTheory.Pairwise.single a with
    | CategoryTheory.Pairwise.single a => h_1 a
    | CategoryTheory.Pairwise.pair a a_1 => h_2 a a_1) =
    h_1 a
-- Mathlib.Order.Interval.Finset.Basic
Finset.Iic_sdiff_Ioc_self_of_le : ∀ {α : Type u_2} {a b : α} [inst : LinearOrder α] [inst_1 : LocallyFiniteOrder α] [inst_2 : LocallyFiniteOrderBot α],
  a ≤ b → Finset.Iic b \ Finset.Ioc a b = Finset.Iic a
-- Mathlib.Algebra.Category.MonCat.Limits
MonCat.forget_createsLimitsOfShape : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] → CategoryTheory.CreatesLimitsOfShape J (CategoryTheory.forget MonCat)
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.update_inv : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Inv (f i)] [inst_1 : DecidableEq I] (f₁ : (i : I) → f i) (i : I)
  (x₁ : f i), Function.update f₁⁻¹ i x₁⁻¹ = (Function.update f₁ i x₁)⁻¹
-- Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal
SSet.Truncated.rightExtensionInclusion_left : ∀ (X : SSet) (n : ℕ), (SSet.Truncated.rightExtensionInclusion X n).left = X
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.getEntryGT.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    [inst : Ord α] →
      (k : α) →
        (motive : (x : Std.DTreeMap.Internal.Impl α β) → x.Ordered → (∃ a ∈ x, compare a k = Ordering.gt) → Sort u_3) →
          (x : Std.DTreeMap.Internal.Impl α β) →
            (x_1 : x.Ordered) →
              (x_2 : ∃ a ∈ x, compare a k = Ordering.gt) →
                ((x : Std.DTreeMap.Internal.Impl.leaf.Ordered) →
                    (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.leaf, compare a k = Ordering.gt) →
                      motive Std.DTreeMap.Internal.Impl.leaf x he) →
                  ((size : ℕ) →
                      (ky : α) →
                        (y : β ky) →
                          (l r : Std.DTreeMap.Internal.Impl α β) →
                            (ho : (Std.DTreeMap.Internal.Impl.inner size ky y l r).Ordered) →
                              (he : ∃ a ∈ Std.DTreeMap.Internal.Impl.inner size ky y l r, compare a k = Ordering.gt) →
                                motive (Std.DTreeMap.Internal.Impl.inner size ky y l r) ho he) →
                    motive x x_1 x_2
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_of_right_mem : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} (x : P) {y : P}, y ∈ s → s.WOppSide x y
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.zpow_apply : ∀ {M : Type u_1} (r : ℤ) (l : Mathlib.Tactic.FieldSimp.NF M),
  l ^ r =
    List.map
      (fun x =>
        match x with
        | (a, x) => (r * a, x))
      l
-- Mathlib.Tactic.Cases
/-- `cases' x`, where the variable `x` has inductive type `t`, splits the main goal,
producing one goal for each constructor of `t`, in which `x` is replaced by that constructor
applied to newly introduced variables. This is a backwards-compatible variant of the
`cases` tactic in Lean 4 core.

Prefer `cases`, `rcases`, or `obtain` when possible, because these tactics promote
structured proofs.

* `cases' x with n1 n2 ...` names the arguments to the constructors. This is the main difference
  with `cases` in core Lean.
* `cases' e`, where `e` is an expression instead of a variable, generalizes `e` in the goal,
  and then performs induction on the resulting variable.
* `cases' h : e`, where `e` is an expression instead of a variable, generalizes `e` in the goal,
  and then splits by cases on the resulting variable, adding to each goal the hypothesis
  `h : e = _` where `_` is the constructor instance.
* `cases' x using r` uses `r` as the case matching rule. Here `r` should be a term whose result type
  is of the form `C t1 t2 ...`, where `C` is a bound variable and `t1`, `t2`, ... (if present) are
  bound variables.

Example:
```
example (h : p ∨ q) : q ∨ p := by
  cases' h with hp hq
  · exact Or.inr hp
  · exact Or.inl hq

-- Though the following equivalent spellings should be preferred
example (h : p ∨ q) : q ∨ p := by
  cases h with
  | inl hp => exact Or.inr hp
  | inr hq => exact Or.inl hq

example (h : p ∨ q) : q ∨ p := by
  rcases h with hp | hq
  · exact Or.inr hp
  · exact Or.inl hq
```
 -/
Mathlib.Tactic.cases' : Lean.ParserDescr
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- `Total V` is the type of _all_ arrows of `V`.  -/
Quiver.Total : (V : Type u) → [Quiver V] → Type (max u v)
-- Mathlib.LinearAlgebra.Dimension.Constructions
Module.finrank_baseChange : ∀ {R : Type u} {S : Type u'} {M' : Type v'} [inst : Semiring R] [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid M']
  [StrongRankCondition R] [StrongRankCondition S] [inst_5 : Module S M'] [Module.Free S M'] [inst_7 : Algebra S R],
  Module.finrank R (TensorProduct S R M') = Module.finrank S M'
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Slice.Model.revPositionsFrom.eq_1 : ∀ {s : String.Slice} (p : s.Pos),
  String.Slice.Model.revPositionsFrom p =
    if h : p = s.startPos then [] else ⟨p.prev h, ⋯⟩ :: String.Slice.Model.revPositionsFrom (p.prev h)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
Real.iteratedDeriv_even_cosh : ∀ (n : ℕ), iteratedDeriv (2 * n) Real.cosh = Real.cosh
-- Lean.Message
Lean.TraceData : Type
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.ofRepresentableBy_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X),
  CategoryTheory.MonObj.one = α.homEquiv'.symm 1
-- Mathlib.Order.Max
/-- **Alias** of the reverse direction of `isMax_toDual_iff`. -/
IsMin.toDual : ∀ {α : Type u_1} [inst : LE α] {a : α}, IsMin a → IsMax (OrderDual.toDual a)
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.one_div_ne_zero' : ∀ {p q r : NNReal}, p.HolderTriple q r → 1 / r ≠ 0
-- Lean.Parser.Do
Lean.Parser.Term.letIdDeclNoBinders.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getEntry?.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (a a_1 : α) (b : β a_1) (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getEntry? a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if (a_1 == a) = true then some ⟨a_1, b⟩ else Std.DHashMap.Internal.AssocList.getEntry? a es
-- Std.Http.Data.Body.Any
/-- A type-erased body handle. Operations are stored as closures, making it open to any body type
that implements `Http.Body`.
 -/
Std.Http.Body.Any : Type
-- Mathlib.Data.Nat.Totient
/-- Euler's totient function is only odd at `1` or `2`.  -/
Nat.odd_totient_iff : ∀ {n : ℕ}, Odd n.totient ↔ n = 1 ∨ n = 2
-- Init.Data.UInt.Lemmas
UInt32.add_assoc : ∀ (a b c : UInt32), a + b + c = a + (b + c)
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {he : t ≠ ∅}, t.get! (t.max he) = t.max he
-- Mathlib.Analysis.Convex.StrictConvexBetween
Wbtw.dist_le_max_dist : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [StrictConvexSpace ℝ V]
  [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (p : P) {p₁ p₂ p₃ : P},
  Wbtw ℝ p₁ p₂ p₃ → dist p₂ p ≤ max (dist p₁ p) (dist p₃ p)
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.image_closedEBall : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β) (x : α)
  (r : ENNReal), ⇑h '' Metric.closedEBall x r = Metric.closedEBall (h x) r
-- Mathlib.Order.Grade
/-- A `Fin n`-graded order is also `ℕ`-graded. We do not mark this an instance because `n` is not
inferable.  -/
GradeMinOrder.finToNat : {α : Type u_3} → [inst : Preorder α] → (n : ℕ) → [GradeMinOrder (Fin n) α] → GradeMinOrder ℕ α
-- Mathlib.Algebra.Group.ULift
ULift.addCancelMonoid.eq_1 : ∀ {α : Type u} [inst : AddCancelMonoid α],
  ULift.addCancelMonoid = Function.Injective.addCancelMonoid ⇑Equiv.ulift ⋯ ⋯ ⋯ ⋯
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.trW.mk' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderShift ℤ] {T : CategoryTheory.Pretriangulated.Triangle C},
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles → P T.obj₁ → P.trW T.mor₂
-- Mathlib.Order.WithBot
WithBot.toDual_le_iff : ∀ {α : Type u_1} [inst : LE α] {x : WithBot α} {y : WithTop αᵒᵈ}, WithBot.toDual x ≤ y ↔ WithTop.ofDual y ≤ x
-- Lean.Elab.Tactic.Omega.Core
/-- Print a `Justification` as an indented tree structure.  -/
Lean.Elab.Tactic.Omega.Justification.toString : {s : Lean.Omega.Constraint} → {x : Lean.Omega.Coeffs} → Lean.Elab.Tactic.Omega.Justification s x → String
-- Mathlib.RingTheory.MvPowerSeries.Rename
_private.Mathlib.RingTheory.MvPowerSeries.Rename.0.MvPowerSeries.renameFunAux' : ∀ {σ : Type u_1} {τ : Type u_2} (f : σ → τ) [inst : Filter.TendstoCofinite f] [inst_1 : DecidableEq τ] (x : τ →₀ ℕ),
  {p | p.1 ∈ Finset.HasAntidiagonal.antidiagonal x ∧ p.2 ∈ ⋯.toFinset ×ˢ ⋯.toFinset}.Finite
-- Mathlib.Topology.Algebra.Support
mulTSupport_fun_one : ∀ {X : Type u_1} {α : Type u_2} [inst : One α] [inst_1 : TopologicalSpace X], (mulTSupport fun x => 1) = ∅
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.comap_mono : ∀ {α : Type u_2} {γ : Type u_3} {f : α → γ}, Monotone fun u => UniformSpace.comap f u