mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Hindman
/-- If `m` and `m'` are finite products in `M`, then so is `m * m'`, provided that `m'` is obtained
from a subsequence of `M` starting sufficiently late.  -/
Hindman.FP.mul : ∀ {M : Type u_1} [inst : Semigroup M] {a : Stream' M} {m : M},
  m ∈ Hindman.FP a → ∃ n, ∀ m' ∈ Hindman.FP (Stream'.drop n a), m * m' ∈ Hindman.FP a
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.instDiscreteTopologyQuotientOfSeparatelyContinuousMul : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] (U : OpenSubgroup G),
  DiscreteTopology (G ⧸ ↑U)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The n-skeleton as a functor `SimplicialObject.Truncated C n ⥤ SimplicialObject C`.  -/
CategoryTheory.SimplicialObject.Truncated.sk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n : ℕ) →
      [∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
            (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F] →
        CategoryTheory.Functor (CategoryTheory.SimplicialObject.Truncated C n) (CategoryTheory.SimplicialObject C)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.mixedEmbedding.normAtComplexPlaces_mixedSpaceOfRealSpace : ∀ {K : Type u_1} [inst : Field K] {x : NumberField.mixedEmbedding.realSpace K},
  (∀ (w : NumberField.InfinitePlace K), w.IsComplex → 0 ≤ x w) →
    NumberField.mixedEmbedding.normAtComplexPlaces (NumberField.mixedEmbedding.mixedSpaceOfRealSpace x) = x
-- Mathlib.Order.Filter.Cofinite
Filter.eventually_cofinite : ∀ {α : Type u_2} {p : α → Prop}, (∀ᶠ (x : α) in Filter.cofinite, p x) ↔ {x | ¬p x}.Finite
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (A : T.Algebra),
  T.forget.obj A = A.A
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.mk.inj : ∀ {R : Type u_2} {A : Type u_3} {inst : CommSemiring R} {inst_1 : AddCommMonoid A} {inst_2 : Module R A}
  {inst_3 : Coalgebra R A} {val : A} {isGroupLikeElem_val : IsGroupLikeElem R val} {val_1 : A}
  {isGroupLikeElem_val_1 : IsGroupLikeElem R val_1},
  { val := val, isGroupLikeElem_val := isGroupLikeElem_val } =
      { val := val_1, isGroupLikeElem_val := isGroupLikeElem_val_1 } →
    val = val_1
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_C_mul_X_pow : ∀ {R : Type u} [inst : Semiring R] (x : R) (k n : ℕ),
  (Polynomial.C x * Polynomial.X ^ k).coeff n = if n = k then x else 0
-- Mathlib.CategoryTheory.Abelian.Opposite
CategoryTheory.cokernelOpUnop.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.cokernelOpUnop f =
    { hom := CategoryTheory.Limits.kernel.lift f (CategoryTheory.Limits.cokernel.π f.op).unop ⋯,
      inv := (CategoryTheory.Limits.cokernel.desc f.op (CategoryTheory.Limits.kernel.ι f).op ⋯).unop, hom_inv_id := ⋯,
      inv_hom_id := ⋯ }
-- Mathlib.Topology.MetricSpace.Ultra.Basic
IsUltrametricDist.ball_eq_of_mem : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [IsUltrametricDist X] {x y : X} {r : ℝ},
  y ∈ Metric.ball x r → Metric.ball x r = Metric.ball y r
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Translating a `SlashInvariantForm` by `g : GL (Fin 2) ℝ`, to obtain a new
`SlashInvariantForm` of level `g⁻¹ Γ g`.  -/
SlashInvariantForm.translate : {F : Type u_1} →
  {Γ : Subgroup (GL (Fin 2) ℝ)} →
    {k : ℤ} →
      [inst : FunLike F UpperHalfPlane ℂ] →
        [SlashInvariantFormClass F Γ k] → F → (g : GL (Fin 2) ℝ) → SlashInvariantForm (ConjAct.toConjAct g⁻¹ • Γ) k
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
csSup_eq_univ_of_not_bddAbove : ∀ {α : Type u_1} [inst : ConditionallyCompleteLinearOrder α] {s : Set α}, ¬BddAbove s → sSup s = sSup Set.univ
-- Mathlib.Order.Interval.Finset.Basic
transGen_wcovBy_of_le : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrder α] {x y : α},
  x ≤ y → Relation.TransGen (fun x1 x2 => x1 ⩿ x2) x y
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.neg_empty : ∀ {α : Type u_2} [inst : Neg α], -∅ = ∅
-- Mathlib.RingTheory.Extension.Basic
/-- Given an `R`-algebra extension `0 → I → P → S → 0` of `S`,
the infinitesimal extension associated to it is `0 → I/I² → P/I² → S → 0`.  -/
Algebra.Extension.infinitesimal : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Extension R S → Algebra.Extension R S
-- Init.Data.Array.Attach
Array.unattach_filter : ∀ {α : Type u_1} {p : α → Prop} {xs : Array { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → (Array.filter f xs).unattach = Array.filter g xs.unattach
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getD_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α} {fallback : γ},
  (Std.TreeMap.filterMap f t).getD k fallback = (t[k]?.pbind fun x h' => f (t.getKey k ⋯) x).getD fallback
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.neighborSet_subset : ∀ {V : Type u} {G : SimpleGraph V} (G' : G.Subgraph) (v : V), G'.neighborSet v ⊆ G.neighborSet v
-- Mathlib.Data.Finmap
/-- `simp`-normal form of `mem_lookup_union`  -/
Finmap.mem_lookup_union' : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ : Finmap β},
  Finmap.lookup a (s₁ ∪ s₂) = some b ↔ b ∈ Finmap.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ Finmap.lookup a s₂
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.uniformBell_succ_left : ∀ (m n : ℕ), (m + 1).uniformBell n = (m * n + n - 1).choose (n - 1) * m.uniformBell n
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
Filter.EventuallyEq.extDerivWithin_eq_of_insert : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  ω₁ =ᶠ[nhdsWithin x (insert x s)] ω₂ → extDerivWithin ω₁ s x = extDerivWithin ω₂ s x
-- Mathlib.Analysis.Normed.Module.Basic
/-- If `E` is a nontrivial normed space over a nontrivially normed field `𝕜`, then `E` is unbounded:
for any `c : ℝ`, there exists a vector `x : E` with norm strictly greater than `c`.  -/
NormedSpace.exists_lt_norm : ∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [Nontrivial E] (c : ℝ), ∃ x, c < ‖x‖
-- Init.Data.SInt.Lemmas
Int64.toBitVec_ofIntClamp : ∀ {n : ℤ}, Int64.minValue.toInt ≤ n → n ≤ Int64.maxValue.toInt → (Int64.ofIntClamp n).toBitVec = BitVec.ofInt 64 n
-- Mathlib.Geometry.Manifold.Submersion
Manifold.IsSubmersionAtOfComplement.writtenInCharts : ∀ {𝕜 : Type u_1} {E'' : Type u_3} {F : Type u_5} {H : Type u_7} {G : Type u_9} {E : Type u}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  [inst_3 : NormedAddCommGroup E''] [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace 𝕜 F] [inst_7 : TopologicalSpace H] [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} {N : Type u_13} [inst_9 : TopologicalSpace M]
  [inst_10 : ChartedSpace H M] [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N}
  {x : M} (h : Manifold.IsSubmersionAtOfComplement F I J n f x),
  Set.EqOn (↑(h.codChart.extend J) ∘ f ∘ ↑(h.domChart.extend I).symm) (Prod.fst ∘ ⇑h.equiv) (h.domChart.extend I).target
-- Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
CategoryTheory.Limits.pullbackZeroZeroIso_hom_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackZeroZeroIso X Y).hom
      CategoryTheory.Limits.prod.snd =
    CategoryTheory.Limits.pullback.snd 0 0
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.fixingSubgroup_top : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [hGKL : IsGaloisGroup G K L], fixingSubgroup G ↑⊤ = ⊥
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
/-- Any two injective resolutions are homotopy equivalent.  -/
CategoryTheory.InjectiveResolution.homotopyEquiv : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X : C} → (I J : CategoryTheory.InjectiveResolution X) → HomotopyEquiv I.cocomplex J.cocomplex
-- Mathlib.Data.Prod.Basic
Prod.fst_surjective : ∀ {α : Type u_1} {β : Type u_2} [h : Nonempty β], Function.Surjective Prod.fst
-- Mathlib.Tactic.FunProp.Elab
_private.Mathlib.Tactic.FunProp.Elab.0.Mathlib.Meta.FunProp.assumptionDischarge : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Computability.Language
/-- The sum of two languages is their union.  -/
Language.instAdd : {α : Type u_1} → Add (Language α)
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.Extension.frob_iterate_apply : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n] (i : ℕ) {x : FiniteField.Extension k p n},
  (FiniteField.Extension.frob k p n ^ i) x = x ^ Nat.card k ^ i
