mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.EqToHom
/-- This is not always a good idea as a `@[simp]` lemma,
as we lose the ability to use results that interact with `F`,
e.g. the naturality of a natural transformation.

In some files it may be appropriate to use `attribute [local simp] eqToHom_map`, however.
 -/
CategoryTheory.eqToHom_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (p : X = Y), F.map (CategoryTheory.eqToHom p) = CategoryTheory.eqToHom ⋯
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.mem_fixingAddSubgroup_insert_iff : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] {a : α} {s : Set α} {m : M},
  m ∈ fixingAddSubgroup M (insert a s) ↔ m +ᵥ a = a ∧ m ∈ fixingAddSubgroup M s
-- Mathlib.Analysis.Calculus.FDeriv.Add
DifferentiableWithinAt.sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {s : Set E} {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x) → DifferentiableWithinAt 𝕜 (∑ i ∈ u, A i) s x
-- Init.Data.BitVec.Lemmas
/-- Prove equality of bitvectors in terms of nat operations.  -/
BitVec.toInt_eq_toNat_cond : ∀ {n : ℕ} (x : BitVec n), x.toInt = if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)
-- Mathlib.Data.List.Nodup
List.Nodup.take_eq_filter_mem : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {l : List α} {n : ℕ},
  l.Nodup → List.take n l = List.filter (fun a => List.elem a (List.take n l)) l
-- Mathlib.NumberTheory.Height.NumberField
/-- The logarithmic height of a tuple of rational numbers that consists of coprime integers
is the logarithm of the maximum of the absolute values of the entries.  -/
Rat.logHeight_eq_max_abs_of_gcd_eq_one : ∀ {ι : Type u_1} [inst : Fintype ι] [Nonempty ι] {x : ι → ℤ},
  Finset.univ.gcd x = 1 → Height.logHeight (Int.cast ∘ x) = Real.log ↑(⨆ i, |x i|)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
/-- If the right adjoint is full, then each component of the counit is a split monomorphism.  -/
CategoryTheory.Adjunction.unit_isSplitEpi_of_L_full : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) [L.Full] (X : C),
  CategoryTheory.IsSplitEpi (h.unit.app X)
-- Init.Data.SInt.Lemmas
ISize.ofIntClamp_toInt : ∀ (x : ISize), ISize.ofIntClamp x.toInt = x
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.star_zero : star 0 = 0
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderivWithin_const_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {x : E} {s : Set E} (c : F), fderivWithin 𝕜 (fun x => c) s x = 0
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C × C),
  CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.tensor C) X Y =
    CategoryTheory.MonoidalCategory.tensorμ X.1 X.2 Y.1 Y.2
-- Mathlib.RingTheory.WittVector.Truncated
/-- A truncated Witt vector over `R` is a vector of elements of `R`,
i.e., the first `n` coefficients of a Witt vector.
We will define operations on this type that are compatible with the (untruncated) Witt
vector operations.

`TruncatedWittVector p n R` takes a parameter `p : ℕ` that is not used in the definition.
In practice, this number `p` is assumed to be a prime number,
and under this assumption we construct a ring structure on `TruncatedWittVector p n R`.
(`TruncatedWittVector p₁ n R` and `TruncatedWittVector p₂ n R` are definitionally
equal as types but will have different ring operations.)
 -/
TruncatedWittVector : ℕ → ℕ → Type u_2 → Type u_2
-- Mathlib.Data.List.Nodup
List.not_nodup_pair : ∀ {α : Type u} (a : α), ¬[a, a].Nodup
-- Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric
_private.Mathlib.Geometry.Manifold.VectorBundle.CovariantDerivative.Metric.0.CovariantDerivative.tensorial_derivMetricTensorAux₂ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace ℝ F] {V : M → Type u_5}
  [inst_7 : TopologicalSpace (Bundle.TotalSpace F V)] [inst_8 : (x : M) → NormedAddCommGroup (V x)]
  [inst_9 : (x : M) → InnerProductSpace ℝ (V x)] [inst_10 : FiberBundle F V] (cov : CovariantDerivative I F V)
  [inst_11 : VectorBundle ℝ F V] [IsContMDiffRiemannianBundle I 1 F V] {x : M} (σ : (x : M) → V x),
  MDiffAt (T% σ) x → TensorialAt I F (fun x_1 => CovariantDerivative.derivMetricTensorAux✝ I cov σ x_1 x) x
