mathlib-initiative/mathlib-types huggingface dataset:
-- Init.System.IO
/-- Executes arbitrary side effects in a pure context, with exceptions indicated via `Except`. This a
**dangerous** operation that can easily undermine important assumptions about the meaning of Lean
programs, and it should only be used with great care and a thorough understanding of compiler
internals, and even then only to implement observationally pure operations.

This function is not a good way to convert an `EIO α` or `IO α` into an `α`. Instead, use
[`do`-notation](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=do-notation).

Because the resulting value is treated as a side-effect-free term, the compiler may re-order,
duplicate, or delete calls to this function. The side effect may even be hoisted into a constant,
causing the side effect to occur at initialization time, even if it would otherwise never be called.
 -/
unsafeIO : {α : Type} → IO α → Except IO.Error α
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.attachCellsιFunctorObj_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)],
  (CategoryTheory.SmallObject.attachCellsιFunctorObj f πX).ι = CategoryTheory.SmallObject.FunctorObjIndex f πX
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.rightInverse_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), Function.RightInverse ⇑e.symm ⇑e
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : PowerSeries R) (T : Subring R) (hp : ∀ (n : ℕ), (PowerSeries.coeff n) p ∈ T)
  {n : ℕ}, ↑((PowerSeries.coeff n) (p.toSubring T hp)) = (PowerSeries.coeff n) p
-- Mathlib.Topology.PreorderRestrict
Preorder.continuous_frestrictLe₂ : ∀ {α : Type u_1} [inst : Preorder α] {X : α → Type u_2} [inst_1 : (i : α) → TopologicalSpace (X i)]
  [inst_2 : LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b), Continuous (Preorder.frestrictLe₂ hab)
-- Mathlib.Algebra.Group.Subsemigroup.Basic
/-- Let `s` be a subset of a semigroup `M` such that the closure of `s` is the whole semigroup.
Then `MulHom.ofDense` defines a mul homomorphism from `M` asking for a proof
of `f (x * y) = f x * f y` only for `y ∈ s`.  -/
MulHom.ofDense : {M : Type u_3} →
  {N : Type u_4} →
    [inst : Semigroup M] →
      [inst_1 : Semigroup N] →
        {s : Set M} → (f : M → N) → Subsemigroup.closure s = ⊤ → (∀ (x y : M), y ∈ s → f (x * y) = f x * f y) → M →ₙ* N
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_filter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [inst_2 : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k : α} (h : m.WF),
  (Std.DHashMap.Raw.filter f m).getKey? k = (m.getKey? k).pfilter fun x h' => f x (m.get x ⋯)
-- Mathlib.Geometry.Manifold.ContMDiff.NormedSpace
contMDiffAt_iff_contDiffAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_5} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E']
  {n : WithTop ℕ∞} {f : E → E'} {x : E},
  ContMDiffAt (modelWithCornersSelf 𝕜 E) (modelWithCornersSelf 𝕜 E') n f x ↔ ContDiffAt 𝕜 n f x
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.ext : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] ⦃h₁ h₂ : α ≃ᵢ β⦄,
  (∀ (x : α), h₁ x = h₂ x) → h₁ = h₂
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- Transport a presentation along an algebra isomorphism.  -/
Algebra.Presentation.ofAlgEquiv : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      {σ : Type t} →
        [inst : CommRing R] →
          [inst_1 : CommRing S] →
            [inst_2 : Algebra R S] →
              Algebra.Presentation R S ι σ →
                {T : Type u_1} →
                  [inst_3 : CommRing T] → [inst_4 : Algebra R T] → (S ≃ₐ[R] T) → Algebra.Presentation R T ι σ
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_update_zero : ∀ {R : Type u_1} [inst : Semiring R] (p : SkewPolynomial R) (n : ℕ), (p.update n 0).support = p.support.erase n
-- Mathlib.Analysis.Normed.Group.Seminorm
NonarchAddGroupNorm.coe_lt_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p q : NonarchAddGroupNorm E}, ⇑p < ⇑q ↔ p < q
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.mul_add_right_left : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime (z * y + x) y
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_or_left : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, P ∧ (Q ∨ R) ⊣⊢ₛ P ∧ Q ∨ P ∧ R
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPStructureInstanceType : Lean.Options → Bool
-- Std.Time.Date.Unit.Day
/-- Creates an `Ordinal` from an integer, ensuring the value is within bounds.
 -/
