mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
/-- A pretransitive action is `n.succ-`preprimitive
iff the action of stabilizers is `n`-preprimitive.  -/
MulAction.isMultiplyPreprimitive_succ_iff_ofStabilizer : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] [MulAction.IsPretransitive M α] {n : ℕ},
  1 ≤ n →
    ∀ {a : α},
      MulAction.IsMultiplyPreprimitive M α n.succ ↔
        MulAction.IsMultiplyPreprimitive (↥(MulAction.stabilizer M a)) (↥(SubMulAction.ofStabilizer M a)) n
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- A variant of the Euler product for Dirichlet L-series.  -/
DirichletCharacter.LSeries_eulerProduct_exp_log : ∀ {N : ℕ} (χ : DirichletCharacter ℂ N) {s : ℂ},
  1 < s.re → Complex.exp (∑' (p : Nat.Primes), -Complex.log (1 - χ ↑↑p * ↑↑p ^ (-s))) = LSeries (fun n => χ ↑n) s
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.one : {α : Type u} → [One α] → One (WithTop α)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instPreservesColimitsOfShapeForgetOrderEmbeddingCarrierObjPartOrdEmbIsCardinalFilteredOfIsCardinalFiltered : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (A : Type u) [inst_1 : CategoryTheory.SmallCategory A]
  [CategoryTheory.IsCardinalFiltered A κ],
  CategoryTheory.Limits.PreservesColimitsOfShape A (CategoryTheory.forget (CategoryTheory.CardinalDirectedPoset κ))
-- Mathlib.Combinatorics.Quiver.Cast
Quiver.Hom.cast_eq_cast : ∀ {U : Type u_1} [inst : Quiver U] {u v u' v' : U} (hu : u = u') (hv : v = v') (e : u ⟶ v),
  Quiver.Hom.cast hu hv e = cast ⋯ e
-- Mathlib.Topology.Algebra.ClopenNhdofOne
/-- Any closed subgroup of a profinite group is the intersection of the open subgroups containing it.
See https://math.stackexchange.com/questions/5023433/closed-subgroups-of-a-compact-topological-group.
 -/
ProfiniteGrp.closedAddSubgroup_eq_sInf_open : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] [CompactSpace G]
  [TotallyDisconnectedSpace G] (H : ClosedAddSubgroup G), ↑H = sInf {N | IsOpen ↑N ∧ ↑H ≤ N}
-- Mathlib.Algebra.Order.Archimedean.Basic
Additive.instArchimedean : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : PartialOrder G] [MulArchimedean G], Archimedean (Additive G)
-- Init.Data.UInt.Lemmas
UInt16.toNat_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt16.size → (UInt16.ofNatClamp n).toNat = n
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode.fixed.injEq : ∀ (n n_1 : ℕ),
  (Std.Http.Protocol.H1.Machine.BodyMode.fixed✝ n = Std.Http.Protocol.H1.Machine.BodyMode.fixed✝ n_1) = (n = n_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.toN_eq_iff : ∀ {X : SSet} {x : X.S} {y : X.N}, x.toN = y ↔ y.subcomplex = x.subcomplex
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.BinaryCofan.ι_app_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y),
  s.ι.app { as := CategoryTheory.Limits.WalkingPair.right } = s.inr