-- Mathlib.Analysis.InnerProductSpace.Positive
/-- For an idempotent operator `p`, TFAE:
* `(range p)ᗮ = ker p`
* `p` is normal
* `p` is self-adjoint
* `p` is positive  -/
ContinuousLinearMap.IsIdempotentElem.TFAE : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] {p : E →L[𝕜] E},
  IsIdempotentElem p → [(↑p).rangeᗮ = (↑p).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE
-- Mathlib.Data.Real.ConjExponents
NNReal.holderConjugate_iff : ∀ {p q : NNReal}, p.HolderConjugate q ↔ 1 < p ∧ p⁻¹ + q⁻¹ = 1
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.taylor_one : ∀ {R : Type u_1} [inst : Semiring R] (r : R), (Polynomial.taylor r) 1 = Polynomial.C 1
-- Mathlib.Order.LatticeIntervals
Set.Ioi.coe_sup : ∀ {α : Type u_1} [inst : SemilatticeSup α] {a : α} {x y : ↑(Set.Ioi a)}, ↑(x ⊔ y) = ↑x ⊔ ↑y
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_le_sum_of_subset_of_nonpos' : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s t : Finset ι}
  [AddLeftMono N], s ⊆ t → (∀ i ∈ t, i ∉ s → f i ≤ 0) → ∑ i ∈ t, f i ≤ ∑ i ∈ s, f i
-- Mathlib.Algebra.Group.Ext
Group.ext : ∀ {G : Type u_1} ⦃g₁ g₂ : Group G⦄, HMul.hMul = HMul.hMul → g₁ = g₂
-- Mathlib.Order.Std
PartialOrder.OfStdArgs.toPreorderArgs : {α : Type u_1} → PartialOrder.OfStdArgs α → Preorder.OfStdArgs α
-- Batteries.Data.Fin.Lemmas
Fin.exists_eq_some_of_findSomeRev?_eq_some : ∀ {n : ℕ} {α : Type u_1} {x : α} {f : Fin n → Option α}, Fin.findSomeRev? f = some x → ∃ i, f i = some x
-- Init.Prelude
Mul.mk : {α : Type u} → (α → α → α) → Mul α
-- Mathlib.Algebra.Group.End
Equiv.Perm.sigmaCongrRightHom_apply : ∀ {α : Type u_7} (β : α → Type u_8) (F : (a : α) → Equiv.Perm (β a)),
  (Equiv.Perm.sigmaCongrRightHom β) F = Equiv.Perm.sigmaCongrRight F
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoOpsRef.toDoOps : Lean.Elab.Do.DoOpsRef → Lean.Elab.Do.DoOps
-- Mathlib.Data.Matrix.Mul
Matrix.mul_assoc : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalSemiring α]
  [inst_1 : Fintype m] [inst_2 : Fintype n] (L : Matrix l m α) (M : Matrix m n α) (N : Matrix n o α),
  L * M * N = L * (M * N)
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.liftNC_smul : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : AddZeroClass M]
  (f : S →+* R) (g : Multiplicative M →* R) (c : S) (φ : AddMonoidAlgebra S M),
  (AddMonoidAlgebra.liftNC ↑f ⇑g) (c • φ) = f c * (AddMonoidAlgebra.liftNC ↑f ⇑g) φ
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.concreteCategoryHom_id : ∀ (n : SimplexCategory), CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id n) = OrderHom.id
-- Mathlib.Tactic.Variable
/-- Try elaborating `ty`. Returns `none` if it doesn't need any additional typeclasses,
or it returns a new binder that needs to come first. Does not add info unless it throws
an exception.  -/
Mathlib.Command.Variable.getSubproblem : Lean.TSyntax `Lean.Parser.Term.bracketedBinder →
  Lean.Term → Lean.Elab.TermElabM (Option (Lean.MessageData × Lean.TSyntax `Lean.Parser.Term.bracketedBinder))
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseWith : Std.Time.FormatConfig → (mod : Std.Time.Modifier) → Std.Internal.Parsec.String.Parser (Std.Time.TypeFormat mod)
-- Mathlib.Tactic.Push.Attr
/-- A theorem for the `pull` tactic  -/
Mathlib.Tactic.Push.PullTheorem : Type
-- Init.Data.Rat.Lemmas
Rat.one_mul : ∀ (a : ℚ), 1 * a = a
-- Mathlib.Probability.Moments.MGFAnalytic
ProbabilityTheory.analyticAt_iteratedDeriv_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {v : ℝ},
  v ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), AnalyticAt ℝ (iteratedDeriv n (ProbabilityTheory.mgf X μ)) v
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.subRight_eq_addRight_neg : ∀ {G : Type u_5} [inst : AddGroup G] (a : G), Equiv.subRight a = Equiv.addRight (-a)
-- Mathlib.Algebra.GroupWithZero.Submonoid.Instances
MonoidWithZeroHom.instCommGroupWithZeroSubtypeMemSubmonoidMrange : {G : Type u_1} →
  {H : Type u_2} →
    [inst : GroupWithZero G] → [inst_1 : CommGroupWithZero H] → (f : G →*₀ H) → CommGroupWithZero ↥(MonoidHom.mrange f)
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.instCreatesLimitWalkingParallelPairParallelPairOfIsCosplitPairOfCreatesLimitOfIsCosplitPair : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₁, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {A B : C} →
            (f g : A ⟶ B) →
              [F.IsCosplitPair f g] →
                [CategoryTheory.Comonad.CreatesLimitOfIsCosplitPair F] →
                  CategoryTheory.CreatesLimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_sup_le_sum_spanRank : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M}, (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank
-- Mathlib.Order.BourbakiWitt
/-- The image of an admissible set under `f` is a subset of itself  -/
ChainCompletePartialOrder.IsAdmissible.image_self_subset_self : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {s : Set α},
  ChainCompletePartialOrder.IsAdmissible x f s → f '' s ⊆ s
-- Mathlib.GroupTheory.Commutator.Basic
instNonemptyElemCommutatorSet : ∀ (G : Type u_1) [inst : Group G], Nonempty ↑(commutatorSet G)
-- Init.Grind.Lint
/-- `#grind_lint mute thm₁ …` marks the given theorem(s) as *muted* during linting.

Muted theorems remain in the environment but are not instantiated when running
`#grind_lint check` or `#grind_lint inspect`.
This is useful for suppressing noisy or recursive lemmas that cause excessive
E-matching without removing their annotations.

Example:
```
#grind_lint mute Array.zip_map Int.zero_shiftRight
```
 -/
Lean.Grind.grindLintMute : Lean.ParserDescr
-- Mathlib.Topology.FiberBundle.Basic
/-- A (topological) fiber bundle with fiber `F` over a base `B` is a space projecting on `B`
for which the fibers are all homeomorphic to `F`, such that the local situation around each point
is a direct product.  -/
FiberBundle : {B : Type u_2} →
  (F : Type u_3) →
    [TopologicalSpace B] →
      [TopologicalSpace F] →
        (E : B → Type u_5) →
          [TopologicalSpace (Bundle.TotalSpace F E)] → [(b : B) → TopologicalSpace (E b)] → Type (max (max u_2 u_3) u_5)
-- Mathlib.Data.Finset.Sum
Finset.disjSum.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (s : Finset α) (t : Finset β), s.disjSum t = { val := s.val.disjSum t.val, nodup := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector.  -/
Orthonormal.inner_right_fintype : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Fintype ι] {v : ι → E},
  Orthonormal 𝕜 v → ∀ (l : ι → 𝕜) (i : ι), inner 𝕜 (v i) (∑ i, l i • v i) = l i
-- Mathlib.RingTheory.Localization.Defs
/-- An auxiliary typeclass to avoid auto-generated declarations
under the `IsLocalization` namespace.  -/
IsLocalization' : {R : Type u_1} →
  [inst : CommSemiring R] → Submonoid R → (S : Type u_2) → [inst_1 : CommSemiring S] → [Algebra R S] → Prop
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
CategoryTheory.InjectiveResolution.self_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (Z : C) [inst_3 : CategoryTheory.Injective Z],
  (CategoryTheory.InjectiveResolution.self Z).ι = CategoryTheory.CategoryStruct.id ((CochainComplex.single₀ C).obj Z)
-- Mathlib.Data.Real.Basic
Real.mk_neg : ∀ {f : CauSeq ℚ abs}, Real.mk (-f) = -Real.mk f
-- Mathlib.Algebra.Category.Ring.Under.Basic
CommRingCat.instAlgebraCarrierRight : {R : CommRingCat} → (A : CategoryTheory.Under R) → Algebra ↑R ↑A.right
-- Mathlib.Analysis.Normed.Operator.Mul
/-- The norm of `lsmul` is at most 1 in any semi-normed group.  -/
ContinuousLinearMap.opNorm_lsmul_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_3} [inst_3 : SeminormedRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : IsBoundedSMul R E] [inst_7 : IsScalarTower 𝕜 R E], ‖ContinuousLinearMap.lsmul 𝕜 R‖ ≤ 1
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.instLinearMapClassComplex : ∀ {A₁ : Type u_1} {A₂ : Type u_2} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂],
  LinearMapClass (CompletelyPositiveMap A₁ A₂) ℂ A₁ A₂
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.mapComp_assoc_right_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.LaxFunctor B CategoryTheory.Cat) {a b c d : B}
  (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (X : ↑(F.obj a)),
  CategoryTheory.CategoryStruct.comp ((F.mapComp g h).toNatTrans.app ((F.map f).toFunctor.obj X))
      ((F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).toNatTrans.app X) =
    CategoryTheory.CategoryStruct.comp ((F.map h).toFunctor.map ((F.mapComp f g).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).toNatTrans.app X)
        ((F.map₂ (CategoryTheory.Bicategory.associator f g h).hom).toNatTrans.app X))
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.op_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.LeftFraction X Y), φ.op.f = φ.f.op
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_inter!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF → m₂.WF → ∀ {k : α}, Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter! m₂).get? k = m₁.get? k
-- Init.Data.Rat.Lemmas
Rat.zpow_one : ∀ (q : ℚ), q ^ 1 = q
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.ringHom_ext_iff : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : MulOneClass M] [inst_2 : Semiring S]
  {f g : MonoidAlgebra R M →+* S},
  f = g ↔
    (∀ (r : R), f (MonoidAlgebra.single 1 r) = g (MonoidAlgebra.single 1 r)) ∧
      ∀ (m : M), f (MonoidAlgebra.single m 1) = g (MonoidAlgebra.single m 1)
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Path.reverse.eq_1 : ∀ {V : Type u_2} [inst : Quiver V] [inst_1 : Quiver.HasReverse V] {a : V}, Quiver.Path.nil.reverse = Quiver.Path.nil
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.eraseTR.eq_1 : ∀ {α : Type u_1} [inst : BEq α] (l : List α) (a : α), l.eraseTR a = List.eraseTR.go✝ l a l #[]
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.base_Y : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {J : CategoryTheory.GrothendieckTopology C}
  {f : Y ⟶ X} {S : J.Cover X} (I : (S.pullback f).Arrow), I.base.Y = I.Y
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Real.Angle.coe_toCircle : ∀ (θ : Real.Angle), ↑θ.toCircle = ↑θ.cos + ↑θ.sin * Complex.I
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.preconnected_bot_iff_subsingleton : ∀ {V : Type u}, ⊥.Preconnected ↔ Subsingleton V
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.set_smul_eq_iSup : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Type u_4}
  [inst_3 : Monoid S] [inst_4 : DistribMulAction S M] [inst_5 : SMulCommClass S R M] (s : Set S) (N : Submodule R M),
  s • N = ⨆ a ∈ s, a • N
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.match_1.eq_3 : ∀ {α : Type u_1} (motive : List (List α) → Sort u_2) (x : List α) (xs : List (List α)) (h_1 : Unit → motive [])
  (h_2 : (x : List α) → motive [x]) (h_3 : (x : List α) → (xs : List (List α)) → motive (x :: xs)),
  (xs = [] → False) →
    (match x :: xs with
      | [] => h_1 ()
      | [x] => h_2 x
      | x :: xs => h_3 x xs) =
      h_3 x xs
