mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.eq_d₂₁_comp_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : G × G →₀ ↑A),
  (CategoryTheory.ConcreteCategory.hom
        (ChainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) →₀ ↑A))
          (fun n => groupHomology.inhomogeneousChains.d A n) 2 1))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₂ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₁ A).inv)
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₂₁ A)) x)
-- Mathlib.Order.Hom.WithTopBot
WithBot.toDualTopEquiv_symm_bot : ∀ {α : Type u_1} [inst : LE α], WithBot.toDualTopEquiv.symm ⊥ = ⊥
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
/-- The **Erdős–Ginzburg–Ziv theorem** for `ℤ/nℤ` for multiset.

Any multiset of at least `2 * n - 1` elements of `ℤ` contains a submultiset of `n` elements whose
sum is divisible by `n`.  -/
ZMod.erdos_ginzburg_ziv_multiset : ∀ {n : ℕ} (s : Multiset (ZMod n)), 2 * n - 1 ≤ s.card → ∃ t ≤ s, t.card = n ∧ t.sum = 0
-- Mathlib.Analysis.Complex.Trigonometric
Complex.tanh_ofReal_re : ∀ (x : ℝ), (Complex.tanh ↑x).re = Real.tanh x
-- Init.Grind.AC
Lean.Grind.AC.instInhabitedSeq.default : Lean.Grind.AC.Seq
-- Mathlib.Combinatorics.SetFamily.Shadow
Finset.shadow_singleton_empty : ∀ {α : Type u_1} [inst : DecidableEq α], {∅}.shadow = ∅
-- Mathlib.LinearAlgebra.TensorProduct.Tower
Submodule.baseChange_bot : ∀ {R : Type u_1} {M : Type u_2} (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M], Submodule.baseChange A ⊥ = ⊥
-- Mathlib.Tactic.Core
/-- Repeats a tactic at most `n` times, stopping sooner if the
tactic fails. Always succeeds.  -/
Lean.Elab.Tactic.iterateAtMost : {m : Type → Type u} → [Monad m] → [MonadExcept Lean.Exception m] → ℕ → m Unit → m Unit
-- Mathlib.RingTheory.Nullstellensatz
/-- Ideal of polynomials with common zeroes at all elements of a set  -/
MvPolynomial.vanishingIdeal : (k : Type u_1) →
  {K : Type u_2} →
    [inst : Field k] → [inst_1 : Field K] → [Algebra k K] → {σ : Type u_3} → Set (σ → K) → Ideal (MvPolynomial σ k)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.node.eq_1 : ∀ (n i : ℕ), Polynomial.Chebyshev.node n i = Real.cos (↑i * Real.pi / ↑n)
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Real.Gamma_nonneg_of_nonneg : ∀ {s : ℝ}, 0 ≤ s → 0 ≤ Real.Gamma s
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.coe_comp_coe : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] (S : CategoryTheory.Subgroupoid C) {X Y Z : ↑S.objs}
  (p : ↑(S.arrows ↑X ↑Y)) (q : ↑(S.arrows ↑Y ↑Z)),
  ↑(CategoryTheory.CategoryStruct.comp p q) = CategoryTheory.CategoryStruct.comp ↑p ↑q
-- Init.Data.Array.Lemmas
Array.prod_append : ∀ {α : Type u_1} [inst : One α] [inst_1 : Mul α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulLeftIdentity (fun x1 x2 => x1 * x2) 1] {as₁ as₂ : Array α}, (as₁ ++ as₂).prod = as₁.prod * as₂.prod
-- Std.Tactic.Do.Syntax
/-- `mpure` moves a pure hypothesis from the stateful context into the pure context.
```lean
example (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
  mintro Hφ
  mpure Hφ
  mexact (ψ Hφ)
```
 -/
