mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case pos
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
⊢ E (loopOfHom T (of e)) = 1

pp: case neg
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∉ wideSubquiverSymmetrify T a b
⊢ E (loopOfHom T (of e)) = f ⟨{ left := a, right := b, hom := e }, h⟩

Tactic:
·

Goal state after:
case pos
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∈ wideSubquiverSymmetrify T a b
⊢ E (loopOfHom T (of e)) = 1
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range →
    (g, h) ∈ I

Tactic:
·

Goal state after:
case mpr
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := ⋯
H' : Subgroup H := ⋯
P : ↥I →* ↥G' := ⋯
Q : ↥I →* ↥H' := ⋯
I' : Subgroup (↥G' × ↥H') := ⋯
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : G
h : H
⊢ (g, h) ∈ map ((map (MonoidHom.fst G H) I).subtype.prodMap (map (MonoidHom.snd G H) I).subtype) (P.prod Q).range →
    (g, h) ∈ I
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case inr
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
this :
  ∀ {G : Type u_1} [inst : Group G] {a b c : ℕ},
    a ≠ b →
      a ≤ c → upperCentralSeries G a = upperCentralSeries G b → a < b → upperCentralSeries G a = upperCentralSeries G c
ab : ¬a < b
⊢ upperCentralSeries G a = upperCentralSeries G c

pp: G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G a = upperCentralSeries G c

Tactic:
·

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
this :
  ∀ {G : Type u_1} [inst : Group G] {a b c : ℕ},
    a ≠ b →
      a ≤ c → upperCentralSeries G a = upperCentralSeries G b → a < b → upperCentralSeries G a = upperCentralSeries G c
ab : ¬a < b
⊢ upperCentralSeries G a = upperCentralSeries G c
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case neg
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∉ wideSubquiverSymmetrify T a b
⊢ E (loopOfHom T (of e)) = f ⟨{ left := a, right := b, hom := e }, h⟩

Tactic:
·

Goal state after:
case neg
G : Type u
inst✝³ : Groupoid G
inst✝² : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝¹ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
X : Type u
inst✝ : Group X
f : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ → X
f' : Labelling (Generators G) X :=
  fun a b e ↦ if h : e ∈ wideSubquiverSymmetrify T a b then 1 else f ⟨{ left := a, right := b, hom := e }, h⟩
F' : G ⥤ CategoryTheory.SingleObj X
hF' : ∀ (a b : Generators G) (g : a ⟶ b), F'.map (of g) = f' g
uF' :
  ∀ (y : G ⥤ CategoryTheory.SingleObj X), (fun F ↦ ∀ (a b : Generators G) (g : a ⟶ b), F.map (of g) = f' g) y → y = F'
E : End (root' T) →* X
hE : ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), E (loopOfHom T (of (↑a).hom)) = f a
x : End (root' T)
a b : Generators G
e : a ⟶ b
h : e ∉ wideSubquiverSymmetrify T a b
⊢ E (loopOfHom T (of e)) = f ⟨{ left := a, right := b, hom := e }, h⟩
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G a ≤ upperCentralSeries G (a + 1)

pp: case refine_2
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G (a + 1) ≤ upperCentralSeries G a

Tactic:
·

Goal state after:
case refine_1
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G a ≤ upperCentralSeries G (a + 1)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G (a + 1) ≤ upperCentralSeries G a

Tactic:
·

Goal state after:
case refine_2
G✝ : Type u_1
inst✝¹ : Group G✝
G : Type u_1
inst✝ : Group G
a b c : ℕ
ab✝ : a ≠ b
ac : a ≤ c
hn : upperCentralSeries G a = upperCentralSeries G b
ab : a < b
⊢ upperCentralSeries G (a + 1) ≤ upperCentralSeries G a
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a

pp: case neg
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : ¬Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : ¬Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
a b : ℕ
ab : a < b
hn : upperCentralSeries G a = upperCentralSeries G b
hG : ¬Group.IsNilpotent G
⊢ nilpotencyClass G ≤ a
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (nilpotencyClass G))

pp: case neg
G : Type u_1
inst✝ : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (nilpotencyClass G))

Tactic:
·

Goal state after:
case pos
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ≤
    (P.prod Q).range

Tactic:
·

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
⊢ ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ≤
    (P.prod Q).range
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case pos.a
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ upperCentralSeries G a ≤ upperCentralSeries G b

pp: case a
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ upperCentralSeries G a ≠ upperCentralSeries G b

Tactic:
·

Goal state after:
case pos.a
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ upperCentralSeries G a ≤ upperCentralSeries G b
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case a
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ upperCentralSeries G a ≠ upperCentralSeries G b

Tactic:
·

Goal state after:
case a
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
a b : ℕ
ab : a < b
ha : a ≤ nilpotencyClass G
hb : b ≤ nilpotencyClass G
⊢ upperCentralSeries G a ≠ upperCentralSeries G b
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (nilpotencyClass G))

Tactic:
·

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
hG : ¬Group.IsNilpotent G
⊢ _root_.StrictMonoOn (upperCentralSeries G) (Set.Iic (nilpotencyClass G))
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ a_1 ∈ upperCentralSeries G '' Set.Iic a, ∃ i, ∃ (_ : i < a + 1), upperCentralSeries G i = a_1

pp: case refine_2
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ i < a + 1, upperCentralSeries G i ∈ upperCentralSeries G '' Set.Iic a

pp: case refine_3
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ (i j : ℕ), i < a + 1 → j < a + 1 → upperCentralSeries G i = upperCentralSeries G j → i = j

