mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equiv.eq_1 : ∀ {ι' : Type u_2} {M' : Type u_7} [inst : AddCommMonoid M'] {ι : Type u_10} {R : Type u_11} {M : Type u_12}
  [inst_1 : Semiring R] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] (b : Module.Basis ι R M) [inst_4 : Module R M']
  (b' : Module.Basis ι' R M') (e : ι ≃ ι'), b.equiv b' e = b.repr ≪≫ₗ (b'.reindex e.symm).repr.symm
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.fst_intCast : ∀ {q : ℕ} (n : ℤ), (↑n).1 = ↑n
-- Mathlib.Analysis.Calculus.FDeriv.Norm
HasFDerivAt.hasFDerivAt_norm_smul_neg : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : StrongDual ℝ E} {x : E} {t : ℝ},
  t < 0 → HasFDerivAt (fun x => ‖x‖) f x → HasFDerivAt (fun x => ‖x‖) (-f) (t • x)
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- The category of R-modules has all limits.  -/
ModuleCat.hasLimitsOfSize : ∀ {R : Type u} [inst : Ring R] [UnivLE.{v, w}],
  CategoryTheory.Limits.HasLimitsOfSize.{t, v, w, max (w + 1) u} (ModuleCat R)
-- Mathlib.Analysis.Normed.Group.AddTorsor
nndist_eq_nnnorm_vsub : ∀ (V : Type u_2) {P : Type u_3} [inst : SeminormedAddCommGroup V] [inst_1 : PseudoMetricSpace P]
  [inst_2 : NormedAddTorsor V P] (x y : P), nndist x y = ‖x -ᵥ y‖₊
-- Mathlib.Analysis.Convex.Topology
/-- If `s` is a convex set, then `a • closure s + b • interior s ⊆ interior s` for all `0 ≤ a`,
`0 < b`, `a + b = 1`. See also `Convex.combo_self_interior_subset_interior` for a weaker version.  -/
Convex.combo_closure_interior_subset_interior : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E},
  Convex 𝕜 s → ∀ {a b : 𝕜}, 0 ≤ a → 0 < b → a + b = 1 → a • closure s + b • interior s ⊆ interior s
-- Mathlib.Analysis.Analytic.Basic
/-- `f` is analytic within `s` at `x` if it has a power series at `x` that converges on `𝓝[s] x`  -/
AnalyticWithinAt : (𝕜 : Type u_1) →
  {E : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → Set E → E → Prop
-- Mathlib.Algebra.Polynomial.Module.Basic
/-- `PolynomialModule.coeff` as an equiv.  -/
PolynomialModule.coeffEquiv : (R : Type u_2) →
  {M : Type u_3} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → PolynomialModule R M ≃ (ℕ →₀ M)
-- Mathlib.Topology.LocallyFinsupp
/-- Restriction of the zero function is the zero function.
 -/
Function.locallyFinsuppWithin.restrict_zero : ∀ {X : Type u_1} [inst : TopologicalSpace X] {Y : Type u_2} [inst_1 : Zero Y] {U V : Set X} (hV : V ⊆ U),
  Function.locallyFinsuppWithin.restrict 0 hV = 0
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiffAt.sub_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {s t : (x : M) → V x} {x₀ : M},
  ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, s x⟩) x₀ →
    ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, t x⟩) x₀ →
      ContMDiffAt I (I.prod (modelWithCornersSelf 𝕜 F)) n (fun x => ⟨x, (s - t) x⟩) x₀
-- Mathlib.MeasureTheory.Function.Egorov
MeasureTheory.Egorov.notConvergentSeq.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : PseudoEMetricSpace β] [inst_1 : Preorder ι] (f : ι → α → β)
  (g : α → β) (n : ℕ) (j : ι),
  MeasureTheory.Egorov.notConvergentSeq f g n j = ⋃ k, ⋃ (_ : j ≤ k), {x | (↑n)⁻¹ < edist (f k x) (g x)}
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- A `DistribMulActionHom` between two modules is a linear map.  -/
DistribMulActionHom.instLinearMapClassId : ∀ {R : Type u_1} {M : Type u_8} {M₃ : Type u_11} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₃]
  [inst_2 : Semiring R] [inst_3 : Module R M] [inst_4 : Module R M₃], LinearMapClass (M →+[R] M₃) R M M₃