-- Mathlib.Data.Bool.Basic
Bool.linearOrder : LinearOrder Bool
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey!_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {f : α → β → Bool} {k : α},
  (Std.ExtDTreeMap.filter f t).getKey! k =
    ((t.getKey? k).pfilter fun x h' => f x (Std.ExtDTreeMap.Const.get t x ⋯)).get!
-- Mathlib.Analysis.SpecificLimits.RCLike
RCLike.tendsto_ofReal_atTop_cobounded : ∀ (𝕜 : Type u_1) [inst : RCLike 𝕜], Filter.Tendsto RCLike.ofReal Filter.atTop (Bornology.cobounded 𝕜)
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.injective : ∀ {𝕜 : 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] {f : E → F}
  {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal},
  ApproximatesLinearOn f (↑f') s c → Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹ → Function.Injective (s.domRestrict f)
-- Mathlib.FieldTheory.Separable
Algebra.isSeparable_tower_bot_of_isSeparable : ∀ (F : Type u_1) [inst : Field F] (K : Type u_2) (E : Type u_3) [inst_1 : Field K] [inst_2 : Ring E]
  [inst_3 : Algebra F K] [inst_4 : Algebra F E] [inst_5 : Algebra K E] [Nontrivial E] [IsScalarTower F K E]
  [h : Algebra.IsSeparable F E], Algebra.IsSeparable F K
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.coroot_eq_polarizationEquiv_apply_root : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : Field R] [inst_4 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [inst_6 : P.IsAnisotropic] [inst_7 : P.IsRootSystem] (i : ι),
  P.coroot i = (2 / (P.RootForm (P.root i)) (P.root i)) • P.PolarizationEquiv (P.root i)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.Monic.ne_zero : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p : AddMonoidAlgebra R A} {D : A → B} [inst_3 : Nonempty A] [Nontrivial R], AddMonoidAlgebra.Monic D p → p ≠ 0
-- Mathlib.Topology.LocallyFinsupp
/-- Functions with locally finite support within `U` form an additive subgroup of functions `X → Y`.
 -/
Function.locallyFinsuppWithin.addSubgroup : {X : Type u_1} → [TopologicalSpace X] → Set X → {Y : Type u_2} → [inst : AddGroup Y] → AddSubgroup (X → Y)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.dvd_of_dvd_mul_right_of_isPrimal : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime x z → x ∣ y * z → IsPrimal x → x ∣ y
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Sums of harmonic functions are harmonic.
 -/
InnerProductSpace.HarmonicOnNhd.add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {s : Set E},
  InnerProductSpace.HarmonicOnNhd f₁ s →
    InnerProductSpace.HarmonicOnNhd f₂ s → InnerProductSpace.HarmonicOnNhd (f₁ + f₂) s
-- Mathlib.Algebra.Order.Nonneg.Field
Nonneg.div : {α : Type u_1} → [inst : Semifield α] → [inst_1 : LinearOrder α] → [IsStrictOrderedRing α] → Div { x // 0 ≤ x }
-- Lean.Elab.DocString
Lean.Doc.instReprSuggestionMode : Repr Lean.Doc.SuggestionMode
-- Mathlib.Probability.Process.Adapted
MeasureTheory.Adapted.mul : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : ι → Type u_3} [inst_1 : (i : ι) → MeasurableSpace (β i)] {u v : (i : ι) → Ω → β i} [inst_2 : (i : ι) → Mul (β i)]
  [∀ (i : ι), MeasurableMul₂ (β i)],
  MeasureTheory.Adapted f u → MeasureTheory.Adapted f v → MeasureTheory.Adapted f (u * v)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_filter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {f : α → Bool} {k : α}, m.WF → (Std.HashSet.Raw.filter f m).get? k = Option.filter f (m.get? k)
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In a commutative semiring, a finite product of sums of squares is a sum of squares.  -/
IsSumSq.prod : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} {I : Finset ι} {x : ι → R},
  (∀ i ∈ I, IsSumSq (x i)) → IsSumSq (∏ i ∈ I, x i)
-- Mathlib.RingTheory.LocalRing.ResidueField.Ideal
Ideal.ResidueField.map.congr_simp : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (I : Ideal R) [inst_2 : I.IsPrime]
  (J : Ideal S) [inst_3 : J.IsPrime] (f f_1 : R →+* S) (e_f : f = f_1) (hf : I = Ideal.comap f J),
  Ideal.ResidueField.map I J f hf = Ideal.ResidueField.map I J f_1 ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.startsWith_slice_iff : ∀ {pat s : String.Slice}, s.startsWith pat = true ↔ pat.copy.toList <+: s.copy.toList
-- Mathlib.Data.PFunctor.Multivariate.M
/-- construct through corecursion the shape of an M-type
without its contents  -/
MvPFunctor.M.corecShape : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {β : Type v} → (g₀ : β → P.A) → ((b : β) → P.last.B (g₀ b) → β) → β → P.last.M
-- Init.BinderPredicates
/-- `satisfies_binder_pred% t pred` expands to a proposition expressing that `t` satisfies `pred`.
 -/
Lean.«termSatisfies_binder_pred%__» : Lean.ParserDescr
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- `map f` and `comap f` form a `GaloisCoinsertion` when `f` is injective.  -/
Submonoid.gciMapComap : {M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        {F : Type u_4} →
          [inst_2 : FunLike F M N] →
            [mc : MonoidHomClass F M N] →
              {f : F} → Function.Injective ⇑f → GaloisCoinsertion (Submonoid.map f) (Submonoid.comap f)
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.composableArrows₂_exact : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ : CategoryTheory.ShortComplex (HomologicalComplex C c)},
  S₁.ShortExact → ∀ (i : ι), (HomologicalComplex.HomologySequence.composableArrows₂ S₁ i).Exact
