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

Goal state before:
pp: M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x y : DivisibleHull M
f : M → ℕ+ → M → ℕ+ → α
h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t'
p q p' q' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
heq' : q ≈ q'
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
obtain ⟨u, hu⟩ := heq'

Goal state after:
M : Type u_1
inst✝ : AddCommMonoid M
α : Type u_2
x y : DivisibleHull M
f : M → ℕ+ → M → ℕ+ → α
h : ∀ (m n m' n' : M) (s t s' t' : ℕ+), mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t'
p q p' q' : M × ↥(nonZeroDivisors ℕ)
heq : p ≈ p'
u : ↥(nonZeroDivisors ℕ)
hu : u • q'.2 • q.1 = u • q.2 • q'.1
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case zero
M : Type u_1
inst✝ : AddCommMonoid M
m : M
s : ℕ+
⊢ 0 • mk m s = mk (0 • m) s

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case zero
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
p : ℕ
i j : B
h : 0 < 2 * p
⊢ (cs.leftInvSeq (alternatingWord i j (2 * p)))[0] = cs.wordProd (alternatingWord j i (2 * 0 + 1))

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ⋃ q, Quot.mk ⇑(leftRel K) '' doubleCoset (out q) ↑H ↑K = Set.univ

Tactic:
rw [Set.iUnion_eq_univ_iff]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(leftRel K)), ∃ i, x ∈ Quot.mk ⇑(leftRel K) '' doubleCoset (out i) ↑H ↑K
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ⋃ q, Quot.mk ⇑(rightRel H) '' doubleCoset (out q) ↑H ↑K = Set.univ

Tactic:
rw [Set.iUnion_eq_univ_iff]

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
cover : ⋃ q, quotToDoubleCoset H K q = Set.univ
⊢ ∀ (x : Quot ⇑(rightRel H)), ∃ i, x ∈ Quot.mk ⇑(rightRel H) '' doubleCoset (out i) ↑H ↑K
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
⊢ (trivializationAt F E x).symm x ((Trivialization.linearMapAt ℝ (trivializationAt F E x) x) v) = v

Tactic:
convert! ((trivializationAt F E x).continuousLinearEquivAt ℝ _ h'x).symm_apply_apply v

Goal state after:
case e'_1
B : Type u_1
inst✝⁷ : TopologicalSpace B
F : Type u_2
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
E : B → Type u_3
inst✝⁴ : TopologicalSpace (TotalSpace F E)
inst✝³ : (x : B) → NormedAddCommGroup (E x)
inst✝² : (x : B) → InnerProductSpace ℝ (E x)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
h : IsContinuousRiemannianBundle F E
x : B
r : ℝ
hr : 1 < r
r' : ℝ
hr' : 1 < r'
r'r : r' < r
h'x : x ∈ (trivializationAt F E x).baseSet
G : E x ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x
C : ℝ := ‖↑G‖ ^ 2
δ : ℝ
δpos : 0 < δ
h'δ : 1 + δ * C < r' ^ 2
g : (x : B) → E x →L[ℝ] E x →L[ℝ] ℝ
g_cont :
  Continuous[inst✝⁷, topologicalSpaceTotalSpace (RingHom.id ℝ) F E (F →L[ℝ] ℝ) fun x ↦ E x →L[ℝ] ℝ] fun x ↦
    TotalSpace.mk' (F →L[ℝ] F →L[ℝ] ℝ) x (g x)
hg : ∀ (x : B) (v w : E x), ⟪v, w⟫ = ((g x) v) w
g' : B → F →L[ℝ] F →L[ℝ] ℝ := fun y ↦ inCoordinates F E (F →L[ℝ] ℝ) (fun x ↦ E x →L[ℝ] ℝ) x y x y (g y)
hg' : ContinuousAt g' x
this✝ : ∀ᶠ (y : B) in 𝓝 x, dist (g' y) (g' x) < δ
y : B
hy : dist (g' y) (g' x) < δ
h'y : y ∈ (trivializationAt F E x).baseSet
this : ‖g' y - g' x‖ ≤ δ
v : E x
w : F := (Trivialization.continuousLinearMapAt ℝ (trivializationAt F E x) x) v
⊢ ⇑(Trivialization.linearMapAt ℝ (trivializationAt F E x) x) =
    ⇑(Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E x) x h'x)
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relIndex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))