-- Mathlib.RingTheory.LaurentSeries
RatFunc.algebraMap_apply_div : ∀ {F : Type u} [inst : Field F] (p q : Polynomial F),
  (algebraMap (RatFunc F) (LaurentSeries F))
      ((algebraMap (Polynomial F) (RatFunc F)) p / (algebraMap (Polynomial F) (RatFunc F)) q) =
    (algebraMap (Polynomial F) (LaurentSeries F)) p / (algebraMap (Polynomial F) (LaurentSeries F)) q
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn?.eq_1 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β), List.minOn? f [] = none
-- Mathlib.Data.Rat.Defs
Rat.mkRat_eq_divInt : ∀ (n : ℤ) (d : ℕ), mkRat n d = Rat.divInt n ↑d
-- Batteries.Data.MLList.Basic
/-- Take the first `n` elements, as a list inside the monad.  -/
MLList.takeAsList : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → ℕ → m (List α)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.le_of_epi : ∀ {n m : ℕ} (f : { len := n } ⟶ { len := m }) [CategoryTheory.Epi f], m ≤ n
-- Mathlib.Control.Functor.Multivariate
_private.Mathlib.Control.Functor.Multivariate.0.MvFunctor.g : {β : Type u} →
  (pp : β → Prop) →
    (n : ℕ) →
      (α : TypeVec.{u} n) →
        TypeVec.Arrow (fun i => { p_1 // α.PredLast pp p_1 }) fun i =>
          { p_1 // TypeVec.ofRepeat (α.PredLast' pp i p_1) }
-- Lean.Parser.Extra
Lean.Parser.antiquotNestedExpr.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.getKey?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.Equiv t₂ → t₁.getKey? k = t₂.getKey? k
-- Init.Data.Int.Basic
Int.ofNat_eq_coe : ∀ {n : ℕ}, Int.ofNat n = ↑n
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
HasStrictDerivAt.rpow : ∀ {x : ℝ} {f g : ℝ → ℝ} {f' g' : ℝ},
  HasStrictDerivAt f f' x →
    HasStrictDerivAt g g' x →
      0 < f x → HasStrictDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instAddAction_1 : {M : Type u_1} → {α : Type u_3} → [inst : AddMonoid M] → [AddAction M α] → AddAction M αᵒᵈ
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.StAct.pop.sizeOf_spec : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} [inst : SizeOf K] [inst_1 : (a : K) → SizeOf (Γ a)]
  [inst_2 : SizeOf σ] (a : σ → Option (Γ k) → σ), sizeOf (Turing.TM2to1.StAct.pop a) = 1
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mkPiRing_eq_iff : ∀ {R : Type u} {ι : Type v} {M : Type u_1} [inst : Fintype ι] [inst_1 : CommRing R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] [inst_4 : TopologicalSpace R] [inst_5 : TopologicalSpace M] [inst_6 : ContinuousMul R]
  [inst_7 : ContinuousSMul R M] {z₁ z₂ : M},
  ContinuousMultilinearMap.mkPiRing R ι z₁ = ContinuousMultilinearMap.mkPiRing R ι z₂ ↔ z₁ = z₂
-- Mathlib.Algebra.Algebra.StrictPositivity
isStrictlyPositive_algebraMap : ∀ {A : Type u_1} {𝕜 : Type u_2} [inst : Ring A] [inst_1 : PartialOrder A] [ZeroLEOneClass A] [inst_3 : Semifield 𝕜]
  [inst_4 : PartialOrder 𝕜] [inst_5 : Algebra 𝕜 A] [PosSMulMono 𝕜 A] {c : 𝕜},
  0 < c → IsStrictlyPositive ((algebraMap 𝕜 A) c)
-- Init.Data.Vector.Lemmas
Vector.getElem_mem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), xs[i] ∈ xs
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKey?_alterKey_eq_self : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  [inst_4 : Std.LawfulEqOrd α] {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.minKey? (Std.Internal.List.alterKey k f l) = some k ↔
      (f (Std.Internal.List.getValueCast? k l)).isSome = true ∧
        ∀ (k' : α), Std.Internal.List.containsKey k' l = true → (compare k k').isLE = true)
-- Init.Data.Slice.List.Lemmas
_private.Init.Data.Slice.List.Lemmas.0.Std.Slice.toList.eq_1 : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  (s : Std.Slice γ), s.toList = (Std.Slice.Internal.iter s).toList
-- Mathlib.FieldTheory.IsRealClosed.Basic
/-- **Alias** of the forward direction of `IsRealClosed.nonneg_iff_isSquare`. -/
IsSquare.of_nonneg : ∀ {R : Type u} [inst : Field R] [IsRealClosed R] [inst_2 : LinearOrder R] [IsStrictOrderedRing R] {x : R},
  0 ≤ x → IsSquare x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey_alter_self : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  [Inhabited α] {k : α} {f : Option (β k) → Option (β k)},
  m.WF → ∀ {hc : k ∈ m.alter k f}, (m.alter k f).getKey k hc = k
-- Mathlib.Order.Basic
Prod.swap_le_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] {x : α × β} {a : α} {b : β}, x.swap ≤ (b, a) ↔ x ≤ (a, b)
-- Lean.Meta.Tactic.Cases
Lean.Meta.Cases.Context.nminors : Lean.Meta.Cases.Context → ℕ
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.exists_mem_sup : ∀ {C : Type u_2} [inst : CommGroup C] {s t : Subgroup C} {P : C → Prop},
  (∃ x ∈ s ⊔ t, P x) ↔ ∃ x₁ ∈ s, ∃ x₂ ∈ t, P (x₁ * x₂)
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.image : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α},
  IsLowerSet s → ∀ (f : α ≃o β), IsLowerSet (⇑f '' s)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.shiftFunctor_obj_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type u_1} [inst_1 : AddCommGroup β] (s : β) (X : β → C)
  (t : β) (n : ℤ), (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift s C) n).obj X t = X (t + n • s)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_le_totalDegree : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (f : MvPolynomial σ R) (i : σ),
  MvPolynomial.degreeOf i f ≤ f.totalDegree