-- Mathlib.FieldTheory.Minpoly.Finite
minpoly.natDegree_le_spanFinrank : ∀ (A : Type u_1) {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] [Module.Finite A B]
  (x : B), (minpoly A x).natDegree ≤ ⊤.spanFinrank
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Init.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterM m α → Sort u_3) (x : α) (xs : List α)
  (h_1 : Unit → motive { internalState := { list := [] } })
  (h_2 : (x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }),
  (match { internalState := { list := x :: xs } } with
    | { internalState := { list := [] } } => h_1 ()
    | { internalState := { list := x :: xs } } => h_2 x xs) =
    h_2 x xs
-- Mathlib.Algebra.Ring.Opposite
/-- The 'unopposite' of a ring hom `Rᵐᵒᵖ →+* Sᵐᵒᵖ`. Inverse to `RingHom.op`.  -/
RingHom.unop : {R : Type u_2} →
  {S : Type u_3} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → (Rᵐᵒᵖ →+* Sᵐᵒᵖ) ≃ (R →+* S)
-- Std.Internal.Do.WP.Basic
/-- Soundness of `Seq.seq`: sequencing `f <*> x` preserves the WP.  -/
Std.Internal.Do.WPMonad.seq_le_wp_seq : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type z} [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}
  (f : m (α → β)) (x : m α) (post : β → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel (Std.Internal.Do.wp f (fun g => Std.Internal.Do.wp x (fun a => post (g a)) epost) epost)
    (Std.Internal.Do.wp (f <*> x) post epost)
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.OplaxTrans.OplaxFunctor.bicategory_associator_hom_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 : CategoryTheory.OplaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2)
  (ι : x_2 ⟶ x_3) (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).hom.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).hom
