mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.IsQuasiInverse.equiv_of_left : ∀ {K : Type u_1} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V₂] [inst_2 : Module K V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : Module K V₃] {u u' : V₃ →ₗ[K] V₂} {v v' : V₂ →ₗ[K] V₃},
  u.IsQuasiInverse v → u'.IsQuasiInverse v' → u ≈ u' → v ≈ v'
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain_sum : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Semiring S] (f : M → N)
  (x : AddMonoidAlgebra S M) (v : M → S → AddMonoidAlgebra R M),
  AddMonoidAlgebra.mapDomain f (x.coeff.sum v) = x.coeff.sum fun a b => AddMonoidAlgebra.mapDomain f (v a b)
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Cauchy–Schwarz inequality with norm  -/
InnerProductSpace.Core.norm_inner_le_norm : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F), ‖inner 𝕜 x y‖ ≤ ‖x‖ * ‖y‖
-- Mathlib.Data.Semiquot
Semiquot.mem_pure : ∀ {α : Type u_1} {a b : α}, a ∈ pure b ↔ a = b
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.add : {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₂] → [ContinuousAdd M₂] → Add (M₁ →SL[σ₁₂] M₂)
-- Mathlib.Topology.Semicontinuity.Hemicontinuity
upperHemicontinuous_iff_forall_isOpen : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] {f : α → Set β} [inst_1 : TopologicalSpace β],
  UpperHemicontinuous f ↔ ∀ (x : α) (u : Set β), IsOpen u → f x ⊆ u → ∀ᶠ (x' : α) in nhds x, f x' ⊆ u
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.IsBasis.exists_iSup_eq : ∀ {X : Type u} [inst : TopologicalSpace X] {ι : Type u_5} {U : ι → TopologicalSpace.Opens X},
  TopologicalSpace.Opens.IsBasis (Set.range U) → ∀ (W : TopologicalSpace.Opens X), ∃ κ a, W = ⨆ k, U (a k)
-- Mathlib.MeasureTheory.Function.EssSup
ENNReal.essSup_const_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal} {a : ENNReal},
  essSup (fun x => a * f x) μ = a * essSup f μ
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_eq_omega0 : ∀ {a : Cardinal.{u_1}}, a.ord = Ordinal.omega0 ↔ a = Cardinal.aleph0
-- Mathlib.Topology.VectorBundle.Riemannian
/-- A continuous Riemannian metric is in particular a Riemannian metric.  -/
Bundle.ContinuousRiemannianMetric.toRiemannianMetric : {B : Type u_4} →
  [inst : TopologicalSpace B] →
    {F : Type u_5} →
      [inst_1 : NormedAddCommGroup F] →
        [inst_2 : NormedSpace ℝ F] →
          {E : B → Type u_6} →
            [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] →
              [inst_4 : (b : B) → TopologicalSpace (E b)] →
                [inst_5 : (b : B) → AddCommGroup (E b)] →
                  [inst_6 : (b : B) → Module ℝ (E b)] →
                    [inst_7 : FiberBundle F E] →
                      [inst_8 : VectorBundle ℝ F E] → Bundle.ContinuousRiemannianMetric F E → Bundle.RiemannianMetric E
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.isOpenMap_iff : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y}, IsOpenQuotientMap f → ∀ {g : Y → Z}, IsOpenMap g ↔ IsOpenMap (g ∘ f)
-- Mathlib.Data.Set.Basic
Set.union_subset : ∀ {α : Type u} {s t r : Set α}, s ⊆ r → t ⊆ r → s ∪ t ⊆ r
-- Mathlib.Topology.Constructions
instNoncompactSpaceMultiplicative : ∀ {X : Type u} [inst : TopologicalSpace X] [NoncompactSpace X], NoncompactSpace (Multiplicative X)
-- Init.Data.String.Pattern.Basic
/-- Checks whether the slice ends with the pattern.
   -/
String.Slice.Pattern.BackwardPattern.endsWith : {ρ : Type} → (pat : ρ) → [self : String.Slice.Pattern.BackwardPattern pat] → String.Slice → Bool
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- The equalizer of two R-algebra homomorphisms  -/
AlgHom.equalizer : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Semiring B] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → (A →ₐ[R] B) → Subalgebra R A
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_closure_of_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {s : Set R} {x : R}, x ∈ s → x ∈ NonUnitalSubsemiring.closure s
-- Mathlib.CategoryTheory.Monad.Basic
/-- Transport a comonad structure on a functor along an isomorphism of functors.  -/
CategoryTheory.Comonad.transport : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C C} → (T : CategoryTheory.Comonad C) → (T.toFunctor ≅ F) → CategoryTheory.Comonad C
-- Init.Prelude
/-- Boolean negation, also known as Boolean complement. `not x` can be written `!x`.