-- Mathlib.Algebra.Lie.Nilpotent
/-- A central extension of nilpotent Lie algebras is nilpotent.  -/
LieAlgebra.nilpotent_of_nilpotent_quotient : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L},
  I ≤ LieAlgebra.center R L → LieRing.IsNilpotent (L ⧸ I) → LieRing.IsNilpotent L
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Cat.freeMap_obj : ∀ {V : Type u_1} {W : Type u_2} [inst : Quiver V] [inst_1 : Quiver W] (F : V ⥤q W) (a : V),
  (CategoryTheory.Cat.freeMap F).obj a = F.obj a
-- Mathlib.Geometry.Manifold.Instances.Sphere
stereographic_apply : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E} (hv : ‖v‖ = 1)
  (x : ↑(Metric.sphere 0 1)), ↑(stereographic hv) x = (2 / (1 - inner ℝ v ↑x)) • (ℝ ∙ v)ᗮ.orthogonalProjectionOnto ↑x
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.sInf_toAddSubgroup : ∀ {R : Type u} [inst : NonAssocRing R] (s : Set (Subring R)), (sInf s).toAddSubgroup = ⨅ t ∈ s, t.toAddSubgroup
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCallsParams.item : Lean.Lsp.CallHierarchyIncomingCallsParams → Lean.Lsp.CallHierarchyItem
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldRev_eq_foldr_toArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {f : δ → (a : α) → β a → δ}
  {init : δ}, Std.DHashMap.Raw.Internal.foldRev f init ↑m = Array.foldr (fun a b => f b a.fst a.snd) init (↑m).toArray
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains_of_contains_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} {γ : α → Type w}
  [inst : Std.TransCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.ExtDTreeMap.filterMap f t).contains k = true → t.contains k = true
-- Mathlib.Algebra.Group.Hom.Defs
OneHom.one_apply : ∀ {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] (x : M), 1 x = 1
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.one : {R : Type u} → {M : Type v} → [One R] → [Zero M] → One (TrivSqZeroExt R M)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.getExprPos? : Lean.Syntax → Option String.Pos.Raw
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
PresheafOfModules.pullbackObjIsDefined_eq_top : ∀ {C D : Type u} [inst : CategoryTheory.SmallCategory C] [inst_1 : CategoryTheory.SmallCategory D]
  {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ RingCat} {S : CategoryTheory.Functor Cᵒᵖ RingCat}
  (φ : S ⟶ F.op.comp R), PresheafOfModules.pullbackObjIsDefined φ = ⊤