Lean.Parser.Tactic.mpureError : Lean.ParserDescr
-- Mathlib.Algebra.Opposites
MulOpposite.eq_1 : ∀ (α : Type u_3), αᵐᵒᵖ = PreOpposite α
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.instBraidedCategoryOverScheme : {S : AlgebraicGeometry.Scheme} → CategoryTheory.BraidedCategory (CategoryTheory.Over S)
-- Mathlib.Data.Nat.Choose.Sum
/-- Summing `i * (n.choose i)` for `i ∈ [0, n]` gives `n * 2 ^ (n - 1)`.  -/
Nat.sum_range_mul_choose : ∀ (n : ℕ), ∑ i ∈ Finset.range (n + 1), i * n.choose i = n * 2 ^ (n - 1)
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.continuousOn_Ico : ∀ {f : ℝ → ℝ} {y z : ℝ}, ConvexOn ℝ (Set.Ico y z) f → ContinuousWithinAt f (Set.Ici y) y → ContinuousOn f (Set.Ico y z)
-- Mathlib.Data.Finsupp.Option
Finsupp.eq_option_embedding_update_none_iff : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {n : Option α →₀ M} {m : α →₀ M} {i : M},
  n = (Finsupp.embDomain Function.Embedding.some m).update none i ↔ n none = i ∧ n.some = m
-- Mathlib.AlgebraicTopology.SimplicialSet.Splitting
SSet.splitting_N : ∀ (X : SSet) (n : ℕ), X.splitting.N n = ↑(X.nonDegenerate n)
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_functor_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  (G : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C) (X_1 : (TopologicalSpace.Opens ↑Y)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).functor.obj G).obj X_1 =
    G.obj (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj (Opposite.unop X_1)))