Std.Time.Day.Ordinal.ofInt : (data : ℤ) → 1 ≤ data ∧ data ≤ 31 → Std.Time.Day.Ordinal
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.instAddSemigroup : {m : Type u_1} → {n : Type u_2} → {A : Type u_5} → [AddSemigroup A] → AddSemigroup (CStarMatrix m n A)
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_diagonal_eq_diagonal_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroClass α] {A : Matrix n n α} {d e : n → α},
  A.hadamard (Matrix.diagonal d) = Matrix.diagonal e ↔ A.diag * d = e
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.mapsTo_Ioi : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a : α},
  StrictAntiOn f (Set.Ici a) → Set.MapsTo f (Set.Ioi a) (Set.Iio (f a))
-- Init.Data.List.MinMax
List.min?_cons : ∀ {α : Type u_1} {x : α} [inst : Min α] [Std.Associative min] {xs : List α},
  (x :: xs).min? = some (xs.min?.elim x (min x))
-- Mathlib.Analysis.Normed.Group.Ultra
IsUltrametricDist.norm_nsmul_le : ∀ {S : Type u_1} [inst : SeminormedAddGroup S] [IsUltrametricDist S] (x : S) (n : ℕ), ‖n • x‖ ≤ ‖x‖
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.instNormedAddCommGroupProd : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {E : Type u_2} →
        {F : Type u_3} →
          [inst_2 : NormedAddCommGroup E] →
            [inst_3 : Module ℂ E] →
              [inst_4 : SMul A E] →
                [inst_5 : NormedAddCommGroup F] →
                  [inst_6 : Module ℂ F] →
                    [inst_7 : SMul A F] →
                      [CStarModule A E] →
                        [CStarModule A F] → [StarOrderedRing A] → NormedAddCommGroup (WithCStarModule A (E × F))
-- Mathlib.Algebra.Group.Equiv.Opposite
MonoidHom.fromOpposite_apply : ∀ {M : Type u_3} {N : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N)
  (hf : ∀ (x y : M), Commute (f x) (f y)), ⇑(f.fromOpposite hf) = ⇑f ∘ MulOpposite.unop
-- Mathlib.CategoryTheory.Triangulated.LocalizingSubcategory
CategoryTheory.ObjectProperty.instIsLocalizedFullyFaithfulFullSubcategoryTrWInverseImageιTriangulatedLocalizerMorphismOfIsVerdierLeftLocalizing : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (A B : CategoryTheory.ObjectProperty 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] [CategoryTheory.IsTriangulated C] [inst_7 : A.IsTriangulated]
  [B.IsTriangulated] [B.IsClosedUnderIsomorphisms] [A.IsVerdierLeftLocalizing B],
  (A.triangulatedLocalizerMorphism B).IsLocalizedFullyFaithful
-- Lean.Meta.ArgsPacker
/-- Given type `(a ⊗' b ⊕' c ⊗' d) → e`, brings `a → b → e` and `c → d → e`
into scope as fresh local declarations and passes their FVars to the continuation `k`.
The `name` is used to form the variable names; uses `name1`, `name2`, … if there are multiple.
 -/
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.withCurriedDecl : {α : Type} → Lean.Meta.ArgsPacker → Lean.Name → Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Std.Async.ContextAsync
/-- Returns a selector that completes when the current context is cancelled.
 -/
Std.Async.ContextAsync.doneSelector : Std.Async.ContextAsync (Std.Async.Selector Unit)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.rightUnshift.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ γ_1 : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n'),
  γ = γ_1 →
    ∀ (n : ℤ) (hn : n' + a = n) (T : CochainComplex.HomComplex.Triplet n),
      γ.rightUnshift n hn T = γ_1.rightUnshift n hn T
-- Init.Data.BitVec.Lemmas
BitVec.toFin_add : ∀ {w : ℕ} (x y : BitVec w), (x + y).toFin = x.toFin + y.toFin
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_pos_iff : ∀ {b x : ℝ}, 1 < b → 0 < x → (0 < Real.logb b x ↔ 1 < x)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.mulL.sizeOf_spec : ∀ (k : ℕ) (a : Nat.Internal.Linear.Expr), sizeOf (Nat.Internal.Linear.Expr.mulL k a) = 1 + sizeOf k + sizeOf a
-- Mathlib.Algebra.Group.AddChar
AddChar.zpow_apply : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : DivisionCommMonoid M] (ψ : AddChar A M) (n : ℤ)
  (a : A), (ψ ^ n) a = ψ a ^ n