-- Mathlib.Topology.Order.Real
EReal.instT5Space : T5Space EReal
-- Mathlib.Algebra.AlgebraicCard
Algebraic.cardinalMk_lift_le_max : ∀ (R : Type u) (A : Type v) [inst : CommRing R] [IsDomain R] [inst_2 : CommRing A] [IsDomain A] [inst_4 : Algebra R A]
  [Module.IsTorsionFree R A],
  Cardinal.lift.{u, v} (Cardinal.mk { x // IsAlgebraic R x }) ≤
    max (Cardinal.lift.{v, u} (Cardinal.mk R)) Cardinal.aleph0
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The comparison morphism for the cokernel of `f`.  -/
CategoryTheory.Limits.cokernelComparison : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          {D : Type u₂} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
                (G : CategoryTheory.Functor C D) →
                  [G.PreservesZeroMorphisms] →
                    [inst_5 : CategoryTheory.Limits.HasCokernel f] →
                      [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)] →
                        CategoryTheory.Limits.cokernel (G.map f) ⟶ G.obj (CategoryTheory.Limits.cokernel f)
-- Init.WF
PSigma.instWellFoundedRelation : {α : Sort u} →
  {β : α → Sort v} →
    [ha : WellFoundedRelation α] → [hb : (a : α) → WellFoundedRelation (β a)] → WellFoundedRelation (PSigma β)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.size_union_of_not_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  (∀ a ∈ t₁, a ∉ t₂) → (t₁ ∪ t₂).size = t₁.size + t₂.size
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.fst : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_8} {F : Type u_9}
  [inst : NormedAddCommGroup E] [NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [NormedSpace ℝ F] {f : α → E × F},
  MeasureTheory.Integrable f μ → MeasureTheory.Integrable (fun x => (f x).1) μ
-- Mathlib.Algebra.Group.Basic
/-- If `n • x = 0`, then `m • x` is the same as `(m % n) • x`  -/
nsmul_eq_mod_nsmul : ∀ {M : Type u_4} [inst : AddMonoid M] {a : M} {n : ℕ} (m : ℕ), n • a = 0 → m • a = (m % n) • a
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.vecMul_surjective_of_invertible : ∀ {m : Type u} [inst : DecidableEq m] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Fintype m] (A : Matrix m m R)
  [Invertible A], Function.Surjective fun v => Matrix.vecMul v A
-- Mathlib.GroupTheory.Complement
Subgroup.IsComplement.equiv_fst_eq_one_of_mem_of_one_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G} (hST : Subgroup.IsComplement S T) {g : G} (h1 : 1 ∈ S),
  g ∈ T → (hST.equiv g).1 = ⟨1, h1⟩
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instAddCommGroup : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → AddCommGroup (ContIntertwiningMap π₁ π₂)
-- Mathlib.Logic.Basic
imp_or : ∀ {a b c : Prop}, a → b ∨ c ↔ (a → b) ∨ (a → c)
-- Mathlib.Algebra.Group.Action.Opposite
MulOpposite.op_smul_eq_op_smul_op : ∀ {M : Type u_1} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul Mᵐᵒᵖ α] [IsCentralScalar M α] (r : M) (a : α),
  MulOpposite.op (r • a) = MulOpposite.op r • MulOpposite.op a
-- Mathlib.MeasureTheory.Measure.Count
MeasureTheory.Measure.count_apply_finite : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSingletonClass α] (s : Set α) (hs : s.Finite),
  MeasureTheory.Measure.count s = ↑hs.toFinset.card
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.wp_liftWith_ReaderT_apply_eq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ρ α : Type u}
  {post : α → ρ → Pred} {epost : EPred} {r : ρ} (f : ({β : Type u} → ReaderT ρ m β → m β) → m α),
  Std.Internal.Do.wp (MonadControl.liftWith f) post epost r =
    Std.Internal.Do.wp (f fun {β} x => x.run r) (fun a => post a r) epost
-- Mathlib.MeasureTheory.OuterMeasure.Induced
/-- `trim` sends the supremum of a countable family of outer measures to the supremum
of the trimmed measures.  -/
MeasureTheory.OuterMeasure.trim_iSup : ∀ {α : Type u_1} [inst : MeasurableSpace α] {ι : Sort u_2} [Countable ι] (μ : ι → MeasureTheory.OuterMeasure α),
  (⨆ i, μ i).trim = ⨆ i, (μ i).trim