This is a function that maps the value `true` to `false` and the value `false` to `true`. The
propositional connective is `Not : Prop → Prop`.


Conventions for notations in identifiers:

 * The recommended spelling of `!` in identifiers is `not`. -/
Bool.not : Bool → Bool
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- Each function of a family equicontinuous on `S` is continuous on `S`.  -/
EquicontinuousOn.continuousOn : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {F : ι → X → α}
  {S : Set X}, EquicontinuousOn F S → ∀ (i : ι), ContinuousOn (F i) S
-- Mathlib.Topology.Compactification.StoneCech
/-- The extension of a continuous function from `α` to a compact
Hausdorff space `β` to the Stone-Čech compactification of `α`.
This extension implements the universal property of this compactification.  -/
stoneCechExtend : {α : Type u} →
  [inst : TopologicalSpace α] →
    {β : Type v} →
      [inst_1 : TopologicalSpace β] → [T2Space β] → {g : α → β} → Continuous g → [CompactSpace β] → StoneCech α → β
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- A type synonym, to be used for `Measure α`, `FiniteMeasure α`, or `ProbabilityMeasure α`,
when they are to be equipped with the Lévy-Prokhorov distance.  -/
MeasureTheory.LevyProkhorov : Type u_2 → Type u_2
-- Qq.Match
Qq.Impl.mkQqLets : {γ : Q(Type)} →
  (decls : List Qq.Impl.PatVarDecl) →
    (have a := Qq.Impl.mkIsDefEqType decls;
      Q(«$a»)) →
      Lean.Elab.TermElabM Q(«$γ») → Lean.Elab.TermElabM Q(«$γ»)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.range_map_nonempty : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] (N : Submodule R M), (Set.range fun ϕ => Submodule.map ϕ N).Nonempty
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.isLittleO_self_div_log_id : (fun n => ↑n / Real.log ↑n ^ 2) =o[Filter.atTop] fun n => ↑n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_eq_isEmpty_erase_and_not_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] (k : α),
  t.isEmpty = ((t.erase k).isEmpty && !t.contains k)
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.lift_le_continuum : ∀ {c : Cardinal.{u}}, Cardinal.lift.{v, u} c ≤ Cardinal.continuum ↔ c ≤ Cardinal.continuum
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.isLocalizationMap : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (self : S.LocalizationMap N), S.IsLocalizationMap self.toFun
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.normalClosure_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G] {s : Set G}, Subgroup.normalClosure s = ⊥ ↔ s ⊆ {1}
-- Mathlib.RingTheory.Coalgebra.Quotient
Submodule.IsCoideal.map_mkQ_comul_eq_zero : ∀ {R : Type u_1} {C : Type u_2} {inst : CommRing R} {inst_1 : AddCommGroup C} {inst_2 : Module R C}
  {inst_3 : CoalgebraStruct R C} {I : Submodule R C} [self : I.IsCoideal] ⦃x : C⦄,
  x ∈ I → (TensorProduct.map I.mkQ I.mkQ) (CoalgebraStruct.comul x) = 0
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.value : Lean.Elab.PartialFixpoint.EqnInfo → Lean.Expr
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCancelMonoid : {α : Type u_1} → [AddCancelMonoid α] → AddCancelMonoid αᵃᵒᵖ
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.length_dropLast_add_one : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, ¬p.Nil → p.dropLast.length + 1 = p.length
-- Lean.Meta.Tactic.Grind.Split
Lean.Meta.Grind.SplitCandidateWithAnchor.mk.injEq : ∀ (c : Lean.Meta.Grind.SplitInfo) (numCases : ℕ) (isRec : Bool) (e : Lean.Expr) (anchor : UInt64)
  (c_1 : Lean.Meta.Grind.SplitInfo) (numCases_1 : ℕ) (isRec_1 : Bool) (e_1 : Lean.Expr) (anchor_1 : UInt64),
  ({ c := c, numCases := numCases, isRec := isRec, e := e, anchor := anchor } =
      { c := c_1, numCases := numCases_1, isRec := isRec_1, e := e_1, anchor := anchor_1 }) =
    (c = c_1 ∧ numCases = numCases_1 ∧ isRec = isRec_1 ∧ e = e_1 ∧ anchor = anchor_1)
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_rci : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_rci._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap α β cmp} {bound : α},
  Std.Slice.toList (Std.Rci.Sliceable.mkSlice t bound...*) = List.filter (fun e => (cmp e.1 bound).isGE) t.toList
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.induce_sUnion_connected_of_pairwise_not_disjoint : ∀ {V : Type u} {G : SimpleGraph V} {S : Set (Set V)},
  S.Nonempty →
    (∀ {s t : Set V}, s ∈ S → t ∈ S → (s ∩ t).Nonempty) →
      (∀ {s : Set V}, s ∈ S → (SimpleGraph.induce s G).Connected) → (SimpleGraph.induce (⋃₀ S) G).Connected