-- Mathlib.Algebra.ContinuedFractions.Basic
GenContFract.Pair.coe_toPair : ∀ {α : Type u_1} {β : Type u_2} [inst : Coe α β] {a b : α}, ↑{ a := a, b := b } = { a := Coe.coe a, b := Coe.coe b }
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_eq_of_equiv_equiv : ∀ {A₁ : Type u_8} {B₁ : Type u_9} {A₂ : Type u_10} {B₂ : Type u_11} [inst : CommRing A₁] [inst_1 : Ring B₁]
  [inst_2 : CommRing A₂] [inst_3 : Ring B₂] [inst_4 : Algebra A₁ B₁] [inst_5 : Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
  (e₂ : B₁ ≃+* B₂),
  (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁) →
    ∀ (x : B₁), (Algebra.norm A₁) x = e₁.symm ((Algebra.norm A₂) (e₂ x))
-- Init.Data.List.Count
List.countP_congr : ∀ {α : Type u_1} {p q : α → Bool} {l : List α}, (∀ x ∈ l, p x = true ↔ q x = true) → List.countP p l = List.countP q l
-- Lean.Parser.Term
Lean.Parser.Term.attrKind.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Analysis.Convex.Strict
StrictConvex.linear_preimage : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜]
  [inst_2 : TopologicalSpace E] [inst_3 : TopologicalSpace F] [inst_4 : AddCommMonoid E] [inst_5 : AddCommMonoid F]
  [inst_6 : Module 𝕜 E] [inst_7 : Module 𝕜 F] {s : Set F},
  StrictConvex 𝕜 s → ∀ (f : E →ₗ[𝕜] F), Continuous ⇑f → Function.Injective ⇑f → StrictConvex 𝕜 (⇑f ⁻¹' s)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isClopen_iff : ∀ {R : Type u} [inst : CommRing R] {s : Set (PrimeSpectrum R)},
  IsClopen s ↔ ∃ e, IsIdempotentElem e ∧ s = ↑(PrimeSpectrum.basicOpen e)
-- Mathlib.Analysis.SpecialFunctions.Pow.Continuity
Filter.Tendsto.cpow : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℂ} {a b : ℂ},
  Filter.Tendsto f l (nhds a) →
    Filter.Tendsto g l (nhds b) → a ∈ Complex.slitPlane → Filter.Tendsto (fun x => f x ^ g x) l (nhds (a ^ b))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
SheafOfModules.instIsClosedUnderIsomorphismsIsQuasicoherent : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat],
  (SheafOfModules.isQuasicoherent R).IsClosedUnderIsomorphisms
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.synthesizeInsts : Array Lean.Expr → Array Lean.BinderInfo → OptionT Lean.Meta.Grind.EMatch.M Unit
-- Mathlib.Data.Finsupp.Option
Finsupp.optionElim_zero : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] (y : M), Finsupp.optionElim y 0 = fun₀ | none => y
-- Init.Data.Nat.Basic
Nat.add_lt_of_lt_sub : ∀ {a b c : ℕ}, a < c - b → a + b < c
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Cache for simplification results. Survives across binder entry.  -/
Lean.Meta.Sym.DSimp.State.cache : Lean.Meta.Sym.DSimp.State → Lean.Meta.Sym.DSimp.Cache
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.indep_bot_left : ∀ {α : Type u_1} {Ω : Type u_2} {_mα : MeasurableSpace α} (m' : MeasurableSpace Ω) {_mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} [ProbabilityTheory.IsZeroOrMarkovKernel κ],
  ProbabilityTheory.Kernel.Indep ⊥ m' κ μ
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Node.measure.measureEntries.eq_def : ∀ {α : Type u_1} {β : Type u_2} (es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (i : ℕ),
  Lean.PersistentHashMap.Node.measure.measureEntries✝ es i =
    if h : i < es.size then
      (match h_eq : es[i] with
        | Lean.PersistentHashMap.Entry.null => 1
        | Lean.PersistentHashMap.Entry.entry key val => 1
        | Lean.PersistentHashMap.Entry.ref node =>
          have this := ⋯;
          2 + node.measure) +
        Lean.PersistentHashMap.Node.measure.measureEntries✝ es (i + 1)
    else 0
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.processApp : Lean.Expr → Lean.Expr → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.Topology.Inseparable
SeparationQuotient.preimage_mk_interior : ∀ {X : Type u_1} [inst : TopologicalSpace X] {t : Set (SeparationQuotient X)},
  SeparationQuotient.mk ⁻¹' interior t = interior (SeparationQuotient.mk ⁻¹' t)
-- Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty
/-- Auxiliary definition for `fullsubcategory`.  -/
CategoryTheory.Pseudofunctor.ObjectProperty.mapComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat} →
      (P : F.ObjectProperty) →
        [inst_1 : P.IsClosedUnderMapObj] →
          {X Y Z : B} →
            (f : X ⟶ Y) → (g : Y ⟶ Z) → P.map (CategoryTheory.CategoryStruct.comp f g) ≅ (P.map f).comp (P.map g)