-- Init.Data.Int.DivMod.Bootstrap
Int.mul_ediv_assoc' : ∀ (b : ℤ) {a c : ℤ}, c ∣ a → a * b / c = a / c * b
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- The directed graph (quiver) associated with a matrix `A`,
with an edge `i ⟶ j` iff `0 < A i j`.  -/
Matrix.toQuiver : {n : Type u_1} → {R : Type u_2} → [Ring R] → [LinearOrder R] → Matrix n n R → Quiver n
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.instNoZeroDivisors : ∀ {Γ : Type u_1} {R : Type u_3} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ] [inst_2 : IsOrderedCancelAddMonoid Γ]
  [inst_3 : NonUnitalNonAssocSemiring R] [NoZeroDivisors R], NoZeroDivisors (HahnSeries Γ R)
-- Init.Data.UInt.Lemmas
UInt16.ofFin_sub : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a - b) = UInt16.ofFin a - UInt16.ofFin b
-- Lean.Meta.RecursorInfo
Lean.Meta.RecursorInfo.mk : Lean.Name →
  Lean.Name →
    List Lean.Meta.RecursorUnivLevelPos →
      Bool → Bool → ℕ → ℕ → List (Option ℕ) → List ℕ → List Bool → Lean.Meta.RecursorInfo
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instMul.eq_1 : ∀ (M : Type u_4) [inst : AddZero M], AddMonoid.End.instMul M = { mul := AddMonoidHom.comp }
-- Init.SimpLemmas
Lean.true_arrow : ∀ (p : Prop), Lean.Arrow True p = p
-- Lean.Level
Lean.Level.PP.Result.format : Lean.Level.PP.Result → Bool → Std.Format
-- Lean.Parser.Term.Basic
Lean.Parser.Term.binderTactic.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Geometry.Manifold.Riemannian.PathELength
Manifold.pathELength_congr_Ioo : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : (x : M) → ENorm (TangentSpace I x)] {a b : ℝ} {γ γ' : ℝ → M},
  Set.EqOn γ γ' (Set.Ioo a b) → Manifold.pathELength I γ a b = Manifold.pathELength I γ' a b
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.approxBounded.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : TopologicalSpace β] {x : MeasurableSpace α} [inst_1 : Norm β]
  [inst_2 : SMul ℝ β] (hf : MeasureTheory.StronglyMeasurable f) (c : ℝ) (n : ℕ),
  hf.approxBounded c n = MeasureTheory.SimpleFunc.map (fun x => min 1 (c / ‖x‖) • x) (hf.approx n)