Tactic:
have h3 := Nat.mul_le_mul (Nat.le_of_dvd (Nat.pos_of_ne_zero hG) h1) (rank_commutator_le_card G)

Goal state after:
case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝ : (center G).FiniteIndex
h1 : (center G).relIndex (_root_.commutator G) ∣ (center G).index
this : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relIndex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
⊢ Nat.card ↥((center G).subgroupOf (_root_.commutator G)) ∣
    (center G).index ^ ((center G).index * Nat.card ↑(commutatorSet G))
Module: Mathlib.GroupTheory.Focal

Goal state before:
pp: case mem
G : Type u_1
inst✝ : Group G
H : Subgroup G
n g : G
hg : g ∈ H
z : G
hz : z ∈ {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
⊢ g * z * g⁻¹ ∈ H.focalSubgroup

Tactic:
obtain ⟨hzH, x, hxP, u, rfl⟩ := hz
    exact subset_closure ⟨by aesop, g * x * g⁻¹, by aesop, g * u * g⁻¹, by group⟩

Goal state after:
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ : G →* H
⊢ ∀ (ϕ : G ≃* G), comap ϕ.toMonoidHom (frattini G) = frattini G

Tactic:
intro φ

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
φ✝ : G →* H
φ : G ≃* G
⊢ comap φ.toMonoidHom (frattini G) = frattini G
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Characteristic
⊢ (S.lowerCentralSeries 0).Characteristic

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
⊢ map f (S.lowerCentralSeries 0) = (map f S).lowerCentralSeries 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: 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.18
inst✝ : Monoid X
f : End (root' T) →* X
⊢ ∀ (X_1 : G), f (loopOfHom T (𝟙 X_1)) = 𝟙 ()

Tactic:
intro a

Goal state after:
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.18
inst✝ : Monoid X
f : End (root' T) →* X
a : G
⊢ f (loopOfHom T (𝟙 a)) = 𝟙 ()
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ ⊤.lowerCentralSeries (nilpotencyClass G) = ⊥

Tactic:
classical
  rw [← lowerCentralSeries_length_eq_nilpotencyClass]
  exact Nat.find_spec (nilpotent_iff_lowerCentralSeries.mp hG)

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝ : Group G
⊢ Monotone fun S ↦ S.lowerCentralSeries 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
S : Subgroup G
inst✝ : S.Normal
⊢ (S.lowerCentralSeries 0).Normal

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_1
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'
x y : G
q : x ⟶ y
⊢ ∀ {a : WideSubquiver.toType (Symmetrify (Generators G)) T}
    (p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a), F'.map (homOfPath T p) = 1

Tactic:
intro a

Goal state after:
case refine_1
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'
x y : G
q : x ⟶ y
a : WideSubquiver.toType (Symmetrify (Generators G)) T
⊢ ∀ (p : Path (root (WideSubquiver.toType (Symmetrify (Generators G)) T)) a), F'.map (homOfPath T p) = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
f : G →* H
h : Function.Surjective ⇑f
⊢ Subgroup.map f (upperCentralSeries G 0) ≤ upperCentralSeries H 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝ : Group G
⊢ comap (mk' (center G)) (upperCentralSeries (G ⧸ center G) 0) = upperCentralSeries G (Nat.succ 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_2.e_5
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 := ⋯
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) (g : a ⟶ b), (functorOfMonoidHom T E).map (of g) = f' g

Tactic:
intro a

Goal state after:
case refine_2.e_5
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 : Generators G
⊢ ∀ (b : Generators G) (g : a ⟶ b), (functorOfMonoidHom T E).map (of g) = f' g
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
P : (G : Type u_2) → [inst : Group G] → [IsNilpotent G] → Prop
hbase : ∀ (G : Type u_2) [inst : Group G] [inst_1 : Subsingleton G], P G
hstep : ∀ (G : Type u_2) [inst : Group G] [inst_1 : IsNilpotent G], P (G ⧸ center G) → P G
G : Type u_2
inst✝¹ : Group G
inst✝ : IsNilpotent G
h : nilpotencyClass G = 0
⊢ P G

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝ : Group G
⊢ derivedSeries G 0 ≤ ⊤.lowerCentralSeries 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_2
inst✝ : CommGroup G
⊢ nilpotencyClass G ≤ 1

Tactic:
rw [← upperCentralSeries_eq_top_iff_nilpotencyClass_le, upperCentralSeries_one]
  apply CommGroup.center_eq_top

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case refine_2
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'
⊢ ∀ (y : End (root' T) →* X),
    (fun F ↦ ∀ (a : ↑(wideSubquiverEquivSetTotal (wideSubquiverSymmetrify T))ᶜ), F (loopOfHom T (of (↑a).hom)) = f a)
        y →
      y = Functor.mapEnd (root' T) F'

Tactic:
intro E hE
        ext x
        suffices (functorOfMonoidHom T E).map x = F'.map x by
          simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root,
            Category.id_comp, Category.comp_id] using! this
        congr
        apply uF'
        intro a b e
        change E (loopOfHom T _) = dite _ _ _
        split_ifs with h
        · rw [loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
        · exact hE ⟨⟨a, b, e⟩, h⟩

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G₁ : Type u_2
G₂ : Type u_3
inst✝¹ : Group G₁
inst✝ : Group G₂
S₁ : Subgroup G₁
S₂ : Subgroup G₂
⊢ (S₁.prod S₂).lowerCentralSeries 0 = (S₁.lowerCentralSeries 0).prod (S₂.lowerCentralSeries 0)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
Ss : (i : η) → Subgroup (Gs i)
⊢ (pi Set.univ Ss).lowerCentralSeries 0 ≤ pi Set.univ fun i ↦ (Ss i).lowerCentralSeries 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
η : Type u_2
Gs : η → Type u_3
inst✝¹ : (i : η) → Group (Gs i)
inst✝ : Finite η
Ss : (i : η) → Subgroup (Gs i)
⊢ (pi Set.univ Ss).lowerCentralSeries 0 = pi Set.univ fun i ↦ (Ss i).lowerCentralSeries 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝ : SMul G X
B : Set X
hfB : IsFixedBlock G B
⊢ IsBlock G B

Tactic:
simp [IsBlock, hfB _]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : g₁ • B ≠ g₂ • B
⊢ Disjoint (g₁ • B) (g₂ • B)

Tactic:
simp only [disjoint_smul_set_right, ne_eq, ← inv_smul_eq_iff, smul_smul] at h ⊢

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hB : ∀ ⦃g : G⦄, g • B ≠ B → Disjoint (g • B) B
g₁ g₂ : G
h : ¬(g₂⁻¹ * g₁) • B = B
⊢ Disjoint ((g₂⁻¹ * g₁) • B) B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B₁ B₂ : Set X
h₁ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₁ ∩ g₂ • B₁).Nonempty → g₁ • B₁ = g₂ • B₁
h₂ : ∀ ⦃g₁ g₂ : G⦄, (g₁ • B₂ ∩ g₂ • B₂).Nonempty → g₁ • B₂ = g₂ • B₂
g₁ g₂ : G
a : X
ha₁ : a ∈ g₁ • B₁ ∩ g₁ • B₂
ha₂ : a ∈ g₂ • B₁ ∩ g₂ • B₂
⊢ g₁ • B₁ ∩ g₁ • B₂ = g₂ • B₁ ∩ g₂ • B₂

Tactic:
rw [h₁ ⟨a, ha₁.1, ha₂.1⟩, h₂ ⟨a, ha₁.2, ha₂.2⟩]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ ↑h' • g • B = g • h • B

Tactic:
← hh,

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
h' : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)
h : G
hH : h ∈ H
hh : g * h * g⁻¹ = ↑h'
⊢ (g * h * g⁻¹) • g • B = g • h • B
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
⊢ ∀ (a : X), ∃! b, (b ∈ range fun g ↦ g • B) ∧ a ∈ b

Tactic:
intro a

Goal state after:
case cover
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
hGX : IsPretransitive G X
hB : IsBlock G B
hBe : B.Nonempty
a : X
⊢ ∃! b, (b ∈ range fun g ↦ g • B) ∧ a ∈ b
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B✝ : Set X
htGX : IsPretransitive G X
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
B' : Set X
ha' : a ∈ B'
hB' : IsBlock G B'
hBB' : ⟨stabilizer G B, ⋯⟩ ≤ ⟨stabilizer G B', ⋯⟩
k : G
hb : k • a ∈ B
this : k ∈ stabilizer G B'
⊢ k • a ∈ B'

Tactic:
exact this.symm ▸ (Set.smul_mem_smul_set ha')

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mpr
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ ⟨B, ⋯⟩ = ⊥ ∨ ⟨B, ⋯⟩ = ⊤

Tactic:
simp only [← Subtype.coe_inj]

Goal state after:
case mpr
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
hGX' : IsPreprimitive G X
B : Set X
haB : a ∈ B
hB : IsBlock G B
⊢ B = ↑⊥ ∨ B = ↑⊤
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
⊢ IsCyclic ↥(alternatingGroup α)

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
h✝ : Subsingleton α
⊢ IsCyclic ↥(alternatingGroup α)

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
h✝ : Nontrivial α
⊢ IsCyclic ↥(alternatingGroup α)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case zero
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
hn : l.length = 2 * 0
⊢ l.prod ∈ closure {σ | σ.IsThreeCycle}

Tactic:
| zero =>

Goal state after:
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
⊢ ∀ (x : α), x ∉ g.support

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα4 : 4 ≤ Nat.card α
g : Perm α
hg : g ∈ alternatingGroup α
hg' : ⟨g, hg⟩ ∈ center ↥(alternatingGroup α)
a : α
⊢ a ∉ g.support
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : IsMulCommutative ↥(alternatingGroup α)
h : 3 < Nat.card α
this : Subsingleton ↥(alternatingGroup α)
⊢ False

Tactic:
← not_nontrivial_iff_subsingleton

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
H : IsMulCommutative ↥(alternatingGroup α)
h : 3 < Nat.card α
this : ¬Nontrivial ↥(alternatingGroup α)
⊢ False
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : ∀ (x_1 : n), (g • aux x) x_1 = (aux y) x_1
i : n
⊢ (σ g • x) i = y i

Tactic:
rw [smul_apply]

Goal state after:
case h
G : Type u_1
α : Type u_2
inst✝⁴ : Group G
inst✝³ : MulAction G α
H : Type u_3
β : Type u_4
inst✝² : Group H
inst✝¹ : MulAction H β
σ : G → H
f : α →ₑ[σ] β
n : Type u_5
hf : Function.Surjective ⇑f
inst✝ : IsPretransitive G (n ↪ α)
x y : n ↪ β
aux : (n ↪ β) → n ↪ α := fun x ↦ x.trans (Function.Embedding.ofSurjective (⇑f) hf)
aux_apply : ∀ (x : n ↪ β) (i : n), f.toFun ((aux x) i) = x i
g : G
hg : ∀ (x_1 : n), (g • aux x) x_1 = (aux y) x_1
i : n
⊢ σ g • x i = y i
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
a✝ : IsMultiplyPretransitive G α 2
a b c d : α
h : a ≠ b
h' : c ≠ d
m : G
e : m • embFinTwo h = embFinTwo h'
⊢ m • a = c

Tactic:
rw [← embFinTwo_apply_zero h, ← smul_apply, e, embFinTwo_apply_zero]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
⊢ g ∈ fixingSubgroup G s

Tactic:
intro a

Goal state after:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
this : IsMultiplyPretransitive G α (s.ncard + m)
Hs : Nonempty (Fin s.ncard ≃ ↑s)
x' : Fin (s.ncard + m) ↪ α := append x
hx : x' = append x
y' : Fin (s.ncard + m) ↪ α := append y
hy : y' = append y
g : G
hg : g • x' = y'
a : ↑s
⊢ g • ↑a = ↑a