ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<GOAL>N ≠ ⊥
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>hK : K ⊔ N = ⊤<GOAL>K = ⊤
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup G<VAR>K.Normal<VAR>hK : K ≤ N<GOAL>K = ⊥ ∨ K = N
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>K : Subgroup ↥N<VAR>(Subgroup.map N.subtype K).Normal<GOAL>K = ⊥ ∨ K = ⊤
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<GOAL>Nat.Prime (Nat.card ↥N).minFac
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<VAR>P : Sylow (Nat.card ↥N).minFac ↥N<GOAL>↑P ≠ ⊥
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<GOAL>IsPGroup (Nat.card ↥N).minFac ↥N
<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>N : Subgroup G<VAR>N.Normal<VAR>h1 : (Nat.card ↥N).Coprime N.index<VAR>h2 : ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'], Nat.card G' < Nat.card G → ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'<VAR>h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H<GOAL>N.IsCommutative
<VAR>n : ℕ<VAR>G : Type u<VAR>Group G<VAR>Finite G<VAR>hG : Nat.card G = n<VAR>N : Subgroup G<VAR>N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<GOAL>∃ H, N.IsComplement' H
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<GOAL>∃ H, N.IsComplement' H
<VAR>G : Type u<VAR>Group G<VAR>N : Subgroup G<VAR>N.Normal<VAR>hN : (Nat.card ↥N).Coprime N.index<GOAL>∃ H, H.IsComplement' N
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>self : LawfulBifunctor F<VAR>α : Type u₀<VAR>β : Type u₁<VAR>x : F α β<GOAL>bimap id id x = x
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>self : LawfulBifunctor F<VAR>α₀ α₁ α₂ : Type u₀<VAR>β₀ β₁ β₂ : Type u₁<VAR>f : α₀ → α₁<VAR>f' : α₁ → α₂<VAR>g : β₀ → β₁<VAR>g' : β₁ → β₂<VAR>x : F α₀ β₀<GOAL>bimap f' g' (bimap f g x) = bimap (f' ∘ f) (g' ∘ g) x
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α : Type u₀<VAR>β : Type u₁<VAR>x : F α β<GOAL>Bifunctor.fst id x = x
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α : Type u₀<VAR>β : Type u₁<GOAL>Bifunctor.fst id = id
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α : Type u₀<VAR>β : Type u₁<GOAL>Bifunctor.snd id = id
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α : Type u₀<VAR>β : Type u₁<VAR>x : F α β<GOAL>Bifunctor.snd id x = x
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α₀ α₁ α₂ : Type u₀<VAR>β : Type u₁<VAR>f : α₀ → α₁<VAR>f' : α₁ → α₂<VAR>x : F α₀ β<GOAL>Bifunctor.fst f' (Bifunctor.fst f x) = Bifunctor.fst (f' ∘ f) x
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α₀ α₁ α₂ : Type u₀<VAR>β : Type u₁<VAR>f : α₀ → α₁<VAR>f' : α₁ → α₂<GOAL>Bifunctor.fst f' ∘ Bifunctor.fst f = Bifunctor.fst (f' ∘ f)
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α₀ α₁ : Type u₀<VAR>β₀ β₁ : Type u₁<VAR>f : α₀ → α₁<VAR>f' : β₀ → β₁<GOAL>Bifunctor.fst f ∘ Bifunctor.snd f' = bimap f f'
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α₀ α₁ : Type u₀<VAR>β₀ β₁ : Type u₁<VAR>f : α₀ → α₁<VAR>f' : β₀ → β₁<VAR>x : F α₀ β₀<GOAL>Bifunctor.fst f (Bifunctor.snd f' x) = bimap f f' x
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α₀ α₁ : Type u₀<VAR>β₀ β₁ : Type u₁<VAR>f : α₀ → α₁<VAR>f' : β₀ → β₁<GOAL>Bifunctor.snd f' ∘ Bifunctor.fst f = bimap f f'
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α₀ α₁ : Type u₀<VAR>β₀ β₁ : Type u₁<VAR>f : α₀ → α₁<VAR>f' : β₀ → β₁<VAR>x : F α₀ β₀<GOAL>Bifunctor.snd f' (Bifunctor.fst f x) = bimap f f' x
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α : Type u₀<VAR>β₀ β₁ β₂ : Type u₁<VAR>g : β₀ → β₁<VAR>g' : β₁ → β₂<GOAL>Bifunctor.snd g' ∘ Bifunctor.snd g = Bifunctor.snd (g' ∘ g)
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>Bifunctor F<VAR>LawfulBifunctor F<VAR>α : Type u₀<VAR>β₀ β₁ β₂ : Type u₁<VAR>g : β₀ → β₁<VAR>g' : β₁ → β₂<VAR>x : F α β₀<GOAL>Bifunctor.snd g' (Bifunctor.snd g x) = Bifunctor.snd (g' ∘ g) x
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>LawfulApplicative F<VAR>α β γ σ : Type u<VAR>f : α → β → γ<VAR>g : σ → β<VAR>x : F α<VAR>y : F σ<GOAL>(Seq.seq (f <$> x) fun x => g <$> y) = Seq.seq (((fun x => x ∘ g) ∘ f) <$> x) fun x => y
<VAR>F : Type u → Type v<VAR>Applicative F<VAR>LawfulApplicative F<VAR>α β : Type u<VAR>f : α → β<GOAL>(fun x => Seq.seq (pure f) fun x_1 => x) = fun x => f <$> x
<VAR>F : Type u → Type u_1<VAR>A1 A2 : Applicative F<VAR>LawfulApplicative F<VAR>LawfulApplicative F<GOAL>(∀ {α : Type u} (x : α), pure x = pure x) → (∀ {α β : Type u} (f : F (α → β)) (x : F α), (Seq.seq f fun x_1 => x) = Seq.seq f fun x_1 => x) → A1 = A2
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α β : Type v<VAR>f : α → β<VAR>x : α<GOAL>f <$> pure x = pure (f x)
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α β : Type v<VAR>f : Functor.Comp F G (α → β)<VAR>x : α<GOAL>(Seq.seq f fun x_1 => pure x) = (fun g => g x) <$> f
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α β γ : Type v<VAR>x : Functor.Comp F G α<VAR>f : Functor.Comp F G (α → β)<VAR>g : Functor.Comp F G (β → γ)<GOAL>(Seq.seq g fun x_1 => Seq.seq f fun x_2 => x) = Seq.seq (Seq.seq (Function.comp <$> g) fun x => f) fun x_1 => x
<VAR>F : Type u → Type w<VAR>G : Type v → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α β : Type v<VAR>f : α → β<VAR>x : Functor.Comp F G α<GOAL>(Seq.seq (pure f) fun x_1 => x) = f <$> x
<VAR>F : Type u_1 → Type u_2<VAR>AF : Applicative F<VAR>LawfulApplicative F<GOAL>Functor.Comp.instApplicativeComp = AF
<VAR>α β : Type w<VAR>f : Type u → Type v<VAR>g : Type w → Type u<VAR>Applicative f<VAR>Applicative g<VAR>h : f (g (α → β))<VAR>x : f (g α)<GOAL>(Seq.seq (Functor.Comp.mk h) fun x_1 => Functor.Comp.mk x) = Functor.Comp.mk (Seq.seq ((fun x x_1 => Seq.seq x fun x => x_1) <$> h) fun x_1 => x)
<VAR>F : Type u → Type u<VAR>Applicative F<VAR>LawfulApplicative F<VAR>α : Type u<VAR>x : id α<GOAL>(fun {α} => (Traversable.PureTransformation F).app α) x = pure x
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>β γ : Type u<VAR>f : β → γ<GOAL>Functor.map f = traverse (pure ∘ f)
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F : Type u → Type u<VAR>Applicative F<VAR>LawfulApplicative F<VAR>α β γ : Type u<VAR>g : α → F β<VAR>f : β → γ<VAR>x : t α<GOAL>Functor.map f <$> traverse g x = traverse (Functor.map f ∘ g) x
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F : Type u → Type u<VAR>Applicative F<VAR>LawfulApplicative F<VAR>α β γ : Type u<VAR>f : β → F γ<VAR>g : α → β<VAR>x : t α<GOAL>traverse f (g <$> x) = traverse (f ∘ g) x
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F : Type u → Type u<VAR>Applicative F<VAR>LawfulApplicative F<VAR>α : Type u<VAR>x : t α<GOAL>traverse pure x = pure x
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>α : Type u<VAR>x : t α<GOAL>sequence (pure <$> x) = pure x
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>LawfulApplicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α : Type u<VAR>x : t (F (G α))<GOAL>sequence (Functor.Comp.mk <$> x) = Functor.Comp.mk (sequence <$> sequence x)
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>LawfulApplicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α : Type u<VAR>η : ApplicativeTransformation F G<VAR>x : t (F α)<GOAL>(fun {α} => η.app α) (sequence x) = sequence ((fun {α} => η.app α) <$> x)
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>α : Type u<GOAL>traverse pure = pure
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>LawfulApplicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → F β<VAR>h : β → G γ<GOAL>traverse (Functor.Comp.mk ∘ Functor.map h ∘ g) = Functor.Comp.mk ∘ Functor.map (traverse h) ∘ traverse g
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>β γ : Type u<VAR>f : β → γ<GOAL>traverse (pure ∘ f) = pure ∘ Functor.map f
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>G : Type u → Type u<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → β<VAR>h : β → G γ<GOAL>traverse (h ∘ g) = traverse h ∘ Functor.map g
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>G : Type u → Type u<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α β γ : Type u<VAR>g : α → G β<VAR>h : β → γ<GOAL>traverse (Functor.map h ∘ g) = Functor.map (Functor.map h) ∘ traverse g
<VAR>t : Type u → Type u<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>LawfulApplicative F<VAR>Applicative G<VAR>LawfulApplicative G<VAR>α β : Type u<VAR>η : ApplicativeTransformation F G<VAR>f : α → F β<GOAL>traverse ((fun {α} => η.app α) ∘ f) = (fun {α} => η.app α) ∘ traverse f
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Functor t<VAR>LawfulFunctor t<VAR>α : Type u<VAR>x : t' α<GOAL>Equiv.map eqv id x = x
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Functor t<VAR>LawfulFunctor t<VAR>α β γ : Type u<VAR>g : α → β<VAR>h : β → γ<VAR>x : t' α<GOAL>Equiv.map eqv (h ∘ g) x = Equiv.map eqv h (Equiv.map eqv g x)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Functor t<VAR>LawfulFunctor t<GOAL>LawfulFunctor t'
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Functor t<VAR>LawfulFunctor t<VAR>F : Functor t'<VAR>h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f<GOAL>LawfulFunctor t'
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Traversable t<VAR>m : Type u → Type u<VAR>Applicative m<VAR>α β : Type u<VAR>f : α → m β<VAR>x : t' α<GOAL>Equiv.traverse eqv f x = ⇑(eqv β) <$> traverse f ((eqv α).symm x)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Traversable t<VAR>LawfulTraversable t<VAR>α : Type u<VAR>x : t' α<GOAL>Equiv.traverse eqv pure x = x
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Traversable t<VAR>LawfulTraversable t<VAR>α β : Type u<VAR>f : α → β<VAR>x : t' α<GOAL>Equiv.traverse eqv (pure ∘ f) x = pure (Equiv.map eqv f x)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>α β γ : Type u<VAR>f : β → F γ<VAR>g : α → G β<VAR>x : t' α<GOAL>Equiv.traverse eqv (Functor.Comp.mk ∘ Functor.map f ∘ g) x = Functor.Comp.mk (Equiv.traverse eqv f <$> Equiv.traverse eqv g x)
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Traversable t<VAR>LawfulTraversable t<VAR>F G : Type u → Type u<VAR>Applicative F<VAR>Applicative G<VAR>LawfulApplicative F<VAR>LawfulApplicative G<VAR>η : ApplicativeTransformation F G<VAR>α β : Type u<VAR>f : α → F β<VAR>x : t' α<GOAL>(fun {α} => η.app α) (Equiv.traverse eqv f x) = Equiv.traverse eqv ((fun {α} => η.app α) ∘ f) x
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Traversable t<VAR>LawfulTraversable t<GOAL>LawfulTraversable t'
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>Traversable t<VAR>LawfulTraversable t<VAR>Traversable t'<VAR>h₀ : ∀ {α β : Type u} (f : α → β), Functor.map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), Functor.mapConst f = (Equiv.map eqv ∘ Function.const α) f<VAR>h₂ : ∀ {F : Type u → Type u} [inst : Applicative F] [inst_1 : LawfulApplicative F] {α β : Type u} (f : α → F β), traverse f = Equiv.traverse eqv f<GOAL>LawfulTraversable t'
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<VAR>x : G<GOAL>x ∈ upperCentralSeriesStep H ↔ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ H
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<GOAL>upperCentralSeriesStep H = Subgroup.comap (QuotientGroup.mk' H) (Subgroup.center (G ⧸ H))
<VAR>G : Type u_1<VAR>Group G<GOAL>upperCentralSeries G 0 = ⊥
<VAR>G : Type u_1<VAR>Group G<GOAL>upperCentralSeries G 1 = Subgroup.center G
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<VAR>x : G<GOAL>x ∈ upperCentralSeries G (n + 1) ↔ ∀ (y : G), x * y * x⁻¹ * y⁻¹ ∈ upperCentralSeries G n
<VAR>G : Type u_2<VAR>Group G<VAR>self : Group.IsNilpotent G<GOAL>∃ n, upperCentralSeries G n = ⊤
<VAR>G : Type u_2<VAR>Group G<VAR>Group.IsNilpotent G<GOAL>∃ n, upperCentralSeries G n = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : ℕ → Subgroup G<VAR>hH : IsAscendingCentralSeries H<VAR>n : ℕ<GOAL>H n ≤ upperCentralSeries G n
<VAR>G : Type u_1<VAR>Group G<GOAL>IsAscendingCentralSeries (upperCentralSeries G)
<VAR>G : Type u_1<VAR>Group G<GOAL>Monotone (upperCentralSeries G)
<VAR>G : Type u_1<VAR>Group G<GOAL>Group.IsNilpotent G ↔ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>H : ℕ → Subgroup G<VAR>n : ℕ<VAR>hn : H n = ⊤<VAR>hasc : IsAscendingCentralSeries H<GOAL>IsDescendingCentralSeries fun m => H (n - m)
<VAR>G : Type u_1<VAR>Group G<VAR>H : ℕ → Subgroup G<VAR>n : ℕ<VAR>hn : H n = ⊥<VAR>hdesc : IsDescendingCentralSeries H<GOAL>IsAscendingCentralSeries fun m => H (n - m)
<VAR>G : Type u_1<VAR>Group G<GOAL>Group.IsNilpotent G ↔ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
<VAR>G : Type u_1<VAR>Group G<GOAL>lowerCentralSeries G 0 = ⊤
<VAR>G : Type u_1<VAR>Group G<GOAL>lowerCentralSeries G 1 = commutator G
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<VAR>q : G<GOAL>q ∈ lowerCentralSeries G (n + 1) ↔ q ∈ Subgroup.closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<GOAL>lowerCentralSeries G (n + 1) = Subgroup.closure {x | ∃ p ∈ lowerCentralSeries G n, ∃ q ∈ ⊤, p * q * p⁻¹ * q⁻¹ = x}
<VAR>G : Type u_1<VAR>Group G<GOAL>Antitone (lowerCentralSeries G)
<VAR>G : Type u_1<VAR>Group G<GOAL>IsDescendingCentralSeries (lowerCentralSeries G)
<VAR>G : Type u_1<VAR>Group G<VAR>H : ℕ → Subgroup G<VAR>hH : IsDescendingCentralSeries H<VAR>n : ℕ<GOAL>lowerCentralSeries G n ≤ H n
<VAR>G : Type u_1<VAR>Group G<GOAL>Group.IsNilpotent G ↔ ∃ n, lowerCentralSeries G n = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>hG : Group.IsNilpotent G<GOAL>upperCentralSeries G (Group.nilpotencyClass G) = ⊤
<VAR>G : Type u_1<VAR>Group G<VAR>hG : Group.IsNilpotent G<VAR>n : ℕ<GOAL>upperCentralSeries G n = ⊤ ↔ Group.nilpotencyClass G ≤ n
<VAR>G : Type u_1<VAR>Group G<VAR>hG : Group.IsNilpotent G<GOAL>Nat.find ⋯ = Group.nilpotencyClass G
<VAR>G : Type u_1<VAR>Group G<VAR>hG : Group.IsNilpotent G<GOAL>lowerCentralSeries G (Group.nilpotencyClass G) = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>hG : Group.IsNilpotent G<VAR>n : ℕ<GOAL>lowerCentralSeries G n = ⊥ ↔ Group.nilpotencyClass G ≤ n
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>n : ℕ<GOAL>Subgroup.map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>hG : Group.IsNilpotent G<GOAL>Group.nilpotencyClass ↥H ≤ Group.nilpotencyClass G
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>f : G →* H<VAR>h : Function.Surjective ⇑f<VAR>n : ℕ<GOAL>Subgroup.map f (upperCentralSeries G n) ≤ upperCentralSeries H n
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>f : G →* H<VAR>n : ℕ<GOAL>Subgroup.map f (lowerCentralSeries G n) ≤ lowerCentralSeries H n
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<VAR>h : lowerCentralSeries G n ≤ Subgroup.center G<GOAL>lowerCentralSeries G (n + 1) = ⊥
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ Subgroup.center G<VAR>hH : Group.IsNilpotent H<GOAL>Group.IsNilpotent G
<VAR>G : Type u_1<VAR>Group G<VAR>H : Type u_2<VAR>Group H<VAR>f : G →* H<VAR>hf1 : f.ker ≤ Subgroup.center G<VAR>hH : Group.IsNilpotent H<GOAL>Group.nilpotencyClass G ≤ Group.nilpotencyClass H + 1
<VAR>G : Type u_1<VAR>Group G<VAR>G' : Type u_2<VAR>Group G'<VAR>h : Group.IsNilpotent G<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<GOAL>Group.IsNilpotent G'
<VAR>G : Type u_1<VAR>Group G<VAR>G' : Type u_2<VAR>Group G'<VAR>f : G →* G'<VAR>hf : Function.Surjective ⇑f<VAR>h : Group.IsNilpotent G<GOAL>Group.nilpotencyClass G' ≤ Group.nilpotencyClass G
<VAR>G : Type u_1<VAR>Group G<VAR>G' : Type u_2<VAR>Group G'<VAR>_h : Group.IsNilpotent G<VAR>f : G ≃* G'<GOAL>Group.IsNilpotent G'
<VAR>G : Type u_1<VAR>Group G<VAR>H : Subgroup G<VAR>H.Normal<VAR>_h : Group.IsNilpotent G<GOAL>Group.nilpotencyClass (G ⧸ H) ≤ Group.nilpotencyClass G
<VAR>G : Type u_1<VAR>Group G<VAR>H₁ H₂ : Subgroup G<VAR>H₁.Normal<VAR>H₂.Normal<VAR>h : H₁ = H₂<GOAL>Subgroup.comap (QuotientGroup.mk' H₁) (Subgroup.center (G ⧸ H₁)) = Subgroup.comap (QuotientGroup.mk' H₂) (Subgroup.center (G ⧸ H₂))
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<GOAL>Subgroup.comap (QuotientGroup.mk' (Subgroup.center G)) (upperCentralSeries (G ⧸ Subgroup.center G) n) = upperCentralSeries G n.succ
<VAR>G : Type u_1<VAR>Group G<VAR>Group.IsNilpotent G<GOAL>Group.nilpotencyClass G = 0 ↔ Subsingleton G
<VAR>G : Type u_1<VAR>Group G<VAR>hH : Group.IsNilpotent G<GOAL>Group.nilpotencyClass (G ⧸ Subgroup.center G) = Group.nilpotencyClass G - 1
<VAR>G : Type u_1<VAR>Group G<VAR>hH : Group.IsNilpotent G<VAR>Nontrivial G<GOAL>Group.nilpotencyClass G = Group.nilpotencyClass (G ⧸ Subgroup.center G) + 1
<VAR>G : Type u_1<VAR>Group G<VAR>h : Group.IsNilpotent (G ⧸ Subgroup.center G)<GOAL>Group.IsNilpotent G
<VAR>P : (G : Type u_2) → [inst : Group G] → [inst : Group.IsNilpotent G] → Prop<VAR>G : Type u_2<VAR>Group G<VAR>Group.IsNilpotent G<VAR>hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G<VAR>hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Group.IsNilpotent G], P (G ⧸ Subgroup.center G) → P G<GOAL>P G
<VAR>G : Type u_1<VAR>Group G<VAR>n : ℕ<GOAL>derivedSeries G n ≤ lowerCentralSeries G n
<VAR>G : Type u_2<VAR>CommGroup G<GOAL>Group.nilpotencyClass G ≤ 1
<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>Group G₁<VAR>Group G₂<VAR>n : ℕ<GOAL>lowerCentralSeries (G₁ × G₂) n = (lowerCentralSeries G₁ n).prod (lowerCentralSeries G₂ n)
<VAR>G₁ : Type u_2<VAR>G₂ : Type u_3<VAR>Group G₁<VAR>Group G₂<VAR>Group.IsNilpotent G₁<VAR>Group.IsNilpotent G₂<GOAL>Group.nilpotencyClass (G₁ × G₂) = max (Group.nilpotencyClass G₁) (Group.nilpotencyClass G₂)
<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>(i : η) → Group (Gs i)<VAR>n : ℕ<GOAL>lowerCentralSeries ((i : η) → Gs i) n ≤ Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>(i : η) → Group (Gs i)<VAR>∀ (i : η), Group.IsNilpotent (Gs i)<VAR>n : ℕ<VAR>h : ∀ (i : η), Group.nilpotencyClass (Gs i) ≤ n<GOAL>Group.IsNilpotent ((i : η) → Gs i)
<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>(i : η) → Group (Gs i)<VAR>Finite η<VAR>n : ℕ<GOAL>lowerCentralSeries ((i : η) → Gs i) n = Subgroup.pi Set.univ fun i => lowerCentralSeries (Gs i) n
<VAR>η : Type u_2<VAR>Gs : η → Type u_3<VAR>(i : η) → Group (Gs i)<VAR>Fintype η<VAR>∀ (i : η), Group.IsNilpotent (Gs i)<GOAL>Group.nilpotencyClass ((i : η) → Gs i) = Finset.univ.sup fun i => Group.nilpotencyClass (Gs i)
<VAR>G : Type u_1<VAR>Group G<VAR>h : Group.IsNilpotent G<GOAL>NormalizerCondition G
<VAR>G : Type u_1<VAR>hG : Group G<VAR>Finite G<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>h : IsPGroup p G<GOAL>Group.IsNilpotent G
<VAR>G : Type u_1<VAR>hG : Group G<VAR>Finite G<VAR>e : ((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G<GOAL>Group.IsNilpotent G
<VAR>G : Type u_1<VAR>hG : Group G<VAR>Finite G<GOAL>[Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal, ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal, Nonempty (((p : { x // x ∈ (Nat.card G).primeFactors }) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE
<VAR>α : Type u_3<VAR>OmegaCompletePartialOrder α<VAR>self : LawfulFix α<VAR>f : α →o α<GOAL>OmegaCompletePartialOrder.Continuous f → Fix.fix ⇑f = f (Fix.fix ⇑f)
<VAR>α : Type u_3<VAR>OmegaCompletePartialOrder α<VAR>LawfulFix α<VAR>f : α → α<VAR>hf : OmegaCompletePartialOrder.Continuous' f<GOAL>Fix.fix f = f (Fix.fix f)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>i : ℕ<GOAL>Part.Fix.approx (⇑f) i ≤ Part.Fix.approx (⇑f) i.succ
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>i j : ℕ<VAR>hij : i ≤ j<GOAL>Part.Fix.approx (⇑f) i ≤ Part.Fix.approx (⇑f) j
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>a : α<VAR>b : β a<GOAL>b ∈ Part.fix (⇑f) a ↔ ∃ i, b ∈ Part.Fix.approx (⇑f) i a
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>i : ℕ<GOAL>Part.Fix.approx (⇑f) i ≤ Part.fix ⇑f
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>x : α<GOAL>∃ i, Part.fix (⇑f) x ≤ Part.Fix.approx (⇑f) i x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>x : (a : α) → Part (β a)<GOAL>x ∈ Part.Fix.approxChain f → x ≤ f x
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>i : ℕ<GOAL>Part.Fix.approx (⇑f) i ∈ Part.Fix.approxChain f
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<GOAL>Part.fix ⇑f = OmegaCompletePartialOrder.ωSup (Part.Fix.approxChain f)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>X : (a : α) → Part (β a)<VAR>hX : f X ≤ X<GOAL>Part.fix ⇑f ≤ X
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)<VAR>hc : OmegaCompletePartialOrder.Continuous f<GOAL>Part.fix ⇑f = f (Part.fix ⇑f)
<VAR>α : Type u_1<VAR>f : Part α →o Part α<VAR>x : Unit → Part α<VAR>u : Unit<GOAL>(Part.toUnitMono f) x u = f (x u)
<VAR>α : Type u_1<VAR>f : Part α →o Part α<VAR>hc : OmegaCompletePartialOrder.Continuous f<GOAL>OmegaCompletePartialOrder.Continuous (Part.toUnitMono f)
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>(x : α) → (y : β x) → Preorder (γ x y)<VAR>f : (x : (a : α) × β a) → γ x.fst x.snd<VAR>x : α<VAR>y : β x<GOAL>(Pi.monotoneCurry α β γ) f x y = Sigma.curry f x y