-- Mathlib.Data.Set.Lattice
Set.biUnion_pair : ∀ {α : Type u_1} {β : Type u_2} (a b : α) (s : α → Set β), ⋃ x ∈ {a, b}, s x = s a ∪ s b
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodAddEquivOfGenerator_symm_apply_zsmul : ∀ {G : Type u_2} [inst : AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ}
  (hn : Nat.card G = n) (i : ℤ), (zmodAddEquivOfGenerator hg hn).symm (i • g) = ↑i
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_alterKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k k' : α) (f : Option (β k) → Option (β k))
  (l : List ((a : α) × β a)) (hl : Std.Internal.List.DistinctKeys l)
  (hc : Std.Internal.List.containsKey k' (Std.Internal.List.alterKey k f l) = true),
  Std.Internal.List.getValueCast k' (Std.Internal.List.alterKey k f l) hc =
    if h : (k == k') = true then cast ⋯ ((f (Std.Internal.List.getValueCast? k l)).get ⋯)
    else Std.Internal.List.getValueCast k' l ⋯
-- Mathlib.Algebra.BigOperators.Group.Multiset.Defs
Multiset.prod_zero : ∀ {M : Type u_3} [inst : CommMonoid M], Multiset.prod 0 = 1
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyGED_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGED k fallback = t₂.getKeyGED k fallback
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
/-- Given an `A`-valued operation `Φ` on sections of a vector bundle `V` which is tensorial at `x`,
the construction `TensorialAt.mkHom` provides the associated continuous linear map `V x →L[𝕜] A`.  -/
TensorialAt.mkHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_5} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] →
                            {V : M → Type u_6} →
                              [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)] →
                                [inst_9 : (x : M) → AddCommGroup (V x)] →
                                  [inst_10 : (x : M) → Module 𝕜 (V x)] →
                                    [inst_11 : (x : M) → TopologicalSpace (V x)] →
                                      [inst_12 : FiberBundle F V] →
                                        {A : Type u_9} →
                                          [inst_13 : AddCommGroup A] →
                                            [inst_14 : Module 𝕜 A] →
                                              [inst_15 : VectorBundle 𝕜 F V] →
                                                [CompleteSpace 𝕜] →
                                                  [FiniteDimensional 𝕜 F] →
                                                    [ContMDiffVectorBundle 1 F V I] →
                                                      [inst_19 : TopologicalSpace A] →
                                                        [IsTopologicalAddGroup A] →
                                                          [ContinuousSMul 𝕜 A] →
                                                            (Φ : ((x : M) → V x) → A) →
                                                              (x : M) → TensorialAt I F Φ x → V x →L[𝕜] A
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isEmpty_toArray : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}, t.toArray.isEmpty = t.isEmpty
-- Mathlib.MeasureTheory.Measure.Haar.MulEquivHaarChar
MeasureTheory.mulEquivHaarChar_trans : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G] [inst_3 : BorelSpace G]
  [inst_4 : IsTopologicalGroup G] [inst_5 : LocallyCompactSpace G] {φ ψ : G ≃ₜ* G},
  MeasureTheory.mulEquivHaarChar (ψ.trans φ) = MeasureTheory.mulEquivHaarChar ψ * MeasureTheory.mulEquivHaarChar φ
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.image_vadd : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s : Finset β} {a : α},
  Finset.image (fun x => a +ᵥ x) s = a +ᵥ s
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.surjective_symm_of_source_eq_univ : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β), e.source = Set.univ → Function.Surjective ↑e.symm
-- Mathlib.Algebra.Group.Hom.Defs
/-- Makes a multiplicative inverse from a bijection which preserves multiplication.  -/
MulHom.inverse : {M : Type u_4} →
  {N : Type u_5} →
    [inst : Mul M] →
      [inst_1 : Mul N] → (f : M →ₙ* N) → (g : N → M) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → N →ₙ* M
-- Mathlib.Data.DFinsupp.Interval
DFinsupp.card_Ioc : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → DecidableEq (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [inst_3 : (i : ι) → Zero (α i)] [inst_4 : (i : ι) → LocallyFiniteOrder (α i)]
  (f g : Π₀ (i : ι), α i), (Finset.Ioc f g).card = ∏ i ∈ f.support ∪ g.support, (Finset.Icc (f i) (g i)).card - 1
-- Lean.Structure
/-- Returns the name of the auxiliary definition that defines the autoParam for the field, if any such definition exists.
This is not the inherited autoParam, but the one that is defined or overridden by this structure.
The effective autoParams are collected in the flat constructor.
 -/
Lean.getAutoParamFnForField? : Lean.Environment → Lean.Name → Lean.Name → Option Lean.Name
-- Lean.Elab.Tactic.Omega.OmegaM
/-- Return the `Expr` representing the list of atoms as a `Coeffs`.  -/
Lean.Elab.Tactic.Omega.atomsCoeffs : Lean.Elab.Tactic.Omega.OmegaM Lean.Expr
-- Mathlib.Algebra.Group.TypeTags.Basic
toAdd_mul : ∀ {α : Type u} [inst : Add α] (x y : Multiplicative α),
  Multiplicative.toAdd (x * y) = Multiplicative.toAdd x + Multiplicative.toAdd y
-- Mathlib.MeasureTheory.Group.Arithmetic
AddUnits.instMeasurableConstVAdd : ∀ {M : Type u_4} {β : Type u_5} [inst : MeasurableSpace β] [inst_1 : AddMonoid M] [inst_2 : AddAction M β]
  [MeasurableConstVAdd M β], MeasurableConstVAdd (AddUnits M) β