-- Mathlib.Logic.Encodable.Basic
/-- A constructive version of `Classical.axiom_of_choice` for `Encodable` types.  -/
Encodable.axiom_of_choice : ∀ {α : Type u_1} {β : α → Type u_2} {R : (x : α) → β x → Prop} [(a : α) → Encodable (β a)]
  [(x : α) → (y : β x) → Decidable (R x y)], (∀ (x : α), ∃ y, R x y) → ∃ f, ∀ (x : α), R x (f x)
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupSeminorm.sSup_of_not_bddAbove : ∀ {E : Type u_3} [inst : AddGroup E] {s : Set (NonarchAddGroupSeminorm E)}, ¬BddAbove s → sSup s = 0
-- Mathlib.Topology.VectorBundle.Hom
Bundle.Trivialization.continuousLinearMap_apply : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  {E₁ : B → Type u_5} [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj}
  {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj} [inst_13 : (x : B) → TopologicalSpace (E₁ x)]
  [inst_14 : FiberBundle F₁ E₁] [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)]
  [inst_17 : FiberBundle F₂ E₂] [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ] [he₁ : MemTrivializationAtlas e₁]
  [he₂ : MemTrivializationAtlas e₂] (p : Bundle.TotalSpace (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x),
  ↑(Bundle.Trivialization.continuousLinearMap σ e₁ e₂) p =
    (p.proj,
      Bundle.Trivialization.continuousLinearMapAt 𝕜₂ e₂ p.proj ∘SL p.snd ∘SL Bundle.Trivialization.symmL 𝕜₁ e₁ p.proj)
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_ofAdd : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous ⇑Multiplicative.ofAdd
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.δ_naturalityᵣ_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {M : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} M]
  [inst_2 : CategoryTheory.MonoidalCategory M] (F : CategoryTheory.Functor M (CategoryTheory.Functor C C)) {m n n' : M}
  (g : n ⟶ n') (X : C) [inst_3 : F.OplaxMonoidal] {Z : C} (h : (F.obj n').obj ((F.obj m).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n).app X)
      (CategoryTheory.CategoryStruct.comp ((F.map g).app ((F.obj m).obj X)) h) =
    CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft m g)).app X)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.OplaxMonoidal.δ F m n').app X) h)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.opProdIsoCoprod_hom_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A B] {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr.unop h
-- Mathlib.Algebra.Group.Subgroup.Basic
MonoidHom.liftOfRightInverseAux.eq_1 : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : Group G₁] [inst_1 : Group G₂] [inst_2 : Group G₃]
  (f : G₁ →* G₂) (f_inv : G₂ → G₁) (hf : Function.RightInverse f_inv ⇑f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker),
  f.liftOfRightInverseAux f_inv hf g hg = { toFun := fun b => g (f_inv b), map_one' := ⋯, map_mul' := ⋯ }