-- Mathlib.Data.Rel
SetRel.preimage.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β), R.preimage t = {a | ∃ b ∈ t, (a, b) ∈ R}
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoFactorisation : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} → CategoryTheory.Limits.StrongEpiMonoFactorisation f → CategoryTheory.Limits.MonoFactorisation f
-- Init.Prelude
/-- `a - b` computes the difference of `a` and `b`.
The meaning of this notation is type-dependent.
* For natural numbers, this operator saturates at 0: `a - b = 0` when `a ≤ b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `-` in identifiers is `sub` (when used as a binary operator). -/
HSub.hSub : {α : Type u} → {β : Type v} → {γ : outParam (Type w)} → [self : HSub α β γ] → α → β → γ
-- Mathlib.Topology.Algebra.Order.Floor
FloorSemiring.tendsto_pow_div_factorial_atTop : ∀ {K : Type u_1} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [FloorSemiring K]
  [inst_4 : TopologicalSpace K] [OrderTopology K] (c : K),
  Filter.Tendsto (fun n => c ^ n / ↑n.factorial) Filter.atTop (nhds 0)
-- Mathlib.AlgebraicGeometry.StructureSheaf
_private.Mathlib.AlgebraicGeometry.StructureSheaf.0.AlgebraicGeometry.StructureSheaf.stalkIsoₗ_hom : ∀ (R M : Type u) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)),
  (AlgebraicGeometry.StructureSheaf.stalkIsoₗ✝ R M x).hom = AlgebraicGeometry.StructureSheaf.stalkToLocalizationₗ✝ R M x
-- Std.Data.ExtTreeSet.Basic
Std.ExtTreeSet.empty_eq_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, Std.ExtTreeSet.empty = ∅
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.liftRel_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Stream'.WSeq α}
  {s2 : Stream'.WSeq β} {f1 : α → γ} {f2 : β → δ},
  Stream'.WSeq.LiftRel R s1 s2 →
    (∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)) →
      Stream'.WSeq.LiftRel S (Stream'.WSeq.map f1 s1) (Stream'.WSeq.map f2 s2)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, m.contains a = false → m.get! a = default
-- Mathlib.Data.PFunctor.Multivariate.M
MvPFunctor.M.Path.root.injEq : ∀ {n : ℕ} {P : MvPFunctor.{u} (n + 1)} (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M) (h : x.dest = ⟨a, f⟩)
  (i : Fin2 n) (c : P.drop.B a i) (a_1 : P.A) (f_1 : P.last.B a_1 → P.last.M) (h_1 : x.dest = ⟨a_1, f_1⟩)
  (c_1 : P.drop.B a_1 i),
  (MvPFunctor.M.Path.root x a f h i c = MvPFunctor.M.Path.root x a_1 f_1 h_1 i c_1) = (a = a_1 ∧ f ≍ f_1 ∧ c ≍ c_1)
-- Batteries.Data.Fin.Coding
Fin.encodeProd_decodeProd : ∀ {m n : ℕ} (x : Fin (m * n)), Fin.encodeProd (Fin.decodeProd x) = x
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_summable_of_mem_ball' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸]
  [CompleteSpace 𝔸], ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, Summable fun n => (↑n.factorial)⁻¹ • x ^ n
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.closedBallSubgroup.eq_1 : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M]
  (c : FiniteMulArchimedeanClass M), c.closedBallSubgroup = FiniteMulArchimedeanClass.subgroup (UpperSet.Ici c)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- `pb.equivAdjoinSimple` is the equivalence between `K⟮pb.gen⟯` and `L` itself.  -/
PowerBasis.equivAdjoinSimple : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → (pb : PowerBasis K L) → ↥K⟮pb.gen⟯ ≃ₐ[K] L
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.instForInSigmaOfMonad : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → {m : Type w → Type w₂} → [Monad m] → ForIn m (Std.DTreeMap α β cmp) ((a : α) × β a)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.maxKey_le : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {he : t.isEmpty = false}, (cmp (t.maxKey he) k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.app_δ_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C}
  (self : CategoryTheory.ComonadHom M N) (X : C) {Z : C} (h : N.obj (N.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.app X) (CategoryTheory.CategoryStruct.comp (N.δ.app X) h) =
    CategoryTheory.CategoryStruct.comp (M.δ.app X)
      (CategoryTheory.CategoryStruct.comp (self.app (M.obj X))
        (CategoryTheory.CategoryStruct.comp (N.map (self.app X)) h))
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_nat_mul_pi_sub : ∀ (x : ℝ) (n : ℕ), Real.cos (↑n * Real.pi - x) = (-1) ^ n * Real.cos x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_eq_false_iff_exists_contains_eq_true : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ((↑m).isEmpty = false ↔ ∃ a, m.contains a = true)
-- Lean.Elab.PreDefinition.WF.GuessLex
Lean.Elab.WF.GuessLex.instInhabitedBasicMeasure : Inhabited Lean.Elab.WF.GuessLex.BasicMeasure
-- Lean.DocString.Types
Lean.Doc.DescItem.mk.sizeOf_spec : ∀ {α : Type u} {β : Type v} [inst : SizeOf α] [inst_1 : SizeOf β] (term : Array α) (desc : Array β),
  sizeOf { term := term, desc := desc } = 1 + sizeOf term + sizeOf desc
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Naturality of the `prodComparison` morphism in the left argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerRight_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B A' : C} (f : A ⟶ A') {Z : D}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj A') (F.obj B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f B))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A' B) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj B)) h)
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `dist_eq_norm`.  -/
hammingDist_eq_hammingNorm : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → AddGroup (β i)] (x y : (i : ι) → β i), hammingDist x y = hammingNorm (-x + y)
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyMap_nullHomotopic : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S₁ S₂ : CategoryTheory.ShortComplex C) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology]
  (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : CategoryTheory.CategoryStruct.comp h₀ S₂.f = 0) (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂)
  (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : CategoryTheory.CategoryStruct.comp S₁.g h₃ = 0),
  CategoryTheory.ShortComplex.leftHomologyMap (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) = 0
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
/-- Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.

This is a computable alternative to `AlgEquiv.ofInjective`.  -/
AlgEquiv.ofLeftInverse : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → {g : B → A} → {f : A →ₐ[R] B} → Function.LeftInverse g ⇑f → A ≃ₐ[R] ↥f.range
-- Mathlib.Order.Hom.Bounded
TopHom.instDistribLattice.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Top α] [inst_1 : DistribLattice β] [inst_2 : OrderTop β],
  TopHom.instDistribLattice = Function.Injective.distribLattice DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
/-- **Alias** of `ContinuousLinearEquiv.coord_norm'`. -/
coord_norm' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E}
  (h : x ≠ 0), ‖↑‖x‖ • ContinuousLinearEquiv.coord 𝕜 x h‖ = 1