-- Mathlib.NumberTheory.FLT.Polynomial
_private.Mathlib.NumberTheory.FLT.Polynomial.0.ineq_pqr_contradiction : ∀ {p q r a b c : ℕ},
  p ≠ 0 →
    q ≠ 0 →
      r ≠ 0 → q * r + r * p + p * q ≤ p * q * r → p * a < a + b + c → q * b < a + b + c → r * c < a + b + c → False
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.mkOfCovers_f : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (J : Type u_1)
  (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↥X), ∃ j y, (map j) y = x)
  (map_prop : autoParam (∀ (j : J), P (map j)) AlgebraicGeometry.Scheme.Cover.mkOfCovers._auto_1) (j : J),
  (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).f j = map j
-- Mathlib.Analysis.Convex.Body
ConvexBody.ext : ∀ {V : Type u_1} [inst : TopologicalSpace V] [inst_1 : AddCommGroup V] [inst_2 : Module ℝ V] {K L : ConvexBody V},
  ↑K = ↑L → K = L
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Submodule.instIsPrimeValIdealMemSetAssociatedPrimes : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} (I : ↑N.associatedPrimes), (↑I).IsPrime
-- Mathlib.Topology.Order.DenselyOrdered
nhdsWithin_Ioi_neBot' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  (Set.Ioi a).Nonempty → a ≤ b → (nhdsWithin b (Set.Ioi a)).NeBot
-- Init.Data.Array.Subarray
Subarray.instGetElemNatLtSizeSubarrayData : {α : Type u_1} → GetElem (Subarray α) ℕ α fun xs i => i < Std.Slice.size xs
-- Init.Grind.AC
Lean.Grind.AC.Seq.sort_k.eq_1 : ∀ (s : Lean.Grind.AC.Seq),
  s.sort_k =
    Lean.Grind.AC.Seq.rec (fun x => Lean.Grind.AC.Seq.var x) (fun x s x_1 => s.sort' (Lean.Grind.AC.Seq.var x)) s
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonWaitForDiagnostics : Lean.ToJson Lean.Lsp.WaitForDiagnostics
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_insertIfNew : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k}, a ∈ (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl ↔ compare k a = Ordering.eq ∨ a ∈ t
-- Mathlib.FieldTheory.Galois.Basic
isGalois_iff : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E],
  IsGalois F E ↔ Algebra.IsSeparable F E ∧ Normal F E
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.K'.elim.match_1.eq_1 : ∀ (motive : Turing.PartrecToTM2.K' → Sort u_1) (h_1 : Unit → motive Turing.PartrecToTM2.K'.main)
  (h_2 : Unit → motive Turing.PartrecToTM2.K'.rev) (h_3 : Unit → motive Turing.PartrecToTM2.K'.aux)
  (h_4 : Unit → motive Turing.PartrecToTM2.K'.stack),
  (match Turing.PartrecToTM2.K'.main with
    | Turing.PartrecToTM2.K'.main => h_1 ()
    | Turing.PartrecToTM2.K'.rev => h_2 ()
    | Turing.PartrecToTM2.K'.aux => h_3 ()
    | Turing.PartrecToTM2.K'.stack => h_4 ()) =
    h_1 ()
-- Std.Http.Server
/-- Semaphore used to enforce the maximum number of simultaneous active connections.
`none` means no connection limit.
 -/
Std.Http.Server.connectionLimit : Std.Http.Server → Option Std.Semaphore
-- Mathlib.CategoryTheory.Sites.IsSheafFor
/-- A family of elements on `{ f : X ⟶ Y }` is an element of `F(X)`.  -/
CategoryTheory.Presieve.FamilyOfElements.singletonEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.Functor Cᵒᵖ (Type w)) →
      {X Y : C} →
        (f : X ⟶ Y) →
          CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.singleton f) ≃ P.obj (Opposite.op X)
-- Mathlib.Algebra.CubicDiscriminant
Cubic.mk.injEq : ∀ {R : Type u_1} (a b c d a_1 b_1 c_1 d_1 : R),
  ({ a := a, b := b, c := c, d := d } = { a := a_1, b := b_1, c := c_1, d := d_1 }) =
    (a = a_1 ∧ b = b_1 ∧ c = c_1 ∧ d = d_1)
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.charpoly.congr_simp : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f f_1 : M →ₗ[R] M), f = f_1 → f.charpoly = f_1.charpoly
-- Init.Data.Nat.Lcm
Nat.lcm_mul_gcd : ∀ (m n : ℕ), m.lcm n * m.gcd n = m * n
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.instTop : {R : Type u} → {M : Type v} → [inst : VAdd R M] → Top (SubAddAction R M)
-- Mathlib.Order.RelClasses
wellFounded_lt : ∀ {α : Type u} [inst : LT α] [WellFoundedLT α], WellFounded fun x1 x2 => x1 < x2
-- Mathlib.CategoryTheory.Sites.Precoverage
/-- **Alias** of `CategoryTheory.Precoverage.HasPullbacks.hasPullbacks_of_mem`. -/
CategoryTheory.Precoverage.hasPullbacks_of_mem : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {J : CategoryTheory.Precoverage C} [self : J.HasPullbacks]
  {X Y : C} {R : CategoryTheory.Presieve Y} (f : X ⟶ Y), R ∈ J.coverings Y → R.HasPullbacks f