-- Mathlib.Topology.Neighborhoods
Filter.Frequently.mem_of_closed : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {s : Set X}, (∃ᶠ (x : X) in nhds x, x ∈ s) → IsClosed s → x ∈ s
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.monomial_mul_monomial : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℕ) (a b : R),
  (PowerSeries.monomial m) a * (PowerSeries.monomial n) b = (PowerSeries.monomial (m + n)) (a * b)
-- Mathlib.GroupTheory.Focal
/-- The **Focal Subgroup** of a subgroup `H` (denoted `H*` or `foc(H)`). It is
generated by elements of the form `x⁻¹ * (u * x * u⁻¹)` where both `x` and `x^u` are in `H`.  -/
AddSubgroup.focalAddSubgroup : {G : Type u_1} → [inst : AddGroup G] → AddSubgroup G → AddSubgroup G
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
/-- The composition of two isometric equivalences between quadratic forms.  -/
QuadraticMap.IsometryEquiv.trans : {R : Type u_2} →
  {M₁ : Type u_5} →
    {M₂ : Type u_6} →
      {M₃ : Type u_7} →
        {N : Type u_9} →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M₁] →
              [inst_2 : AddCommMonoid M₂] →
                [inst_3 : AddCommMonoid M₃] →
                  [inst_4 : AddCommMonoid N] →
                    [inst_5 : Module R M₁] →
                      [inst_6 : Module R M₂] →
                        [inst_7 : Module R M₃] →
                          [inst_8 : Module R N] →
                            {Q₁ : QuadraticMap R M₁ N} →
                              {Q₂ : QuadraticMap R M₂ N} →
                                {Q₃ : QuadraticMap R M₃ N} →
                                  Q₁.IsometryEquiv Q₂ → Q₂.IsometryEquiv Q₃ → Q₁.IsometryEquiv Q₃
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.continuous_compContinuousLinearMapCLM : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {G : Type wG} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [Finite ι],
  Continuous ContinuousAlternatingMap.compContinuousLinearMapCLM
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balLeft.match_4.splitter : {α : Type u_1} →
  (motive : RBTree.RBNode α → Sort u_2) →
    (l : RBTree.RBNode α) →
      ((a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b)) →
        ((l : RBTree.RBNode α) →
            (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α),
                l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
              motive l) →
          motive l
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.setLike : {R : Type u} →
  {M : Type v} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → SetLike (Submodule R M) M
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The equivariant map between `SubAddAction.ofStabilizer M a`
and `ofFixingAddSubgroup M {a}`.  -/
SubAddAction.ofFixingAddSubgroup_of_singleton : (M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        (a : α) →
          have φ := fun x =>
            match x with
            | ⟨m, hm⟩ => ⟨m, ⋯⟩;
          ↥(SubAddAction.ofFixingAddSubgroup M {a}) →ₑ[φ] ↥(SubAddAction.ofStabilizer M a)
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- `F` creates all finite limits.  -/
CategoryTheory.Limits.CreatesFiniteCoproducts.creates : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {F : CategoryTheory.Functor C D} →
          [self : CategoryTheory.Limits.CreatesFiniteCoproducts F] →
            (J : Type) → [Fintype J] → CategoryTheory.CreatesColimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.Algebra.Regular.Opposite
isAddLeftRegular_unop : ∀ {R : Type u_1} [inst : Add R] {a : Rᵃᵒᵖ}, IsAddLeftRegular (AddOpposite.unop a) ↔ IsAddRightRegular a
-- Mathlib.Data.Matrix.Mul
Matrix.submatrix_mul : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype n] [inst_1 : Fintype o]
  [inst_2 : Mul α] [inst_3 : AddCommMonoid α] {p : Type u_10} {q : Type u_11} (M : Matrix m n α) (N : Matrix n p α)
  (e₁ : l → m) (e₂ : o → n) (e₃ : q → p),
  Function.Bijective e₂ → (M * N).submatrix e₁ e₃ = M.submatrix e₁ e₂ * N.submatrix e₂ e₃
-- Init.Control.MonadAttach
WeaklyLawfulMonadAttach.map_attach : ∀ {m : Type u → Type v} {inst : Monad m} {inst_1 : MonadAttach m} [self : WeaklyLawfulMonadAttach m] {α : Type u}
  {x : m α}, Subtype.val <$> MonadAttach.attach x = x
