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

Goal state before:
pp: case pos
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
h : j = k
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := ⋯ ▸ g, tail := tail, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

pp: case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
h : ¬j = k
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := 1, tail := cons g tail h1 h2, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩

Tactic:
· subst k
      by_cases hij : j = i <;> simp_all

Goal state after:
case neg
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m : M i
k : ι
g : M k
tail : Word M
h1 : tail.fstIdx ≠ some k
h2 : g ≠ 1
ih :
  ⟨i, m⟩ ∈
      (↑(consRecOn tail ⟨{ head := 1, tail := empty, fstIdx_ne := ⋯ }, ⋯⟩ fun j_1 m w h1 h2 x ↦
              if ij : j = j_1 then ⟨{ head := ⋯ ▸ m, tail := w, fstIdx_ne := ⋯ }, ⋯⟩
              else ⟨{ head := 1, tail := cons m w h1 h2, fstIdx_ne := ⋯ }, ⋯⟩)).tail.toList ↔
    ⟨i, m⟩ ∈ tail.toList.tail ∨ ¬i = j ∧ ∃ (h : ¬tail.toList = []), tail.toList.head h = ⟨i, m⟩
h : ¬j = k
⊢ ⟨i, m⟩ ∈ (↑⟨{ head := 1, tail := cons g tail h1 h2, fstIdx_ne := ⋯ }, ⋯⟩).tail.toList ↔
    ⟨i, m⟩ ∈ (cons g tail h1 h2).toList.tail ∨
      ¬i = j ∧ ∃ (h : ¬(cons g tail h1 h2).toList = []), (cons g tail h1 h2).toList.head h = ⟨i, m⟩
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
w : Word M
⊢ (⟨i, m₁⟩ ∈
        (have __src := (equivPair j) w;
            { head := m₂ * ((equivPair j) w).head, tail := __src.tail, fstIdx_ne := ⋯ }).tail.toList ∨
      m₁ ≠ 1 ∧
        ∃ (h : j = i),
          m₁ =
            h ▸
              (have __src := (equivPair j) w;
                { head := m₂ * ((equivPair j) w).head, tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

Tactic:
mem_equivPair_tail_iff,

Goal state after:
ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
w : Word M
⊢ ((⟨i, m₁⟩ ∈ w.toList.tail ∨ i ≠ j ∧ ∃ (h : w.toList ≠ []), w.toList.head h = ⟨i, m₁⟩) ∨
      m₁ ≠ 1 ∧
        ∃ (h : j = i),
          m₁ =
            h ▸
              (have __src := (equivPair j) w;
                { head := m₂ * ((equivPair j) w).head, tail := __src.tail, fstIdx_ne := ⋯ }).head) ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: ι : Type u_1
M : ι → Type u_2
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i j : ι
m₁ : M i
m₂ : M j
w : Word M
⊢ ⟨i, m₁⟩ ∈ (of m₂ • w).toList ↔
    ¬i = j ∧ ⟨i, m₁⟩ ∈ w.toList ∨
      m₁ ≠ 1 ∧
        ∃ (hij : i = j),
          ⟨i, m₁⟩ ∈ w.toList.tail ∨
            (∃ m', ⟨j, m'⟩ ∈ w.toList.head? ∧ m₁ = ⋯ ▸ (m₂ * m')) ∨ w.fstIdx ≠ some j ∧ m₁ = ⋯ ▸ m₂

Tactic:
by
  rw [of_smul_def, mem_rcons_iff, mem_equivPair_tail_iff, equivPair_head, or_assoc]
  by_cases hij : i = j
  · subst i
    simp only [not_true, ne_eq, false_and, exists_prop, true_and, false_or]
    by_cases hw : ⟨j, m₁⟩ ∈ w.toList.tail
    · simp [hw, show m₁ ≠ 1 from w.ne_one _ (List.mem_of_mem_tail hw)]
    · simp only [hw, false_or, Option.mem_def, and_congr_right_iff]
      intro hm1
      split_ifs with h
      · rcases h with ⟨hnil, rfl⟩
        simp only [List.head?_eq_some_head hnil, Option.some.injEq]
        constructor
        · rintro rfl
          exact Or.inl ⟨_, rfl, rfl⟩
        · rintro (⟨_, h, rfl⟩ | hm')
          · simp only [Sigma.ext_iff, heq_eq_eq, true_and] at h
            subst h
            rfl
          · simp only [fstIdx, Option.map_eq_some_iff, Sigma.exists,
              exists_and_right, exists_eq_right, not_exists] at hm'
            exact (hm'.1 (w.toList.head hnil).2 (by rw [List.head?_eq_some_head])).elim
      · revert h
        rw [fstIdx]
        cases w.toList
        · simp
        · simp +contextual [Sigma.ext_iff]
  · rcases w with ⟨_ | _, _, _⟩ <;>
    simp [or_comm, hij, Ne.symm hij, eq_comm]

Goal state after:
Module: Mathlib.GroupTheory.CoprodI

Goal state before:
pp: case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
⊢ ∀ (m : M i) (w : Word M), w.prod • empty = w → (of m • w).prod • empty = of m • w

Tactic:
m

Goal state after:
case smul
ι : Type u_1
M : ι → Type u_2
inst✝³ : (i : ι) → Monoid (M i)
N : Type u_3
inst✝² : Monoid N
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (M i)
i : ι
m : M i
⊢ ∀ (w : Word M), w.prod • empty = w → (of m • w).prod • empty = of m • w
Module: Mathlib.GroupTheory.Coxeter.Inversion

Goal state before:
pp: case cons.head
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)

Tactic:
use (π ω)⁻¹, i

Goal state after:
case h
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
i : B
ω : List B
ih :
  (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω ∈ cs.rightInvSeq ω →
    cs.IsReflection ((cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω)
⊢ (cs.wordProd ω)⁻¹ * cs.simple i * cs.wordProd ω = (cs.wordProd ω)⁻¹ * cs.simple i * (cs.wordProd ω)⁻¹⁻¹
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
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
⊢ False

Tactic:
set! t := (ris ω).getD j 1 with h₁

Goal state after:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
j j' : ℕ
j_lt_j' : j < j'
j'_lt_length : j' < ω.length
dup : (cs.rightInvSeq ω).getD j 1 = (cs.rightInvSeq ω).getD j' 1
t : W := (cs.rightInvSeq ω).getD j 1
h₁ : t = (cs.rightInvSeq ω).getD j 1
⊢ False
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: α : Type u_2
inst✝ : Mul α
a : α
s t : Set α
⊢ doubleCoset a s t = Set.image2 (fun x1 x2 ↦ x1 * a * x2) s t

Tactic:
simp_rw [doubleCoset, Set.mul_singleton, ← Set.image2_mul, Set.image2_image_left]

Goal state after:
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
⊢ mk H K a = mk H K b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k

Tactic:
eq''

Goal state after:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
⊢ (setoid ↑H ↑K) a b ↔ ∃ h ∈ H, ∃ k ∈ K, b = h * a * k
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
φ : G →* Mˣ
⊢ φ ∈ OrderDual.ofDual ((subgroupOrderIsoSubgroupMonoidHom G M) H) ↔ ∀ g ∈ H, φ g = 1

Tactic:
by
  simp [subgroupOrderIsoSubgroupMonoidHom]

Goal state after:
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf : Function.Bijective ⇑((transferSylow P hP).domRestrict ↑P)
⊢ (transferSylow P hP).ker.IsComplement' ↑P

Tactic:
Function.Bijective,

Goal state after:
G : Type u_1
inst✝³ : Group G
p : ℕ
P : Sylow p G
hP : normalizer ↑P ≤ centralizer ↑P
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Finite (Sylow p G)
inst✝ : (↑P).FiniteIndex
hf :
  Function.Injective ⇑((transferSylow P hP).domRestrict ↑P) ∧ Function.Surjective ⇑((transferSylow P hP).domRestrict ↑P)
⊢ (transferSylow P hP).ker.IsComplement' ↑P
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x y : G
hx : ⁅x, y⁻¹⁆ ∈ N
⊢ ⁅x⁻¹, y⁆ ∈ N

Tactic:
rw [commutatorElement_def, mul_assoc, inv_inv] at hx ⊢

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x y : G
hx : x * y⁻¹ * (x⁻¹ * y) ∈ N
⊢ x⁻¹ * y * (x * y⁻¹) ∈ N
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case succ
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
d : ℕ
hd : map f (S.lowerCentralSeries d) = (map f S).lowerCentralSeries d
⊢ map f ⁅S.lowerCentralSeries d, S⁆ = ⁅(map f S).lowerCentralSeries d, map f S⁆

Tactic:
Subgroup.map_commutator,

Goal state after:
case succ
G : Type u_1
inst✝¹ : Group G
S : Subgroup G
K : Type u_2
inst✝ : Group K
f : G →* K
d : ℕ
hd : map f (S.lowerCentralSeries d) = (map f S).lowerCentralSeries d
⊢ ⁅map f (S.lowerCentralSeries d), map f S⁆ = ⁅(map f S).lowerCentralSeries d, map f S⁆
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
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ map f ⊤ = map f (upperCentralSeries G n)

Tactic:
rw [hn]

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
this : IsNilpotent G'
n : ℕ
hn : upperCentralSeries G n = ⊤
⊢ map f ⊤ = map f (upperCentralSeries G n)

Tactic:
rw [hn]

Goal state after:
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:
rw [hn]

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 b
Module: Mathlib.GroupTheory.GroupAction.Transitive

Goal state before:
pp: 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 : α →ₑ[φ] β
hf : Function.Surjective ⇑f
h : IsPretransitive M α
x' : α
g : M
⊢ ∃ g_1, g_1 • f x' = f (g • x')

Tactic:
exact ⟨φ g, by simp only [map_smulₛₗ]⟩

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

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
⊢ ∀ ⦃g₁ g₂ : G⦄, g₁ • ↑s ≠ g₂ • ↑s → ∀ ⦃a : H⦄, a ∈ g₁ • ↑s → a ∉ g₂ • ↑s

Tactic:
rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩

Goal state after:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G H H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
⊢ ∀ ⦃g₁ g₂ : G⦄, g₁ • ↑s ≠ g₂ • ↑s → ∀ ⦃a : H⦄, a ∈ g₁ • ↑s → a ∉ g₂ • ↑s

Tactic:
rintro a b hab _ ⟨c, hc, rfl⟩ ⟨d, hd, (hcd : b • d = a • c)⟩

Goal state after:
G : Type u_1
inst✝⁵ : Group G
S : Type u_3
H : Type u_4
inst✝⁴ : Group H
inst✝³ : SetLike S H
inst✝² : SubgroupClass S H
s : S
inst✝¹ : MulAction G H
inst✝ : IsScalarTower G Hᵐᵒᵖ H
a b : G
hab : a • ↑s ≠ b • ↑s
c : H
hc : c ∈ ↑s
d : H
hd : d ∈ ↑s
hcd : b • d = a • c
⊢ False
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case mp
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
B : Set X
inst✝ : IsPretransitive G X
hB : IsBlock G B
a : X
ha : a ∈ B
k : G
k_mem : k ∈ stabilizer G B
⊢ a ∈ B

Tactic:
exact ha

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
a : X
B : Set X
ha : a ∈ B
hB : IsBlock G B
⊢ a ∈ B

Tactic:
exact ha

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

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

Tactic:
apply isCyclic_of_card_dvd_prime (p := 3)

Goal state after:
case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : Nat.card α ≤ 3
h✝ : Nontrivial α
this : 1 < Nat.card α
⊢ Nat.card ↥(alternatingGroup α) ∣ 3
Module: Mathlib.SetTheory.Cardinal.Embedding

Goal state before:
pp: α : Type u_1
m n : ℕ
hmn : m ≤ n
hn : ↑n ≤ ENat.card α
⊢ Surjective fun x ↦ (castLEEmb hmn).trans x

Tactic:
by
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  exact Fin.Embedding.restrictSurjective_of_add_le_ENatCard hn

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

Goal state before:
pp: case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

Tactic:
Disjoint.cycleType_mul,

Goal state after:
case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ (swap 0 4).cycleType + (swap 1 3).cycleType = Multiset.replicate 2 2

case «2»
g : Perm (Fin 5)
h1 : g ≠ 1
h_1 : g.cycleType.card = 2
ha : Even 2
h2 : g.cycleType = Multiset.replicate 2 2
h✝ : 2 * 2 ≤ card (Fin 5)
h : 2 ≤ 3
h04 : 0 ≠ 4
h13 : 1 ≠ 3
⊢ (swap 0 4).Disjoint (swap 1 3)
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 α)
a : α
ha : a ∈ g.support
⊢ a ∈ g.support

Tactic:
exact ha

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

Goal state before:
pp: case pos
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
this : IsPretransitive G α
B : Set α
hB : IsBlock G B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : a = c
⊢ a ∈ B

Tactic:
exact ha

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 α
h2 : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
this : IsPretransitive G α
B : Set α
hB : ∀ ⦃g : G⦄ ⦃a : α⦄, a ∈ B → g • a ∈ B → g • B = B
a : α
ha : a ∈ B
b : α
hb : b ∈ B
h : a ≠ b
c : α
a✝ : c ∈ ⊤
h' : ¬a = c
g : G
hga : g • a = a
hgb : g • b = c
⊢ a ∈ B

Tactic:
exact ha

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

Goal state before:
pp: case hα
k : ℕ
hrec :
  ∀ {G : Type u_1} [inst : Group G] {α : Type u_2} [inst_1 : MulAction G α] [Finite α],
    IsMultiplyPretransitive G α k →
      ∀ {s : Set α}, s.ncard = k → (fixingSubgroup G s).index * (Nat.card α - k)! = (Nat.card α)!
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : Finite α
Hk : IsMultiplyPretransitive G α (k + 1)
s : Set α
hs : s.ncard = k + 1
⊢ k + 1 ≤ Nat.card α

Tactic:
· rw [← hs, ← Set.ncard_univ]
        exact ncard_le_ncard s.subset_univ finite_univ

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

Goal state before:
pp: case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
this : Nontrivial ↥(ofStabilizer G a)
⊢ False

Tactic:
rw [nontrivial_iff] at this

Goal state after:
case right
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hsn' : 2 < ENat.card α
hG' : IsMultiplyPretransitive G α 2
a : α
this✝¹ : IsPretransitive G α
this✝ : Nontrivial α
hGa : IsCoatom (stabilizer G a)
hyp : normalClosure ↑(stabilizer G a) ≤ stabilizer G a
this : ∃ x y, x ≠ y
⊢ False
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: case inl
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n = 0
⊢ IsMultiplyPreprimitive M α n

Tactic:
rw [hn]

Goal state after:
case inl
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
n : ℕ
hα : ↑n.succ ≤ ENat.card α
inst✝ : IsMultiplyPretransitive M α n.succ
hn : n = 0
⊢ IsMultiplyPreprimitive M α 0
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
⊢ alternatingGroup α ≤ G

Tactic:
rcases Nat.lt_or_ge (Nat.card α) 2 with hα1 | hα

Goal state after:
case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα1 : Nat.card α < 2
⊢ alternatingGroup α ≤ G

case inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
G : Subgroup (Equiv.Perm α)
hmt : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
hα : Nat.card α ≥ 2
⊢ alternatingGroup α ≤ G
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case refine_1
α : Type u_2
s : Set α
inst✝ : DecidablePred fun x ↦ x ∈ s
g : Perm ↑s
w : α
hs : w ∈ s
⊢ (ofSubtype g) w ∈ s

Tactic:
simp [ofSubtype_apply_of_mem _ hs]

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

Goal state before:
pp: case 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 α)))
⊢ ∃ g, g.IsSwap ∧ g ∈ G

Tactic:
cases G.eq_bot_or_eq_top_of_prime_card with
  | inl h =>
    exfalso; exact ne_bot_of_gt hG h
  | inr h =>
    rw [h, ← stabilizer_univ_eq_top (Perm α) α]
    apply this
    simp_all

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (↥(alternatingGroup α)) s ≤ G
⊢ G = ⊤

Tactic:
by
  obtain ⟨g, hg, hg3⟩ := exists_mem_stabilizer_isThreeCycle s h4
  rw [eq_top_iff, ← Subgroup.map_subtype_le_map_subtype,
    ← MonoidHom.range_eq_map, Subgroup.range_subtype]
  -- By Jordan's theorem, it suffices to prove that G acts primitively
  apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem _ hg3
  · use ⟨g, hg3.mem_alternatingGroup⟩
    simpa only [SetLike.mem_coe, Subgroup.subtype_apply, and_true] using hG hg
  · let φ := (alternatingGroup α).subtype.subgroupMap G
    let f : α →ₑ[φ] α := {
      toFun := id
      map_smul' _ _ := rfl }
    rwa [← isPreprimitive_congr (f := f) ((alternatingGroup α).subtype.subgroupMap_surjective G)
      Function.bijective_id]

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

Goal state before:
pp: case inr.hsn'
α : 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
⊢ n + 2 < Nat.card α

Tactic:
rw [hn]

Goal state after:
case inr.hsn'
α : 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
⊢ n + 2 < n + 3
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
⊢ ∀ (hy : ∀ a ∈ v, a < Fintype.card α), u.Disjoint v → (klift' u hu).Disjoint (klift' v hy)

Tactic:
hv

Goal state after:
case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := fun n hn ↦ ⟨n, hn⟩
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := fun l hl ↦ pmap klift l hl
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := pmap klift' c.ranges hc'_lt
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
u : List ℕ
hu : ∀ a ∈ u, a < Fintype.card α
v : List ℕ
hv : ∀ a ∈ v, a < Fintype.card α
⊢ u.Disjoint v → (klift' u hu).Disjoint (klift' v hv)
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: case h.right.right
α : Type u_2
inst✝ : Fintype α
c : List ℕ
hc : c.sum ≤ Fintype.card α
klift : (n : ℕ) → n < Fintype.card α → Fin (Fintype.card α) := ⋯
klift' : (l : List ℕ) → (∀ a ∈ l, a < Fintype.card α) → List (Fin (Fintype.card α)) := ⋯
hc'_lt : ∀ l ∈ c.ranges, ∀ n ∈ l, n < Fintype.card α
l : List (List (Fin (Fintype.card α))) := ⋯
hl : ∀ (a : List ℕ) (ha : a ∈ c.ranges), map (⇑Fin.valEmbedding) (klift' a ⋯) = a
⊢ Pairwise Disjoint (map (map ⇑(Fintype.equivFin α).symm) l)

Tactic:
refine Pairwise.map _ (fun s t ↦ disjoint_map (Equiv.injective _)) ?_
    -- List.Pairwise List.disjoint l
    apply Pairwise.pmap (List.ranges_disjoint c)
    intro u hu v hv huv
    apply disjoint_pmap
    · intro a a' ha ha' h
      simpa only [klift, Fin.mk_eq_mk] using h
    exact huv

Goal state after: