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

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦
      if i = j then 1
      else
        if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3
        else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).IsSymm

Tactic:
unfold Matrix.IsSymm

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n : ℕ
⊢ (Matrix.of fun i j ↦
        if i = j then 1
        else
          if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3
          else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2).transpose =
    Matrix.of fun i j ↦
      if i = j then 1
      else if ↑i = n - 1 ∧ ↑j = n - 3 ∨ ↑j = n - 1 ∧ ↑i = n - 3 then 3 else if ↑j + 1 = ↑i ∨ ↑i + 1 = ↑j then 3 else 2
Module: Mathlib.GroupTheory.Coxeter.Matrix

Goal state before:
pp: B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ (Matrix.of fun i j ↦ if i = j then 1 else m + 2).IsSymm

Tactic:
unfold Matrix.IsSymm

Goal state after:
B : Type u_1
B' : Type u_2
e : B ≃ B'
M : CoxeterMatrix B
n m : ℕ
⊢ (Matrix.of fun i j ↦ if i = j then 1 else m + 2).transpose = Matrix.of fun i j ↦ if i = j then 1 else m + 2
Module: Mathlib.GroupTheory.Coxeter.Length

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i i' : B
m : ℕ
hM : M.M i i' ≠ 0
h : cs.length (cs.wordProd (alternatingWord i i' (M.M i i' + 1))) < M.M i i' + 1
⊢ ¬cs.IsReduced (alternatingWord i i' (M.M i i').succ)

Tactic:
unfold IsReduced
      rw [Nat.succ_eq_add_one, length_alternatingWord]
      lia

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

Goal state before:
pp: B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
i : B
⊢ cs.rightInvSeq (ω.concat i) = (List.map (⇑(MulAut.conj (cs.simple i))) (cs.rightInvSeq ω)).concat (cs.simple i)

Tactic:
induction ω with
  | nil => simp
  | cons j ω ih =>
    dsimp [rightInvSeq, concat]
    rw [ih]
    simp only [concat_eq_append, wordProd_append, wordProd_cons, wordProd_nil, mul_one, mul_inv_rev,
      inv_simple, map_cons, MulAut.conj_apply, cons_append, cons.injEq, and_true]
    group

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
w_ih_w₁ : ∀ (x : M i✝) (hnotone : x * _w₁✝.head ≠ 1), (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
w_ih_w₂ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (replaceHead (x * _w₂✝.head) hnotone _w₂✝).prod = of x * _w₂✝.prod
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod

Tactic:
specialize w_ih_w₁ _ hnotone

Goal state after:
case append
ι : Type u_1
M : ι → Type u_2
inst✝ : (i : ι) → Monoid (M i)
i j i✝ j✝ k✝ l✝ : ι
_w₁✝ : NeWord M i✝ j✝
_hne✝ : j✝ ≠ k✝
_w₂✝ : NeWord M k✝ l✝
w_ih_w₂ : ∀ (x : M k✝) (hnotone : x * _w₂✝.head ≠ 1), (replaceHead (x * _w₂✝.head) hnotone _w₂✝).prod = of x * _w₂✝.prod
x : M i✝
hnotone : x * (_w₁✝.append _hne✝ _w₂✝).head ≠ 1
w_ih_w₁ : (replaceHead (x * _w₁✝.head) hnotone _w₁✝).prod = of x * _w₁✝.prod
⊢ (replaceHead (x * (_w₁✝.append _hne✝ _w₂✝).head) hnotone (_w₁✝.append _hne✝ _w₂✝)).prod =
    of x * (_w₁✝.append _hne✝ _w₂✝).prod
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
m n : M
h : mk m s = mk n s
⊢ m = n

Tactic:
mk_eq_mk_iff_smul_eq_smul

Goal state after:
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : IsAddTorsionFree M
s : ℕ+
m n : M
h : ↑s • m = ↑s • n
⊢ m = n
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : mk m s = mk m' s'
h' : mk n t = mk n' t'
⊢ (↑t • m ≤ ↑s • n) = (↑t' • m' ≤ ↑s' • n')

Tactic:
mk_eq_mk_iff_smul_eq_smul

Goal state after:
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
m n m' n' : M
s t s' t' : ℕ+
h : ↑s' • m = ↑s • m'
h' : ↑t' • n = ↑t • n'
⊢ (↑t • m ≤ ↑s • n) = (↑t' • m' ≤ ↑s' • n')
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case pos
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : i ≠ j
⊢ (lift f) w.prod ≠ 1

Tactic:
have : lift f w.inv.prod ≠ 1 :=
        lift_word_prod_nontrivial_of_head_card f X hXnonempty hXdisj hpp w.inv hcard hh.symm

Goal state after:
case pos
ι : Type u_1
G : Type u_4
inst✝³ : Group G
H : ι → Type u_5
inst✝² : (i : ι) → Group (H i)
f : (i : ι) → H i →* G
α : Type u_6
inst✝¹ : MulAction G α
X : ι → Set α
hXnonempty : ∀ (i : ι), (X i).Nonempty
hXdisj : Pairwise (Disjoint on X)
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
inst✝ : Nontrivial ι
i j : ι
w : NeWord H i j
hcard : 3 ≤ #(H j)
hh : i ≠ j
this : (lift f) w.inv.prod ≠ 1
⊢ (lift f) w.prod ≠ 1
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : ↑sb • ma ≤ ↑sa • mb
h' : ↑sa • mb ≤ ↑sb • ma
⊢ mk ma sa = mk mb sb

Tactic:
mk_eq_mk_iff_smul_eq_smul

Goal state after:
case mk.mk
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
ma : M
sa : ℕ+
mb : M
sb : ℕ+
h : ↑sb • ma ≤ ↑sa • mb
h' : ↑sa • mb ≤ ↑sb • ma
⊢ ↑sb • ma = ↑sa • mb
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < c • a - b • a

Tactic:
← sub_smul

Goal state after:
M✝ : Type u_1
inst✝³ : AddCommMonoid M✝
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a : DivisibleHull M
ha : 0 < a
b c : ℚ
h : b < c
⊢ 0 < (c - b) • a
Module: Mathlib.GroupTheory.FiniteAbelian.Duality

Goal state before:
pp: G : Type u_1
M : Type u_2
inst✝² : CommGroup G
inst✝¹ : Finite G
inst✝ : CommMonoid M
hM : HasEnoughRootsOfUnity M (Monoid.exponent G)
H : Subgroup G
this✝¹ : Fintype ↥H
this✝ : HasEnoughRootsOfUnity M (Monoid.exponent ↥H)
this : HasEnoughRootsOfUnity M (Monoid.exponent (G ⧸ H))
⊢ Nat.card ↥(domRestrictHom H Mˣ).ker = Nat.card (G →* Mˣ) / Nat.card (↥H →* Mˣ)

Tactic:
rw [card_monoidHom_of_hasEnoughRootsOfUnity, card_monoidHom_of_hasEnoughRootsOfUnity,
    H.card_eq_card_quotient_mul_card_subgroup,
    mul_div_cancel_right₀ _ (Fintype.card_eq_nat_card ▸ Fintype.card_ne_zero),
    ← card_monoidHom_of_hasEnoughRootsOfUnity (G ⧸ H) M,
    Nat.card_congr (domRestrictHomKerEquiv Mˣ H).toEquiv]

Goal state after:
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR : IsComplement (↑H) R₀
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
⊢ ∃ T, #T ≤ H.index * #S ∧ closure ↑T = ⊤

Tactic:
replace hR : IsComplement (H : Set G) R := by rwa [Set.coe_toFinset]

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.FiniteIndex
S : Finset G
hS : closure ↑S = ⊤
this✝¹ : Fintype (G ⧸ H) := fintypeQuotientOfFiniteIndex
this✝ : DecidableEq G
R₀ : Set G
hR1 : 1 ∈ R₀
this : Fintype ↑R₀
R : Finset G := R₀.toFinset
hR : IsComplement ↑H ↑R
⊢ ∃ T, #T ≤ H.index * #S ∧ closure ↑T = ⊤
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : Sum.inr e ∈ T b a
⊢ treeHom T
        (have this := a;
        this) ≫
      of e =
    treeHom T b

Tactic:
rw [treeHom_eq T (Path.cons default ⟨Sum.inr e, H⟩), homOfPath]

Goal state after:
case inr
G : Type u
inst✝² : Groupoid G
inst✝¹ : IsFreeGroupoid G
T : WideSubquiver (Symmetrify (Generators G))
inst✝ : Arborescence (WideSubquiver.toType (Symmetrify (Generators G)) T)
a b : Generators G
e : a ⟶ b
H : Sum.inr e ∈ T b a
⊢ (homOfPath T default ≫ Sum.recOn (↑⟨Sum.inr e, H⟩) (fun e ↦ of e) fun e ↦ inv (of e)) ≫ of e = treeHom T b
Module: Mathlib.GroupTheory.Generators

Goal state before:
pp: G : Type u_1
H : Type u_2
ι : Type u_3
ι' : Type u_4
inst✝¹ : Group G
inst✝ : Group H
P : Generators G ι
S : Set G
h : Subgroup.closure S = ⊤
⊢ Subgroup.closure (Set.range Subtype.val) = ⊤

Tactic:
rwa [Subtype.range_coe]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
h : IsNilpotent G
⊢ nilpotencyClass G' ≤ nilpotencyClass G

Tactic:
have := nilpotent_of_surjective _ hf
  rw [nilpotencyClass_def, nilpotencyClass_def]
  classical apply Nat.find_mono
  intro n hn
  rw [eq_top_iff]
  calc
    ⊤ = f.range := symm (f.range_eq_top_of_surjective hf)
    _ = Subgroup.map f ⊤ := MonoidHom.range_eq_map _
    _ = Subgroup.map f (upperCentralSeries G n) := by rw [hn]
    _ ≤ upperCentralSeries G' n := upperCentralSeries.map hf n

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
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)
this : (functorOfMonoidHom T E).map x = F'.map x
⊢ E x = (Functor.mapEnd (root' T) F') x

Tactic:
by
          simpa only [loopOfHom, functorOfMonoidHom, IsIso.inv_id, treeHom_root,
            Category.id_comp, Category.comp_id] using! this

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case zero
G : Type u_1
inst✝¹ : Group G
hH : IsNilpotent G
inst✝ : Nontrivial G
h : nilpotencyClass G = 0
⊢ 0 = 0 - 1 + 1

Tactic:
exfalso
    rw [nilpotencyClass_zero_iff_subsingleton] at h
    apply false_of_nontrivial_of_subsingleton G

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

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

Tactic:
| inr h =>

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

Goal state before:
pp: M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
⊢ commutator M ≤ N

Tactic:
obtain a : α := Nontrivial.to_nonempty.some

Goal state after:
M : Type u_1
inst✝² : Group M
α : Type u_2
inst✝¹ : MulAction M α
IwaS : IwasawaStructure M α
inst✝ : IsQuasiPreprimitive M α
N : Subgroup M
nN : N.Normal
hNX : fixedPoints (↥N) α ≠ Set.univ
is_transN : IsPretransitive (↥N) α
ntα : Nontrivial α
a : α
⊢ commutator M ≤ N
Module: Mathlib.GroupTheory.GroupAction.Iwasawa

Goal state before:
pp: case inr
M : Type u_1
inst✝³ : Group M
α : Type u_2
inst✝² : MulAction M α
inst✝¹ : Nontrivial M
is_perfect : commutator M = ⊤
inst✝ : IsQuasiPreprimitive M α
IwaS : IwasawaStructure M α
is_faithful : FaithfulSMul M α
N : Subgroup M
nN : N.Normal
h : commutator M ≤ N
⊢ N = ⊥ ∨ N = ⊤

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
hH : H.index = 1
⊢ H.Normal

Tactic:
rw [index_eq_one] at hH
  rw [hH]
  infer_instance

Goal state after:
Module: Mathlib.GroupTheory.IndexNormal

Goal state before:
pp: case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
hHp : H.index = (Nat.card G).minFac
hG0 : ¬Nat.card G = 0
hG1 : Nat.card G = 1
⊢ H.Normal

Tactic:
rw [hG1, minFac_one] at hHp
    exact normal_of_index_eq_one hHp

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

Goal state before:
pp: case inr
G : Type u_1
inst✝³ : Group G
X : Type u_2
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
B : Set X
inst✝ : Finite X
hB : IsBlock G B
hB' : Nat.card X < 2 * (orbit G B).ncard
h : B.Nonempty
⊢ B.ncard < 2

Tactic:
| inr h =>

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

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
Hnt : ∃ a, a ∉ fixedPoints G X
⊢ IsPreprimitive G X

Tactic:
obtain ⟨_, ha⟩ := Hnt

Goal state after:
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
H : ∀ {B : Set X}, IsBlock G B → IsTrivialBlock B
w✝ : X
ha : w✝ ∉ fixedPoints G X
⊢ IsPreprimitive G X
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: case mpr.inr
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
h : B = Set.univ
⊢ B = ↑⊥ ∨ B = ↑⊤

Tactic:
| inr h =>

Goal state after:
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✝
B : Type u_4
inst✝¹⁰ : TopologicalSpace B
F : Type u_5
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace ℝ F
E : B → Type u_6
inst✝⁷ : TopologicalSpace (TotalSpace F E)
inst✝⁶ : (b : B) → TopologicalSpace (E b)
inst✝⁵ : (b : B) → AddCommGroup (E b)
inst✝⁴ : (b : B) → Module ℝ (E b)
inst✝³ : ∀ (b : B), IsTopologicalAddGroup (E b)
inst✝² : ∀ (b : B), ContinuousConstSMul ℝ (E b)
inst✝¹ : FiberBundle F E
inst✝ : VectorBundle ℝ F E
g : ContinuousRiemannianMetric F E
b : B
e : E b ≃L[ℝ] F := Trivialization.continuousLinearEquivAt ℝ (trivializationAt F E b) b ⋯
m : (E b →L[ℝ] E b →L[ℝ] ℝ) ≃L[ℝ] F →L[ℝ] F →L[ℝ] ℝ := e.arrowCongr (e.arrowCongr (ContinuousLinearEquiv.refl ℝ ℝ))
A : ∀ (v : E b), ((g.inner b) v) v = ((fun w ↦ ((m (g.inner b)) w) w) ∘ ⇑e) v
⊢ ContinuousAt (fun v ↦ ((fun w ↦ ((m (g.inner b)) w) w) ∘ ⇑e) v) 0

Tactic:
fun_prop

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

Goal state before:
pp: case mp
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsMultiplyPreprimitive M α 1 → IsPreprimitive M α

pp: case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α → IsMultiplyPreprimitive M α 1

Tactic:
· intro H1
    rw [← isPreprimitive_of_fixingSubgroup_empty_iff]
    apply H1.isPreprimitive_ofFixingSubgroup (by simp)

Goal state after:
case mpr
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
⊢ IsPreprimitive M α → IsMultiplyPreprimitive M α 1
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : Nat.card α ≤ 2
⊢ IsTrivialBlock B

Tactic:
exact isTrivialBlock_of_card_le_two h2 B

Goal state after:
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr.inr.inr
α : Type u_2
inst✝ : DecidableEq α
s : Set α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
this : ∀ (t : Set α), 1 < t.encard → ∃ g, g.IsSwap ∧ g ∈ stabilizer (Perm α) t
h1' : s.encard ≤ 1
h1c' : sᶜ.encard ≤ 1
hα✝ : univ.encard = 2
x✝ : Finite α
hα : Nat.card α = 2
hα2 : Fact (Nat.Prime (Nat.card (Perm α)))
h : G = ⊤
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
x✝ : IsMultiplyPretransitive (Perm α) α (s.ncard + 1)
⊢ sᶜ ⊆ B

Tactic:
apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le

Goal state after:
case hBs
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
x✝ : IsMultiplyPretransitive (Perm α) α (s.ncard + 1)
⊢ ¬B ⊆ s

case hBsc
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
x✝ : IsMultiplyPretransitive (Perm α) α (s.ncard + 1)
⊢ ¬B ⊆ sᶜ

case hB
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝ : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
not_isBlock_sc : ¬IsBlock (↥G) sᶜ
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hB_not_le_s : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ s → B.Subsingleton
x✝ : IsMultiplyPretransitive (Perm α) α (s.ncard + 1)
⊢ IsBlock (↥G) B
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: α : Type u_2
inst✝² : DecidableEq α
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
⊢ AddAction.toPerm g = 1 ↔ AddAction.toPerm g = 1

Tactic:
by
  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
  · contrapose h with h
    have : ∃ a, (g +ᵥ a : α) ≠ a := by simpa [Equiv.ext_iff] using h
    obtain ⟨a, ha⟩ := this
    obtain ⟨s, has, has'⟩ := exists_mem_notMem hn hα (Ne.symm ha)
    rw [Equiv.ext_iff, not_forall]
    use s
    contrapose has'
    simp only [AddAction.toPerm_apply, coe_one, id_eq] at has'
    rw [← has']
    simpa [← mem_coe_iff]
  · simp only [Equiv.ext_iff, AddAction.toPerm_apply] at h ⊢
    simp [Subtype.ext_iff, Finset.ext_iff, mem_vadd_finset, h]

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

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ Fintype.card ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ) = 2

Tactic:
Fintype.card_subtype,

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : DecidableEq α
inst✝ : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this✝ : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support)ᶜ.ncard = n + 1
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ {x | x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ}.card = 2
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ Fintype.card ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ) = 3

Tactic:
Fintype.card_subtype,

Goal state after:
α : Type u_1
G : Subgroup (Perm α)
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this : IsPretransitive ↥(fixingSubgroup (↥G) (↑g.support)ᶜ) ↥(ofFixingSubgroup (↥G) (↑g.support)ᶜ)
⊢ {x | x ∈ ofFixingSubgroup (↥G) (↑g.support)ᶜ}.card = 3
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
j : ℤ
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ (g ^ (j + m)) (a c) = (g ^ j) x

Tactic:
rw [zpow_add, mul_apply, hm]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset
this : sign c = 1
⊢ c.IsCycle

Tactic:
· rw [mem_cycleFactorsFinset_iff] at hc
      exact hc.left

Goal state after:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case H.inr
ι : Type u_1
G : ι → Type u_2
H : Type u_3
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
motive : (con φ).Quotient → Prop
of : ∀ (i : ι) (g : G i), motive (((con φ).mk'.comp (inl.comp CoprodI.of)) g)
base : ∀ (h : H), motive (((con φ).mk'.comp inr) h)
mul : ∀ (x y : (con φ).Quotient), motive x → motive y → motive (x * y)
h : H
⊢ motive ↑(inr h)

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.GroupTheory.Perm.Centralizer

Goal state before:
pp: case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : ↥g.cycleFactorsFinset
⊢ _root_.Disjoint ((fun i ↦ ((fun c ↦ zpowers ↑c) i).subtype.range) a)
    (⨆ j, ⨆ (_ : j ≠ a), (fun i ↦ ((fun c ↦ zpowers ↑c) i).subtype.range) j)

Tactic:
simp only [range_subtype, ne_eq]

Goal state after:
case refine_1.hind
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : ↥g.cycleFactorsFinset
⊢ _root_.Disjoint (zpowers ↑a) (⨆ j, ⨆ (_ : ¬j = a), zpowers ↑j)