-- Lean.Data.Lsp.Extra
Lean.Lsp.DependencyBuildMode.once.sizeOf_spec : sizeOf Lean.Lsp.DependencyBuildMode.once = 1
-- Mathlib.Analysis.Convex.Piecewise
/-- The piecewise function `(Set.Ici e).piecewise f g` of a function `f` decreasing and concave on
`Set.Ici e` and a function `g` increasing and concave on `Set.Iic e`, such that `f e = g e`, is
concave on the universal set.  -/
concaveOn_univ_piecewise_Ici_of_antitoneOn_Ici_monotoneOn_Iic : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LinearOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [PosSMulMono 𝕜 E] [inst_7 : AddCommGroup β]
  [inst_8 : PartialOrder β] [IsOrderedAddMonoid β] [inst_10 : Module 𝕜 β] [PosSMulMono 𝕜 β] {e : E} {f g : E → β},
  ConcaveOn 𝕜 (Set.Ici e) f →
    ConcaveOn 𝕜 (Set.Iic e) g →
      AntitoneOn f (Set.Ici e) → MonotoneOn g (Set.Iic e) → f e = g e → ConcaveOn 𝕜 Set.univ ((Set.Ici e).piecewise f g)
-- Mathlib.Algebra.Order.Group.Abs
mabs_div_lt_iff : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b c : G},
  |a / b|ₘ < c ↔ a / b < c ∧ b / a < c
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
minSmoothness_def : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] (n : WithTop ℕ∞),
  minSmoothness 𝕜 n = if IsRCLikeNormedField 𝕜 then n else ⊤
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.compProd_sum_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {ι : Type u_4} [inst : Countable ι] {κ : ι → ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel (α × β) γ} [∀ (i : ι), ProbabilityTheory.IsSFiniteKernel (κ i)],
  (ProbabilityTheory.Kernel.sum κ).compProd η = ProbabilityTheory.Kernel.sum fun i => (κ i).compProd η
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ModuleDocstringState.toState : Lean.Doc.ModuleDocstringState✝ → Lean.Doc.State
-- Lean.Message
Lean.instToMessageDataMessageData : Lean.ToMessageData Lean.MessageData