-- Lean.Meta.Hint
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.joinEdits : {α : Type} → Array (Lean.Diff.Action × α) → Array (Lean.Diff.Action × Array α)
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.star_im : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], star a.im = -a.im + ↑c₂ * ↑a.imI
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
/-- Relate the integral `cos x ^ n` over `[0, π/2]` to the integral of `sin x ^ n` over `[0, π]`,
which is studied in `Mathlib/Analysis/Real/Pi/Wallis.lean` and other places.  -/
EulerSine.integral_cos_pow_eq : ∀ (n : ℕ), ∫ (x : ℝ) in 0..Real.pi / 2, Real.cos x ^ n = 1 / 2 * ∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ n
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instInvolutiveStar : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [InvolutiveStar β] → InvolutiveStar (MeasureTheory.SimpleFunc α β)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- The `i`th canonical injection, from `A i` to the free product, as
a linear map  -/
LinearAlgebra.FreeProduct.lof : {I : Type u} →
  [inst : DecidableEq I] →
    (R : Type v) →
      [inst_1 : CommSemiring R] →
        (A : I → Type w) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] → (i : I) → A i →ₗ[R] LinearAlgebra.FreeProduct R A
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticForm.toMatrix'.congr_simp : ∀ {R : Type u_3} {n : Type w} [inst : Fintype n] {inst_1 : DecidableEq n} [inst_2 : DecidableEq n] [inst_3 : CommRing R]
  [inst_4 : Invertible 2] (Q Q_1 : QuadraticForm R (n → R)),
  Q = Q_1 → ∀ (a a_1 : n), a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → Q.toMatrix' a a_2 = Q_1.toMatrix' a_1 a_3
-- Mathlib.MeasureTheory.Group.Action
/-- Equivalent definitions of a measure invariant under a multiplicative action of a group.

0. `SMulInvariantMeasure G α μ`;

1. for every `c : G` and a measurable set `s`, the measure of the preimage of `s` under scalar
  multiplication by `c` is equal to the measure of `s`;

2. for every `c : G` and a measurable set `s`, the measure of the image `c • s` of `s` under
  scalar multiplication by `c` is equal to the measure of `s`;

3. property 1 for any set, including non-measurable ones;
4. property 2 for any set, including non-measurable ones;

5. for any `c : G`, scalar multiplication by `c` maps `μ` to `μ`;

6. for any `c : G`, scalar multiplication by `c` is a measure-preserving map.  -/
MeasureTheory.smulInvariantMeasure_tfae : ∀ (G : Type u) {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasurableConstSMul G α],
  [MeasureTheory.SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x => c • x) ⁻¹' s) = μ s,
      ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun x => c • x) μ = μ,
      ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c • x) μ μ].TFAE
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.whiskerRight_tensorUnit_comp_rightUnitor_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] {X : C} {Y : D} (f : Y ⟶ F.obj X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit D))
      (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.Functor.LaxMonoidal.ε F))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))
-- Lean.Elab.Tactic.Grind.Basic
Lean.Elab.Tactic.Grind.grindTacElabAttribute : Lean.KeyedDeclsAttribute Lean.Elab.Tactic.Grind.GrindTactic
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_pow_even : ∀ (n : ℕ), ∫ (x : ℝ) in 0..Real.pi, Real.sin x ^ (2 * n) = Real.pi * ∏ i ∈ Finset.range n, (2 * ↑i + 1) / (2 * ↑i + 2)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonResolvableCompletionList : Lean.FromJson Lean.Lsp.ResolvableCompletionList
-- Mathlib.Probability.Independence.Integration
/-- **Alias** of `ProbabilityTheory.IndepFun.integrable_right_of_integrable_op`.

---

If `X` and `Y` are two independent random variables, `B X Y` is integrable, `X` is not
almost-surely `0` and `c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ`, then `Y` is integrable.

This is useful for the case where `B` is scalar multiplication, as it will allow to drop
integrability hypotheses.  -/
ProbabilityTheory.IndepFun.integrable_right_of_integrable_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {E : Type u_5} {F : Type u_6} {G : Type u_7}
  [inst : NormedAddGroup E] [inst_1 : MeasurableSpace E] [OpensMeasurableSpace E] [inst_3 : TopologicalSpace F]
  [inst_4 : ContinuousENorm F] [inst_5 : MeasurableSpace F] [OpensMeasurableSpace F] [inst_7 : TopologicalSpace G]
  [inst_8 : ContinuousENorm G] {X : Ω → E} {Y : Ω → F},
  ProbabilityTheory.IndepFun X Y μ →
    ∀ (B : E → F → G) (c : NNReal),
      c ≠ 0 →
        (∀ (x : E) (y : F), ↑c * ‖x‖ₑ * ‖y‖ₑ ≤ ‖B x y‖ₑ) →
          MeasureTheory.Integrable (fun ω => B (X ω) (Y ω)) μ →
            MeasureTheory.AEStronglyMeasurable X μ →
              MeasureTheory.AEStronglyMeasurable Y μ → ¬X =ᵐ[μ] 0 → MeasureTheory.Integrable Y μ