-- Mathlib.Data.Finsupp.Order
Finsupp.mapDomain_lt_mapDomain_iff_lt : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : Preorder α] {f : ι → κ},
  Function.Injective f → ∀ (g₁ g₂ : ι →₀ α), Finsupp.mapDomain f g₁ < Finsupp.mapDomain f g₂ ↔ g₁ < g₂
-- Mathlib.Topology.MetricSpace.PiNat
/-- The restrictions of `x` and `y` to `n` are equal if and only if `x m = y m` for all `m < n`.  -/
PiNat.res_eq_res : ∀ {α : Type u_2} {x y : ℕ → α} {n : ℕ}, PiNat.res x n = PiNat.res y n ↔ ∀ ⦃m : ℕ⦄, m < n → x m = y m
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.lt_rootMultiplicity_iff_isRoot_iterate_derivative_of_mem_nonZeroDivisors' : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R} {n : ℕ},
  p ≠ 0 →
    (∀ m ≤ n, m ≠ 0 → ↑m ∈ nonZeroDivisors R) →
      (n < Polynomial.rootMultiplicity t p ↔ ∀ m ≤ n, ((⇑Polynomial.derivative)^[m] p).IsRoot t)
-- Mathlib.Order.Interval.Set.Basic
Set.right_mem_Ioc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∈ Set.Ioc b a ↔ b < a
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.id_tensor_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : C}
  (f : W ⟶ X) (g : X ⟶ Y) {Z_1 : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z)
        (CategoryTheory.CategoryStruct.comp f g))
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z) f)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id Z) g) h)
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.toBilinForm_injective : ∀ {𝕜 : Type u_2} {E : Type u_5} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E], Function.Injective ContinuousLinearMap.toBilinForm
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.instHasPullbackOppositeOpOfHasPushout : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [CategoryTheory.Limits.HasPushout f g], CategoryTheory.Limits.HasPullback f.op g.op
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.fromLocalizedModule_mk : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M) (s : ↥S),
  (IsLocalizedModule.fromLocalizedModule S f) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (f m)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eq_some_iff_exists_beq_and_mem_toList : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β},
  Std.Internal.List.DistinctKeys l →
    (Std.Internal.List.getValue? k l = some v ↔ ∃ k', (k == k') = true ∧ (k', v) ∈ List.map (fun x => (x.fst, x.snd)) l)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.PushoutCocone.inl_colimit_cocone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : Z ⟶ X) (g : Z ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.span f g)],
  CategoryTheory.Limits.PushoutCocone.inl (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Limits.span f g)) =
    CategoryTheory.Limits.pushout.inl f g
-- Init.Data.Array.Lemmas
Array.filterMap_push : ∀ {α : Type u_1} {β : Type u_2} {stop : ℕ} {f : α → Option β} {a : α} {xs : Array α},
  stop = xs.size + 1 →
    Array.filterMap f (xs.push a) 0 stop =
      match f a with
      | none => Array.filterMap f xs
      | some b => (Array.filterMap f xs).push b
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.neg_def : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] (w : FreeAddMonoid (G ⊕ H)),
  -AddMonoid.Coprod.mk w =
    AddMonoid.Coprod.mk (FreeAddMonoid.ofList (List.map (Sum.map Neg.neg Neg.neg) (FreeAddMonoid.toList w)).reverse)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
/-- The presheaf of smooth functions from `M` to `A`, for `A` an additive abelian Lie
group, as a presheaf of additive abelian groups.  -/
smoothPresheafAddCommGroup : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              ModelWithCorners 𝕜 EM HM →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [ChartedSpace HM M] →
                                  (A : Type u) →
                                    [inst_9 : TopologicalSpace A] →
                                      [inst_10 : ChartedSpace H A] →
                                        [inst_11 : AddCommGroup A] →
                                          [LieAddGroup I (↑⊤) A] → TopCat.Presheaf AddCommGrpCat (TopCat.of M)