Tactic:
·

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ a_1 ∈ upperCentralSeries G '' Set.Iic a, ∃ i, ∃ (_ : i < a + 1), upperCentralSeries G i = a_1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ i < a + 1, upperCentralSeries G i ∈ upperCentralSeries G '' Set.Iic a

pp: case refine_3
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ (i j : ℕ), i < a + 1 → j < a + 1 → upperCentralSeries G i = upperCentralSeries G j → i = j

Tactic:
·

Goal state after:
case refine_2
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ i < a + 1, upperCentralSeries G i ∈ upperCentralSeries G '' Set.Iic a
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ (g, h) ∈
      ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ↔
    (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd

Tactic:
H',

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
G' : Subgroup G := map (MonoidHom.fst G H) I
H' : Subgroup H := map (MonoidHom.snd G H) I
P : ↥I →* ↥G' := (MonoidHom.fst G H).subgroupMap I
Q : ↥I →* ↥H' := (MonoidHom.snd G H).subgroupMap I
I' : Subgroup (↥G' × ↥H') := (P.prod Q).range
hI₁' : Surjective (Prod.fst ∘ ⇑I'.subtype)
hI₂' : Surjective (Prod.snd ∘ ⇑I'.subtype)
this✝ : I'.goursatFst.Normal
this : I'.goursatSnd.Normal
e : ↥G' ⧸ I'.goursatFst ≃* ↥H' ⧸ I'.goursatSnd
he :
  (((QuotientGroup.mk' I'.goursatFst).prodMap (QuotientGroup.mk' I'.goursatSnd)).comp I'.subtype).range =
    e.toMonoidHom.graph
g : ↥(map (MonoidHom.fst G H) I)
h : ↥(map (MonoidHom.snd G H) I)
⊢ (g, h) ∈
      ((QuotientGroup.mk' (P.prod Q).range.goursatFst).prodMap (QuotientGroup.mk' (P.prod Q).range.goursatSnd)).ker ↔
    (g, h) ∈ (P.prod Q).range.goursatFst.prod (P.prod Q).range.goursatSnd
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ (i j : ℕ), i < a + 1 → j < a + 1 → upperCentralSeries G i = upperCentralSeries G j → i = j

Tactic:
·

Goal state after:
case refine_3
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
⊢ ∀ (i j : ℕ), i < a + 1 → j < a + 1 → upperCentralSeries G i = upperCentralSeries G j → i = j
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: case mp
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive M α → IsPretransitive N β

pp: case mpr
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive N β → IsPretransitive M α

Tactic:
·

Goal state after:
case mp
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive M α → IsPretransitive N β
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: case mpr
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive N β → IsPretransitive M α

Tactic:
·

Goal state after:
case mpr
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
⊢ IsPretransitive N β → IsPretransitive M α
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: case mpr
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
g : M
hk : φ g • f x = f y
⊢ ∃ g, g • x = y

Tactic:
use g

Goal state after:
case h
M : Type u_3
N : Type u_4
α : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : MulAction M α
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hφ : Function.Surjective φ
hf : Function.Bijective ⇑f
hN : IsPretransitive N β
x y : α
g : M
hk : φ g • f x = f y
⊢ g • x = y
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hbase
⊢ ∀ (G : Type u_1) [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer ↑H = H → H = ⊤

pp: case hstep
⊢ ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
·

Goal state after:
case hbase
⊢ ∀ (G : Type u_1) [inst : Group G] [Subsingleton G] (H : Subgroup G), normalizer ↑H = H → H = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case hstep
⊢ ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤

Tactic:
·

Goal state after:
case hstep
⊢ ∀ (G : Type u_1) [inst : Group G] [IsNilpotent G],
    (∀ (H : Subgroup (G ⧸ center G)), normalizer ↑H = H → H = ⊤) → ∀ (H : Subgroup G), normalizer ↑H = H → H = ⊤
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃ x ∈ range fun x ↦ orbit G x, a ∈ x

pp: case h₃
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∅ ∉ range fun x ↦ orbit G x

Tactic:
·

Goal state after:
case h₂
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∀ (a : X), ∃ x ∈ range fun x ↦ orbit G x, a ∈ x
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case h₃
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∅ ∉ range fun x ↦ orbit G x

Tactic:
·

Goal state after:
case h₃
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
⊢ ∅ ∉ range fun x ↦ orbit G x
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f '' B)

pp: case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ IsTrivialBlock (⇑f '' B)

Tactic:
·

Goal state after:
case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f '' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ IsTrivialBlock (⇑f '' B)

Tactic:
·

Goal state after:
case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Surjective ⇑f
B : Set α
hB : B = univ
⊢ IsTrivialBlock (⇑f '' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f ⁻¹' B)

pp: case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = univ
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
·

Goal state after:
case inl
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B.Subsingleton
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = univ
⊢ IsTrivialBlock (⇑f ⁻¹' B)

Tactic:
·

Goal state after:
case inr
M : Type u_3
α : Type u_4
N : Type u_5
β : Type u_6
inst✝³ : Monoid M
inst✝² : MulAction M α
inst✝¹ : Monoid N
inst✝ : MulAction N β
φ : M → N
f : α →ₑ[φ] β
hf : Function.Injective ⇑f
B : Set β
hB : B = univ
⊢ IsTrivialBlock (⇑f ⁻¹' B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case mp
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B

pp: case mpr
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock B → IsTrivialBlock (g • B)

Tactic:
·

Goal state after:
case mp
M : Type u_3
α : Type u_4
inst✝¹ : Group M
inst✝ : MulAction M α
B : Set α
g : M
⊢ IsTrivialBlock (g • B) → IsTrivialBlock B