-- Mathlib.Algebra.Module.LocalizedModule.Basic
_private.Mathlib.Algebra.Module.LocalizedModule.Basic.0.LocalizedModule.example_oreLocalizationInstCommRing_eq_localizedModuleInstCommRing : ∀ {R : Type u_3} [inst : CommRing R] {S : Submonoid R}, OreLocalization.instCommRing = LocalizedModule.instCommRing
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.instInhabitedHom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Preadditive C] → (M N : CategoryTheory.Mat_ C) → Inhabited (M ⟶ N)
-- Mathlib.Algebra.BigOperators.Pi
Pi.addMonoidHomAddEquiv.eq_1 : ∀ {ι : Type u_7} [inst : Fintype ι] [inst_1 : DecidableEq ι] (M : ι → Type u_8) [inst_2 : (i : ι) → AddCommMonoid (M i)]
  (M' : Type u_9) [inst_3 : AddCommMonoid M'],
  Pi.addMonoidHomAddEquiv M M' =
    { toFun := fun φ i => φ.comp (AddMonoidHom.single M i),
      invFun := fun φ => ∑ i, (φ i).comp (Pi.evalAddMonoidHom M i), left_inv := ⋯, right_inv := ⋯, map_add' := ⋯ }
-- Mathlib.Logic.Hydra
Relation.cutExpand_double_left : ∀ {α : Type u_1} {r : α → α → Prop} {a a₁ a₂ b : α}, r a₁ a → r a₂ a → Relation.CutExpand r {a₁, a₂, b} {a, b}
-- Mathlib.Topology.Category.LightProfinite.Extend
/-- An abbreviation for `S.fintypeDiagram' ⋙ toLightProfinite`.  -/
LightProfinite.diagram' : (S : LightProfinite) →
  CategoryTheory.Functor (CategoryTheory.StructuredArrow S FintypeCat.toLightProfinite) LightProfinite
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.functor_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  {X Y : C} (f : X ⟶ Y) (T : C),
  (CategoryTheory.Limits.coprod.functor.map f).app T =
    CategoryTheory.Limits.coprod.map f (CategoryTheory.CategoryStruct.id T)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {fallback : β k},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getD k fallback = t₂.getD k fallback
-- Mathlib.LinearAlgebra.Prod
LinearMap.pair_fst_snd : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.fst R M M₂).prod (LinearMap.snd R M M₂) = LinearMap.id
-- Mathlib.Analysis.Convex.Combination
/-- Convex hull of `s` is equal to the set of all centers of masses of `Finset`s `t`, `z '' t ⊆ s`.
For universe reasons, you shouldn't use this lemma to prove that a given center of mass belongs
to the convex hull. Use convexity of the convex hull instead.
 -/
convexHull_eq : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s : Set E),
  (convexHull R) s = {x | ∃ ι t w z, (∀ i ∈ t, 0 ≤ w i) ∧ ∑ i ∈ t, w i = 1 ∧ (∀ i ∈ t, z i ∈ s) ∧ t.centerMass w z = x}
-- Mathlib.Order.WellFounded
StrictMono.not_bddBelow_range_of_wellFoundedGT : ∀ {β : Type u_2} [inst : LinearOrder β] {f : β → β} [WellFoundedGT β] [NoMinOrder β],
  StrictMono f → ¬BddBelow (Set.range f)
-- Mathlib.Analysis.Calculus.FDeriv.Star
/-- If `f` is differentiable at `z`, then `star ∘ f ∘ star` is differentiable at `star z`.  -/
DifferentiableAt.star_star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] [inst_9 : StarAddMonoid E] [StarModule 𝕜 E]
  [ContinuousStar E] [NormedStarGroup 𝕜] {f : E → F} {z : E},
  DifferentiableAt 𝕜 f z → DifferentiableAt 𝕜 (star ∘ f ∘ star) (star z)
-- Mathlib.Algebra.Group.Equiv.Basic
Equiv.inv.eq_1 : ∀ (G : Type u_14) [inst : InvolutiveInv G], Equiv.inv G = Function.Involutive.toPerm Inv.inv ⋯
-- Init.Sym.DSimp.DSimprocDSL
/-- Register a named `Sym.dsimp` variant.

```
register_sym_dsimp myVariant where
  pre  := match
  post := ground >> zeta_delta
  maxSteps := 50000
```
 -/
Lean.Parser.Command.registerSymDSimp : Lean.ParserDescr
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey!_eq_getKey!ₘ : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) [inst_1 : Inhabited α] (l : Std.DTreeMap.Internal.Impl α β),
  l.getKey! k = l.getKey!ₘ k