-- Mathlib.Tactic.Linter.Multigoal
/-- The `SyntaxNodeKind`s in `exclusions` correspond to tactics that the linter allows,
even though there are multiple active goals.
Reasons for admitting a kind in `exclusions` include
* the tactic focuses on one goal, e.g. `·`, `focus`, `on_goal i =>`, ...;
* the tactic is reordering the goals, e.g. `swap`, `rotate_left`, ...;
* the tactic is structuring a proof, e.g. `skip`, `<;>`, ...;
* the tactic is creating new goals, e.g. `constructor`, `cases`, `induction`, ....

There is some overlap in scope between `ignoreBranch` and `exclusions`.

Tactic combinators like `repeat` or `try` are a mix of both.
 -/
_private.Mathlib.Tactic.Linter.Multigoal.0.Mathlib.Linter.Style.multiGoal.exclusions : Std.HashSet Lean.SyntaxNodeKind
-- Mathlib.Logic.Lemmas
dite_ite_distrib_left : ∀ {α : Sort u_1} {p q : Prop} [inst : Decidable p] [inst_1 : Decidable q] {a : p → α} {b c : ¬p → α},
  (dite p a fun hp => if q then b hp else c hp) = if q then dite p a b else dite p a c
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.instIsContinuousOverPullbackOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.Over.pullback f).IsContinuous (J.over Y) (J.over X)
-- Mathlib.RingTheory.TensorProduct.Pi
Algebra.TensorProduct.piRightHom_one : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] {ι : Type u_4}
  (B : ι → Type u_5) [inst_7 : (i : ι) → Semiring (B i)] [inst_8 : (i : ι) → Algebra R (B i)],
  (TensorProduct.piRightHom R S A B) 1 = 1
-- Mathlib.RingTheory.Localization.BaseChange
instIsLocalizedModuleTensorProductSemilinearMapAlgHomToAlgHom : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [IsLocalization S A] {T : Type u_5} [inst_4 : CommSemiring T] [inst_5 : Algebra R T],
  IsLocalizedModule S ↑(IsScalarTower.toAlgHom R T (TensorProduct R A T))
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.ext : ∀ {M : Type u_4} {N : Type u_5} [inst : AddZero M] [inst_1 : AddZero N] ⦃f g : M →+ N⦄, (∀ (x : M), f x = g x) → f = g
-- Init.Meta.Defs
/-- If the provided `Syntax` is a string literal, returns the string it represents.

Even if the `Syntax` is a `str` node, the function may return `none` if its internally ill-formed.
The parser should always create well-formed `str` nodes.
 -/
Lean.Syntax.isStrLit? : Lean.Syntax → Option String
-- Mathlib.Analysis.Distribution.TestFunction
/-- **Alias** of `FunLike.coeAddMonoidHom`. -/
TestFunction.coeFnAddMonoidHom : (F : Type u_1) →
  (α : Type u_2) →
    (β : Type u_3) →
      [inst : FunLike F α β] →
        [inst_1 : AddZero F] → [inst_2 : AddZeroClass β] → [IsZeroApply F α β] → [IsAddApply F α β] → F →+ α → β