-- Init.Prelude
/-- The homogeneous version of `HOr`: `a ||| b : α` where `a b : α`.
(It is called `OrOp` because `Or` is taken for the propositional connective.)
 -/
OrOp : Type u → Type u
-- Mathlib.CategoryTheory.Triangulated.Generators
CategoryTheory.ObjectProperty.triangEnvelopeIter_succ' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  (P : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C] (n : ℕ),
  P.triangEnvelopeIter (n + 1) =
    ((P.triangEnvelopeIter n).extensionProduct (P.shiftClosure ℤ).binaryProductsClosure.retractClosure).retractClosure
-- Mathlib.RingTheory.Polynomial.IntegralNormalization
Polynomial.integralNormalization_coeff_ne_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {i : ℕ},
  i ≠ p.natDegree → p.integralNormalization.coeff i = p.coeff i * p.leadingCoeff ^ (p.natDegree - 1 - i)
-- Mathlib.Tactic.Widget.StringDiagram
Mathlib.Tactic.Widget.StringDiagram.IdNode.mk : ℕ → ℕ → ℕ → Mathlib.Tactic.BicategoryLike.Atom₁ → Mathlib.Tactic.Widget.StringDiagram.IdNode
-- Mathlib.RingTheory.Perfection
Perfection.liftMonoidHom.eq_1 : ∀ (p : ℕ) (M : Type u_2) [inst : CommMonoid M] [inst_1 : PerfectRing M p] (N : Type u_3) [inst_2 : CommMonoid N],
  Perfection.liftMonoidHom p M N =
    {
      toFun := fun f =>
        { toFun := fun r => ⟨fun n => f ((powMulEquiv M (p ^ n)).symm r), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ },
      invFun := (Perfection.coeffMonoidHom N p 0).comp, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Mathlib.Topology.FiberBundle.Basic
FiberBundle.trivialization_mem_atlas : ∀ {B : Type u_2} (F : Type u_3) [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] (E : B → Type u_5)
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : (b : B) → TopologicalSpace (E b)]
  [inst_4 : FiberBundle F E] (b : B), trivializationAt F E b ∈ trivializationAtlas F E
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInf : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [Min β] → Min (l.Germ β)
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn?.match_1.congr_eq_1 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (l : List α) (h_1 : Unit → motive [])
  (h_2 : (x : α) → (xs : List α) → motive (x :: xs)),
  l = [] →
    (match l with
      | [] => h_1 ()
      | x :: xs => h_2 x xs) ≍
      h_1 ()
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Complete matches of safe rules.  -/
Aesop.ForwardRuleMatches.safeMatches : Aesop.ForwardRuleMatches → Lean.PHashSet Aesop.ForwardRuleMatch
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- If a function has a Taylor series at order at least `1` on a neighborhood of `x`, then the term
of order `1` of this series is a derivative of `f` at `x`.  -/
HasFTaylorSeriesUpToOn.hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {x : E} {n : WithTop ℕ∞} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpToOn n f p s → n ≠ 0 → s ∈ nhds x → HasFDerivAt f ((continuousMultilinearCurryFin1 𝕜 E F) (p x 1)) x
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
CategoryTheory.MonoidalCategory.externalProductBifunctorCurried_map_app_app_app : ∀ (J₁ : Type u₁) (J₂ : Type u₂) (C : Type u₃) [inst : CategoryTheory.Category.{v₁, u₁} J₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  [inst_3 : CategoryTheory.MonoidalCategory C] {X Y : CategoryTheory.Functor J₁ C} (f : X ⟶ Y)
  (X_1 : CategoryTheory.Functor J₂ C) (c : J₁) (X_2 : J₂),
  ((((CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C).map f).app X_1).app c).app X_2 =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (f.app c) (X_1.obj X_2)
-- Mathlib.Data.WSeq.Relation
/-- Two weak sequences are `LiftRel R` related if they are either both empty,
or they are both nonempty and the heads are `R` related and the tails are
`LiftRel R` related. (This is a coinductive definition.)  -/
Stream'.WSeq.LiftRel : {α : Type u} → {β : Type v} → (α → β → Prop) → Stream'.WSeq α → Stream'.WSeq β → Prop
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
/-- We don't want to keep carrying the `RingId` around.  -/
Lean.Meta.Grind.Arith.CommRing.RingM : Type → Type
-- Mathlib.Data.Seq.Basic
Stream'.Seq.map_get? : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream'.Seq α) (n : ℕ),
  (Stream'.Seq.map f s).get? n = Option.map f (s.get? n)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_union : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.RefIdentJsonRepr.f.injEq : ∀ (m i m_1 i_1 : String),
  (Lean.Lsp.RefIdent.RefIdentJsonRepr.f m i = Lean.Lsp.RefIdent.RefIdentJsonRepr.f m_1 i_1) = (m = m_1 ∧ i = i_1)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddResult
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.DerivedLitsInvariant.hcongr_6 : ∀ (n n' : ℕ),
  n = n' →
    ∀ (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
      (f' : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n'),
      f ≍ f' →
        ∀ (fassignments_size : f.assignments.size = n) (fassignments_size' : f'.assignments.size = n'),
          fassignments_size ≍ fassignments_size' →
            ∀ (assignments assignments' : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
              assignments = assignments' →
                ∀ (assignments_size : assignments.size = n) (assignments_size' : assignments'.size = n'),
                  assignments_size ≍ assignments_size' →
                    ∀ (derivedLits : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
                      (derivedLits' : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin n')),
                      derivedLits ≍ derivedLits' →
                        f.DerivedLitsInvariant fassignments_size assignments assignments_size derivedLits ≍
                          f'.DerivedLitsInvariant fassignments_size' assignments' assignments_size' derivedLits'
-- Mathlib.Analysis.InnerProductSpace.Basic
_private.Mathlib.Analysis.InnerProductSpace.Basic.0.«term⟪_,_⟫_2» : Lean.ParserDescr
-- Mathlib.RingTheory.IsGaloisGroup.Defs
IsGaloisGroup.of_ringHom_surjective : ∀ (G : Type u_1) (A : Type u_2) (A' : Type u_3) (B : Type u_4) [inst : Group G] [inst_1 : CommSemiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra A B] [inst_4 : MulSemiringAction G B] [hG : IsGaloisGroup G A B]
  [inst_5 : CommSemiring A'] [inst_6 : Algebra A' B] (e : A →+* A'),
  (∀ (a : A), (algebraMap A' B) (e a) = (algebraMap A B) a) → Function.Surjective ⇑e → IsGaloisGroup G A' B
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ResultingUniverseResult.mk.inj : ∀ {u : Lean.Level} {assign? : Option (Lean.LMVarId × Lean.Level)} {u_1 : Lean.Level}
  {assign?_1 : Option (Lean.LMVarId × Lean.Level)},
  { u := u, assign? := assign? } = { u := u_1, assign? := assign?_1 } → u = u_1 ∧ assign? = assign?_1
-- Mathlib.MeasureTheory.Group.FundamentalDomain
_private.Mathlib.MeasureTheory.Group.FundamentalDomain.0.MeasureTheory.termπ_2 : Lean.ParserDescr
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.pure_bind : ∀ {α β : Type u} (f : α → FreeAbelianGroup β) (x : α), pure x >>= f = f x
-- Lean.Parser.Command
Lean.Parser.Command.opaque.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups
/-- A subgroup of the alternating group that contains
the stabilizer of a set acts primitively on that set
if the complement is nontrivial.  -/
alternatingGroup.stabilizer_subgroup_isPreprimitive : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {s : Set α},
  sᶜ.Nontrivial →
    ∀ {G : Subgroup ↥(alternatingGroup α)},
      MulAction.stabilizer (↥(alternatingGroup α)) s ≤ G → MulAction.IsPreprimitive ↥(MulAction.stabilizer (↥G) s) ↑s
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.coe_top : ∀ {M : Type u_1} [inst : AddZeroClass M], ↑⊤ = Set.univ
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
Finsupp.basisSingleOne_repr : ∀ {R : Type u_1} {ι : Type u_3} [inst : Semiring R], Finsupp.basisSingleOne.repr = LinearEquiv.refl R (ι →₀ R)
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.haveLebesgueDecompositionSMul : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ ν : MeasureTheory.Measure α) [μ.HaveLebesgueDecomposition ν] (r : NNReal),
  (r • μ).HaveLebesgueDecomposition ν
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.incl_injective : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] (E : LieAlgebra.Extension R M L), Function.Injective ⇑E.incl
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_sumCoords_of_fintype : ∀ {ι : Type u_10} {R : Type u_11} {M : Type u_12} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (b : Module.Basis ι R M) [inst_3 : Fintype ι], ⇑b.sumCoords = ⇑(∑ i, b.coord i)
-- Mathlib.Order.Fin.Basic
Fin.cast_strictMono : ∀ {k l : ℕ} (h : k = l), StrictMono (Fin.cast h)
-- Mathlib.RingTheory.Congruence.Hom
/-- Given ring congruence relations `c, d` on a ring such that `d` contains `c`,
the definition of the homomorphism from the quotient by `c` to the quotient by
`d` induced by `d`'s quotient map.  -/
RingCon.factorₐ_mk : ∀ {M : Type u_1} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M] {c d : RingCon M}
  (h : c ≤ d) (x : M), (RingCon.factorₐ R h) ⟦x⟧ = ⟦x⟧
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
/-- `F` creates all finite limits.  -/
CategoryTheory.Limits.CreatesFiniteProducts.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.CreatesFiniteProducts F] →
            (J : Type) → [Fintype J] → CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- If the p-adic valuation of a finite set of positive rationals is greater than a given rational
number, then the p-adic valuation of their sum is also greater than the same rational number.  -/
padicValRat.lt_sum_of_lt : ∀ {p j : ℕ} [hp : Fact (Nat.Prime p)] {F : ℕ → ℚ} {S : Finset ℕ},
  S.Nonempty →
    (∀ i ∈ S, padicValRat p (F j) < padicValRat p (F i)) →
      (∀ (i : ℕ), 0 < F i) → padicValRat p (F j) < padicValRat p (∑ i ∈ S, F i)
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `DifferentiableAt.finsetProd`. -/
DifferentiableAt.finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {ι : Type u_2} {𝔸' : Type u_3} [inst_1 : NormedCommRing 𝔸']
  [inst_2 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableAt 𝕜 (f i) x) → DifferentiableAt 𝕜 (∏ i ∈ u, f i) x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_eq_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst_2 : Inhabited α] {k : α}, k ∈ t → t.getKey! k = k
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.Plus.inj_of_sep : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_5 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  (P : CategoryTheory.Functor Cᵒᵖ D),
  (∀ (X : C) (S : J.Cover X) (x y : CategoryTheory.ToType (P.obj (Opposite.op X))),
      (∀ (I : S.Arrow),
          (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) x =
            (CategoryTheory.ConcreteCategory.hom (P.map I.f.op)) y) →
        x = y) →
    ∀ (X : C), Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((J.toPlus P).app (Opposite.op X)))
-- Mathlib.Algebra.Group.WithOne.Basic
WithOne.mapMulHom_injective' : ∀ {α : Type u} {β : Type v} [inst : Mul α] [inst_1 : Mul β], Function.Injective WithOne.mapMulHom
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.mem_grade_iff' : ∀ {M : Type u_1} (R : Type u_3) [inst : CommSemiring R] (m : M) (a : AddMonoidAlgebra R M),
  a ∈ AddMonoidAlgebra.grade R m ↔ a ∈ (AddMonoidAlgebra.lsingle m).range
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
complEDS_one : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (k : ℤ), complEDS b c d k 1 = 1
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.IsSt.add : ∀ {x y : ℝ*} {r s : ℝ}, x.IsSt r → y.IsSt s → (x + y).IsSt (r + s)
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_sub : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u v : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : Sub β],
  MeasureTheory.stoppedValue (u - v) τ = MeasureTheory.stoppedValue u τ - MeasureTheory.stoppedValue v τ
-- Mathlib.Data.Part
Part.someDecidable : {α : Type u_1} → (a : α) → Decidable (Part.some a).Dom
-- Mathlib.Topology.Connected.TotallyDisconnected
isTotallyDisconnected_of_image : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] {s : Set α} [inst_1 : TopologicalSpace β] {f : α → β},
  ContinuousOn f s → Function.Injective f → IsTotallyDisconnected (f '' s) → IsTotallyDisconnected s