-- Mathlib.Geometry.Convex.Cone.Basic
/-- A convex cone is pointed if it includes `0`.  -/
ConvexCone.Pointed : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → ConvexCone R M → Prop
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.instInhabitedHom : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.Pseudofunctor B C} → {η : F ⟶ G} → Inhabited (η ⟶ η)
-- Lean.DocString.Syntax
Lean.Doc.Syntax.arg_num : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.preimage_mul_preimage_subset : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] [inst_2 : FunLike F α β]
  [MulHomClass F α β] (m : F) {s t : Set β}, ⇑m ⁻¹' s * ⇑m ⁻¹' t ⊆ ⇑m ⁻¹' (s * t)
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.z_zero_zero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (self : CategoryTheory.TwistShiftData C A), self.z 0 0 = 1
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_x : ∀ (u : PNat.XgcdType), u.flip.x = u.y
-- Lean.Meta.ArgsPacker
/-- Create a unary application by packing the given arguments using `PSigma.mk`.
The `type` should be the expected type of the packed argument, as created with `packType`.
 -/
Lean.Meta.ArgsPacker.Unary.pack : Lean.Expr → Array Lean.Expr → Lean.Expr
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.map.eq_1 : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} {B : Type u_6} (M : CStarMatrix m n A) (f : A → B),
  M.map f = CStarMatrix.ofMatrix fun i j => f (M i j)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.continuous_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y),
  Continuous ⇑h.symm
-- Mathlib.Algebra.Category.ModuleCat.Biproducts
/-- The isomorphism `A × B ≃ₗ[R] M` coming from a left split exact sequence `0 ⟶ A ⟶ M ⟶ B ⟶ 0`
of modules.  -/
lequivProdOfLeftSplitExact : {R : Type u} →
  {A : Type uA} →
    {M : Type uM} →
      {B : Type uB} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup A] →
            [inst_2 : AddCommGroup B] →
              [inst_3 : AddCommGroup M] →
                [inst_4 : Module R A] →
                  [inst_5 : Module R B] →
                    [inst_6 : Module R M] →
                      {j : A →ₗ[R] M} →
                        {g : M →ₗ[R] B} →
                          {f : M →ₗ[R] A} →
                            Function.Surjective ⇑g → j.range = g.ker → f ∘ₗ j = LinearMap.id → (A × B) ≃ₗ[R] M
-- Mathlib.RingTheory.TensorProduct.MonoidAlgebra
AddMonoidAlgebra.rTensorEquivAlgEquiv.invFun.eq_1 : ∀ {R : Type u_1} {M : Type u_2} {S : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : CommSemiring A] [inst_3 : CommSemiring B] [inst_4 : Algebra R S]
  [inst_5 : Algebra R A] [inst_6 : Algebra R B] [inst_7 : Algebra S A] [inst_8 : IsScalarTower R S A]
  [inst_9 : AddCommMonoid M],
  AddMonoidAlgebra.rTensorEquivAlgEquiv.invFun =
    AddMonoidAlgebra.liftNCAlgHom (Algebra.TensorProduct.map (AlgHom.id S A) AddMonoidAlgebra.singleZeroAlgHom)
      ((↑Algebra.TensorProduct.includeRight.toRingHom).comp (AddMonoidAlgebra.of B M)) ⋯
-- Mathlib.Algebra.Order.Monovary
monovaryOn_neg_left : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : AddCommGroup α] [inst_1 : Preorder α] [IsOrderedAddMonoid α]
  [inst_3 : PartialOrder β] {s : Set ι} {f : ι → α} {g : ι → β}, MonovaryOn (-f) g s ↔ AntivaryOn f g s
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.liftIco_coe_apply : ∀ {𝕜 : Type u_1} {B : Type u_2} [inst : AddCommGroup 𝕜] {p : 𝕜} [inst_1 : LinearOrder 𝕜] [inst_2 : IsOrderedAddMonoid 𝕜]
  [hp : Fact (0 < p)] {a : 𝕜} [inst_3 : Archimedean 𝕜] {f : 𝕜 → B} {x : 𝕜},
  x ∈ Set.Ico a (a + p) → AddCircle.liftIco p a f ↑x = f x
-- Mathlib.LinearAlgebra.TensorProduct.Submodule
Submodule.mulMap_comp_lTensor : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (M : Submodule R S)
  {N N' : Submodule R S} (hN : N' ≤ N), M.mulMap N ∘ₗ LinearMap.lTensor (↥M) (Submodule.inclusion hN) = M.mulMap N'