-- Mathlib.Topology.Partial
rtendsto'_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {r : SetRel Y X} {l : Filter Y} {x : X},
  Filter.RTendsto' r l (nhds x) ↔ ∀ (s : Set X), IsOpen s → x ∈ s → r.preimage s ∈ l
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Subgroup.upperCentralSeries`.

---

`upperCentralSeries G n` is the `n`th term in the upper central series of `G`.

This is the increasing chain of subgroups of `G` that starts with the trivial subgroup `⊥` of `G`
and then continues defining `upperCentralSeries G (n + 1)` to be all the elements of `G`
that, modulo `upperCentralSeries G n`, belong to the center of the quotient
`G ⧸ upperCentralSeries G n`.

In particular, the identities
* `upperCentralSeries G 0 = ⊥` (`upperCentralSeries_zero`);
* `upperCentralSeries G 1 = center G` (`upperCentralSeries_one`);

hold.
 -/
upperCentralSeries : (G : Type u_1) → [inst : Group G] → ℕ → Subgroup G
-- Lean.Elab.Exception
Lean.Elab.isAbortTacticException : Lean.Exception → Bool
-- Mathlib.Data.Set.Basic
Set.powerset_mono : ∀ {α : Type u} {s t : Set α}, 𝒫 s ⊆ 𝒫 t ↔ s ⊆ t
-- Mathlib.GroupTheory.GroupAction.Primitive
MulAction.IsPreprimitive.of_subsingleton : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] [Nonempty G] [Subsingleton X], MulAction.IsPreprimitive G X
-- Mathlib.Algebra.Algebra.Equiv
/-- If `A₁` is equivalent to `A₁'` and `A₂` is equivalent to `A₂'`, then the type of maps
`A₁ →ₐ[R] A₂` is equivalent to the type of maps `A₁' →ₐ[R] A₂'`.  -/
AlgEquiv.arrowCongr : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      {A₁' : Type uA₁'} →
        {A₂' : Type uA₂'} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A₁] →
              [inst_2 : Semiring A₂] →
                [inst_3 : Semiring A₁'] →
                  [inst_4 : Semiring A₂'] →
                    [inst_5 : Algebra R A₁] →
                      [inst_6 : Algebra R A₂] →
                        [inst_7 : Algebra R A₁'] →
                          [inst_8 : Algebra R A₂'] → (A₁ ≃ₐ[R] A₁') → (A₂ ≃ₐ[R] A₂') → (A₁ →ₐ[R] A₂) ≃ (A₁' →ₐ[R] A₂')
-- Mathlib.GroupTheory.Congruence.Hom
/-- The kernel of a multiplicative homomorphism as a congruence relation.  -/
Con.ker : {M : Type u_1} →
  {N : Type u_2} →
    {F : Type u_4} → [inst : Mul M] → [inst_1 : Mul N] → [inst_2 : FunLike F M N] → [MulHomClass F M N] → F → Con M
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Version of `exponent_min` using `ExpChar`.  -/
IsPurelyInseparable.exponent_min' : ∀ {K : Type u_2} {L : Type u_3} [inst : CommRing K] [inst_1 : Ring L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [ExpChar K p] {e : ℕ},
  e < IsPurelyInseparable.exponent K L → ∃ a, a ^ p ^ e ∉ (algebraMap K L).range
-- Mathlib.Logic.Relation
/-- **Alias** of `irrefl_iff_le_ne`. -/
irreflexive_iff_subrelation_ne : ∀ {α : Type u_1} {r : α → α → Prop}, Std.Irrefl r ↔ r ≤ Ne
-- Mathlib.GroupTheory.GroupAction.Hom
DistribMulActionHom.mk.sizeOf_spec : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_10}
  [inst_2 : AddMonoid A] [inst_3 : DistribMulAction M A] {B : Type u_11} [inst_4 : AddMonoid B]
  [inst_5 : DistribMulAction N B] [inst_6 : SizeOf M] [inst_7 : SizeOf N] [inst_8 : SizeOf A] [inst_9 : SizeOf B]
  (toMulActionHom : A →ₑ[⇑φ] B) (map_zero' : toMulActionHom.toFun 0 = 0)
  (map_add' : ∀ (x y : A), toMulActionHom.toFun (x + y) = toMulActionHom.toFun x + toMulActionHom.toFun y),
  sizeOf { toMulActionHom := toMulActionHom, map_zero' := map_zero', map_add' := map_add' } =
    1 + sizeOf toMulActionHom + sizeOf map_zero'
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from variables to their "upper" bounds. We say a relational constraint `c` is a upper bound for a variable `x`
if `x` is the maximal variable in `c`, and `x` coefficient in `c` is positive.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.uppers : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
/-- The property of preserving kernels expressed in terms of kernel forks.

This is a variant of `isLimitForkMapOfIsLimit` for equalizers,
which we can't use directly between `G.map 0 = 0` does not hold definitionally.
 -/
CategoryTheory.Limits.isLimitForkMapOfIsLimit' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (G : CategoryTheory.Functor C D) →
              [inst_4 : G.PreservesZeroMorphisms] →
                {X Y Z : C} →
                  {f : X ⟶ Y} →
                    {h : Z ⟶ X} →
                      (w : CategoryTheory.CategoryStruct.comp h f = 0) →
                        [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) G] →
                          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι h w) →
                            CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (G.map h) ⋯)
-- Mathlib.Combinatorics.SimpleGraph.Hamiltonian
SimpleGraph.not_isHamiltonian_of_card_eq_two : ∀ {α : Type u_1} [inst : DecidableEq α] {G : SimpleGraph α} [inst_1 : Fintype α], Fintype.card α = 2 → ¬G.IsHamiltonian
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.mul_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (f g : M ≃ₗ[R] M)
  (x : M), (f * g) x = f (g x)
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_comp : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H] {K : Type u_3}
  [inst_2 : SeminormedAddCommGroup K] (f : NormedAddGroupHom G H) (g : NormedAddGroupHom H K),
  g.completion.comp f.completion = (g.comp f).completion
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Iso.unop_trans : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} (α : X ≅ Y) (β : Y ≅ Z),
  (α ≪≫ β).unop = β.unop ≪≫ α.unop
-- Batteries.Data.List.Basic
List.takeD.eq_def : ∀ {α : Type u_1} (x : ℕ) (x_1 : List α) (x_2 : α),
  List.takeD x x_1 x_2 =
    match x, x_1, x_2 with
    | 0, x, x_3 => []
    | n.succ, l, x => l.headD x :: List.takeD n l.tail x
-- Mathlib.Tactic.Linter.DeprecatedSyntaxLinter
/-- `getDeprecatedSyntax t` returns all usages of deprecated syntax in the input syntax `t`.  -/
_private.Mathlib.Tactic.Linter.DeprecatedSyntaxLinter.0.Mathlib.Linter.Style.getDeprecatedSyntax : Lean.Syntax → Array (Lean.SyntaxNodeKind × Lean.Syntax × Lean.MessageData)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get!_eq_getD_default : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {a : α}, t.get! a = t.getD a default
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.ext_iff₂ : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {x : AddZeroClass M} {x_1 : AddZeroClass N} {x_2 : AddCommMonoid P}
  {f g : M →+ N →+ P}, f = g ↔ ∀ (x_3 : M) (y : N), (f x_3) y = (g x_3) y
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
algebraicIndependent_image : ∀ {R : Type u_3} {A : Type u_5} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {ι : Type u_7}
  {s : Set ι} {f : ι → A}, Set.InjOn f s → ((AlgebraicIndependent R fun x => f ↑x) ↔ AlgebraicIndependent R fun x => ↑x)