-- Lean.Parser.Command
Lean.Parser.Command.optNamedPrio.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- The subsemiring of elements `x : R` such that `f x = g x`  -/
RingHom.eqLocusS : {R : Type u} →
  {S : Type v} → [inst : NonAssocSemiring R] → [inst_1 : NonAssocSemiring S] → (R →+* S) → (R →+* S) → Subsemiring R
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.msymm_isSymmetric : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] {n : ℕ}
  (μ : n.Partition), (MvPolynomial.msymm σ R μ).IsSymmetric
-- Init.Data.Option.Attach
Option.bind_attach : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {f : { x // o = some x } → Option β},
  o.attach.bind f = o.pbind fun a h => f ⟨a, h⟩
-- Mathlib.Order.Defs.PartialOrder
ge_antisymm_iff : ∀ {α : Type u_1} [inst : PartialOrder α] {a b : α}, a = b ↔ b ≤ a ∧ a ≤ b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
/-- Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃` to a category `C₃` which has pushouts, the Leibniz pushout
  (pushout-product) of `f₁ : X₁ ⟶ Y₁` in `C₁` and `f₂ : X₂ ⟶ Y₂` in `C₂` is the map
  `pushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ⟶ (F.obj Y₁).obj Y₂` induced by the diagram
```
  `(F.obj X₁).obj X₂` ----> `(F.obj Y₁).obj X₂`
          |                            |
          |                            |
          v                            v
  `(F.obj X₁).obj Y₂` ----> `(F.obj Y₁).obj Y₂`
```
 -/
CategoryTheory.Functor.leibnizPushout : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
            CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃) →
              [CategoryTheory.Limits.HasPushouts C₃] →
                CategoryTheory.Functor (CategoryTheory.Arrow C₁)
                  (CategoryTheory.Functor (CategoryTheory.Arrow C₂) (CategoryTheory.Arrow C₃))
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.rTensor_comp_mapL : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F]
  [inst_4 : InnerProductSpace 𝕜 F] [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G]
  [inst_7 : NormedAddCommGroup H] [inst_8 : InnerProductSpace 𝕜 H] {A : Type u_6} [inst_9 : NormedAddCommGroup A]
  [inst_10 : InnerProductSpace 𝕜 A] (f₁ : E →L[𝕜] F) (f₂ : A →L[𝕜] E) (g : G →L[𝕜] H),
  ContinuousLinearMap.rTensor H f₁ ∘SL TensorProduct.mapL f₂ g = TensorProduct.mapL (f₁ ∘SL f₂) g
-- Mathlib.Order.UpperLower.Basic
isUpperSet_sUnion : ∀ {α : Type u_1} [inst : LE α] {S : Set (Set α)}, (∀ s ∈ S, IsUpperSet s) → IsUpperSet (⋃₀ S)
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv_last : ∀ (n : ℕ), (finSuccEquiv (n + 1)) (Fin.last (n + 1)) = some (Fin.last n)
-- Mathlib.Logic.Function.Defs
/-- Composition of dependent functions: `(f ∘' g) x = f (g x)`, where type of `g x` depends on `x`
and type of `f (g x)` depends on `x` and `g x`.  -/
Function.«term_∘'_» : Lean.TrailingParserDescr
-- Mathlib.Order.Category.Lat
/-- The equivalence between `Lat` and itself induced by `OrderDual` both ways.  -/
Lat.dualEquiv : Lat ≌ Lat
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.IsPos.induction_on_add : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] [Finite ι] [IsDomain R] [P.IsCrystallographic] {i : ι},
  b.IsPos i →
    ∀ {p : ι → Prop},
      (∀ i ∈ b.support, p i) → (∀ (i j k : ι), P.root k = P.root i + P.root j → p i → j ∈ b.support → p k) → p i
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos : ∀ {f : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially f → (∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in Filter.atTop, f x ≤ 0
-- Mathlib.Analysis.LocallyConvex.BalancedCoreHull
balancedCore_zero_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {s : Set E},
  0 ∈ s → 0 ∈ balancedCore 𝕜 s
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : LE α] (f : ι → UpperSet α), ↑(⨆ i, f i) = ⋂ i, ↑(f i)
-- Mathlib.GroupTheory.OrderOfElement
IsAddTorsionFree.addOrderOf_nonpos : ∀ {G : Type u_1} [inst : AddCommGroup G] [IsAddTorsionFree G] (g : G), addOrderOf g ≤ 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_iff_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t ↔ t.contains k = true