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

Goal state before:
pp: ι : 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 α
hpp : Pairwise fun i j ↦ ∀ (h : H i), h ≠ 1 → (f i) h • X j ⊆ X i
i✝ j✝ i j k✝ l : ι
w₁ : NeWord H i j
hne : j ≠ k✝
w₂ : NeWord H k✝ l
hIw₁ : ∀ {k : ι}, j ≠ k → (lift f) w₁.prod • X k ⊆ X i
hIw₂ : ∀ {k : ι}, l ≠ k → (lift f) w₂.prod • X k ⊆ X k✝
k : ι
hk : l ≠ k
⊢ (lift f) (w₁.append hne w₂).prod • X k = (lift f) w₁.prod • (lift f) w₂.prod • X k

Tactic:
by
        simp [mul_smul]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this : ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
⊢ ↑1 • ↑(⟨a.den, ⋯⟩ * (⟨b.den, ⋯⟩ * s)) • (a * b).num • m = ↑1 • ↑(⟨(a * b).den, ⋯⟩ * s) • a.num • b.num • m

Tactic:
convert! this using 1

Goal state after:
case e'_2
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this : ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
⊢ ↑1 • ↑(⟨a.den, ⋯⟩ * (⟨b.den, ⋯⟩ * s)) • (a * b).num • m = ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m

case e'_3
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this : ((a * b).num * ↑a.den * ↑b.den * ↑↑s) • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
⊢ ↑1 • ↑(⟨(a * b).den, ⋯⟩ * s) • a.num • b.num • m = (a.num * b.num * ↑(a * b).den * ↑↑s) • m
Module: Mathlib.GroupTheory.DoubleCoset

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a b : G
h : ¬Disjoint (doubleCoset a ↑H ↑K) (doubleCoset b ↑H ↑K)
⊢ doubleCoset a ↑H ↑K = doubleCoset b ↑H ↑K

Tactic:
by
  rw [disjoint_comm] at h
  have ha : a ∈ doubleCoset b H K := mem_doubleCoset_of_not_disjoint h
  apply doubleCoset_eq_of_mem ha

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * ↑a.den * ↑b.den * (↑↑s * ↑↑s)) • m =
    ((a.num * ↑b.den + b.num * ↑a.den) * ↑(a + b).den * (↑↑s * ↑↑s)) • m
⊢ ↑1 • ↑(⟨a.den, ⋯⟩ * s * (⟨b.den, ⋯⟩ * s)) • (a + b).num • m =
    ↑1 • ↑(⟨(a + b).den, ⋯⟩ * s) • (↑(⟨b.den, ⋯⟩ * s) • a.num • m + ↑(⟨a.den, ⋯⟩ * s) • b.num • m)

Tactic:
convert! this using 1

Goal state after:
case e'_2
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * ↑a.den * ↑b.den * (↑↑s * ↑↑s)) • m =
    ((a.num * ↑b.den + b.num * ↑a.den) * ↑(a + b).den * (↑↑s * ↑↑s)) • m
⊢ ↑1 • ↑(⟨a.den, ⋯⟩ * s * (⟨b.den, ⋯⟩ * s)) • (a + b).num • m = ((a + b).num * ↑a.den * ↑b.den * (↑↑s * ↑↑s)) • m

case e'_3
M✝ : Type u_1
inst✝¹ : AddCommMonoid M✝
M : Type u_2
inst✝ : AddCommGroup M
a b : ℚ
m : M
s : ℕ+
this :
  ((a + b).num * ↑a.den * ↑b.den * (↑↑s * ↑↑s)) • m =
    ((a.num * ↑b.den + b.num * ↑a.den) * ↑(a + b).den * (↑↑s * ↑↑s)) • m
⊢ ↑1 • ↑(⟨(a + b).den, ⋯⟩ * s) • (↑(⟨b.den, ⋯⟩ * s) • a.num • m + ↑(⟨a.den, ⋯⟩ * s) • b.num • m) =
    ((a.num * ↑b.den + b.num * ↑a.den) * ↑(a + b).den * (↑↑s * ↑↑s)) • m
Module: Mathlib.GroupTheory.FiniteIndexNormalSubgroup

Goal state before:
pp: G : Type u_1
inst✝² : Group G
H : Type u_2
N : Type u_3
inst✝¹ : Group H
inst✝ : Group N
f : G →* H
K : FiniteIndexNormalSubgroup H
⊢ (Subgroup.comap f K.toSubgroup).FiniteIndex

Tactic:
let g : G →* (H ⧸ K.toSubgroup) := (QuotientGroup.mk' K.toSubgroup).comp f
    have hker : K.toSubgroup.comap f = g.ker := by
      simpa using MonoidHom.comap_ker (g := QuotientGroup.mk' K.toSubgroup) (f := f)
    simpa [hker] using (inferInstance : g.ker.FiniteIndex)

Goal state after:
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)
Φ : (Subgroup (G →* Mˣ))ᵒᵈ
⊢ (fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker)
      ((fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker) Φ) =
    Φ

Tactic:
by
    have : HasEnoughRootsOfUnity M (Monoid.exponent (G →* Mˣ)) := by
      rwa [Monoid.exponent_eq_of_mulEquiv (monoidHom_mulEquiv_of_hasEnoughRootsOfUnity G M).some]
    ext φ
    rw [OrderDual.ofDual_toDual, mem_ker, domRestrictHom_apply, domRestrict_eq_one_iff]
    simp

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
⊢ ∃ T, #T ≤ H.index * #S ∧ closure ↑T = ⊤

Tactic:
have : DecidableEq G := Classical.decEq G

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
⊢ ∃ T, #T ≤ H.index * #S ∧ closure ↑T = ⊤
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
f : G →* H
hf : Surjective ⇑f
T : Set G
hT_fin : T.Finite
hT : normalClosure T = f.ker
S : Set G
hS_fin : S.Finite
hS : normalClosure (⇑f '' S) = N
⊢ normalClosure (S ∪ T) = normalClosure S ⊔ f.ker

Tactic:
← hT,

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
N : Subgroup H
f : G →* H
hf : Surjective ⇑f
T : Set G
hT_fin : T.Finite
hT : normalClosure T = f.ker
S : Set G
hS_fin : S.Finite
hS : normalClosure (⇑f '' S) = N
⊢ normalClosure (S ∪ T) = normalClosure S ⊔ normalClosure T
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_2
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
n : ℕ
h : upperCentralSeries H n = ⊤
⊢ upperCentralSeries G n = ⊤

Tactic:
simp [← Subgroup.comap_top e.toMonoidHom, ← h]

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

Goal state before:
pp: α : Type u_1
X : Type u_2
inst✝¹ : DecidableEq α
inst✝ : MulAction (FreeGroup α) X
x : X
w : α × Bool
g : FreeGroup α
hg : g ∈ startsWith w
l✝ : List (α × Bool) := g.toWord
h : ⟨g, hg⟩ = ⟨mk g.toWord, ⋯⟩
a b : α × Bool
l : List (α × Bool)
hl : a :: b :: l = g.toWord
ha : a = w
h1 : (a.1 = b.1 → a.2 = b.2) ∧ IsReduced (b :: l)
⊢ mk (b :: l) ∈ startsWith b

Tactic:
simp [startsWith, h1.2.reduce_eq]

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

Goal state before:
pp: case mpr
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
a : X
H : Subgroup G
hH : stabilizer G a ≤ H
g : G
⊢ g ∈ H → g ∈ stabilizer G (orbit (↥H) a)

Tactic:
· intro hg
    rw [mem_stabilizer_iff, ← Subgroup.coe_mk H g hg, ← Submonoid.smul_def (S := H.toSubmonoid)]
    apply smul_orbit (G := H)

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
⊢ stabilizer G sᶜ = stabilizer G s

Tactic:
have (s : Set α) : stabilizer G s ≤ stabilizer G (sᶜ) := by
    intro g h
    simp [Set.smul_set_compl, mem_stabilizer_iff.1 h]

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
this : ∀ (s : Set α), stabilizer G s ≤ stabilizer G sᶜ
⊢ stabilizer G sᶜ = stabilizer G s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

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

Tactic:
Nat.succ_inj

Goal state after:
case succ
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ : σ ∈ alternatingGroup α
n : ℕ
ih : ∀ (l : List (Perm α)), (∀ g ∈ l, g.IsSwap) → l.length = 2 * n → l.prod ∈ closure {σ | σ.IsThreeCycle}
a : Perm α
l : List (Perm α)
hl : ∀ g ∈ a :: l, g.IsSwap
hn : l.length = 2 * n + 1
⊢ (a :: l).prod ∈ closure {σ | σ.IsThreeCycle}
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
⊢ (swap 0 4 * swap 1 3).cycleType = Multiset.replicate 2 2

Tactic:
have h13 : (1 : Fin 5) ≠ 3 := by decide

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 * swap 1 3).cycleType = Multiset.replicate 2 2
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 • b = d

Tactic:
by rw [← embFinTwo_apply_one h, ← smul_apply, e, embFinTwo_apply_one]

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 α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : g • j 0 = j' 0
h' : g • j 1 = j' 1
i : Fin 2
hi : i = 0
⊢ (g • j) i = j' i

pp: case neg
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : g • j 0 = j' 0
h' : g • j 1 = j' 1
i : Fin 2
hi : ¬i = 0
⊢ (g • j) i = j' i

Tactic:
· simp [hi, h]

Goal state after:
case neg
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
H : ∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d
j j' : Fin 2 ↪ α
g : G
h : g • j 0 = j' 0
h' : g • j 1 = j' 1
i : Fin 2
hi : ¬i = 0
⊢ (g • j) i = j' i
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case mpr
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
⊢ (∀ {a b c d : α}, a ≠ b → c ≠ d → ∃ g, g • a = c ∧ g • b = d) → IsMultiplyPretransitive G α 2

Tactic:
intro H
    constructor
    intro j j'
    obtain ⟨g, h, h'⟩ :=
      H (j.injective.ne_iff.mpr Fin.zero_ne_one) (j'.injective.ne_iff.mpr Fin.zero_ne_one)
    use g
    ext i
    by_cases hi : i = 0
    · simp [hi, h]
    · simp [eq_one_of_ne_zero i hi, 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
this : RiemannianBundle E := { g := g.toRiemannianMetric }
⊢ IsContinuousRiemannianBundle F E

Tactic:
exact ⟨⟨g.inner, g.continuous, fun b v w ↦ rfl⟩⟩

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : 1 = n.succ
h : s = ∅
⊢ n < 1

Tactic:
Nat.succ_inj

Goal state after:
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
inst✝ : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : 0 = n
h : s = ∅
⊢ n < 1
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s✝ s t : Set α
x : ↥(ofFixingSubgroup M (s ∪ t))
hx : ⟨↑x, ⋯⟩ ∈ Subtype.val ⁻¹' t
⊢ ↑x ∈ s ∪ t

Tactic:
by
          apply Set.mem_union_right s
          simpa only [Set.mem_preimage, Subtype.coe_mk] using hx

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

Goal state before:
pp: case h'
n : ℕ
hrec :
  ∀ m < n,
    ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
      IsPreprimitive G α →
        ∀ {s : Set α},
          s.ncard = m + 1 →
            m + 2 < Nat.card α →
              (IsPretransitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPretransitive G α 2) ∧
                (IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → IsMultiplyPreprimitive G α 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1
hsn' : n + 2 < Nat.card α
this : Finite α
hs_ne_univ : s ≠ Set.univ
hs_nonempty : s.Nonempty
hn : n + 1 ≥ 2
hn2 : 2 * (n + 1) ≥ Nat.card α
a : α
ha✝ : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
g : G
hga : a ∈ g • sᶜ
hgb : b ∉ g • sᶜ
t : Set α := s ∩ g • s
ha : a ∉ s ∪ g • s
⊢ Nat.card α ≤ 2 * (n + 1)

Tactic:
exact hn2

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

Goal state before:
pp: case right.hf.right
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
y : α
hx : f y ∈ ofFixingSubgroup N t
⊢ ∃ a, g a = ⟨f y, hx⟩

Tactic:
suffices y ∈ ofFixingSubgroup M s by
          exact ⟨⟨y, this⟩, rfl⟩

Goal state after:
case right.hf.right
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
N : Type u_3
β : Type u_4
inst✝¹ : Group N
inst✝ : MulAction N β
φ : M → N
hφ : Function.Surjective φ
f : α →ₑ[φ] β
hf : Function.Bijective ⇑f
n : ℕ
H : IsMultiplyPreprimitive N β n
s : Set α
hs : s.encard + 1 = ↑n
t : Set β := ⇑f '' s
ψ : ↥(fixingSubgroup M s) → ↥(fixingSubgroup N t) :=
  fun x ↦
    match x with
    | ⟨g, hg⟩ => ⟨φ g, ⋯⟩
g : ↥(ofFixingSubgroup M s) →ₑ[ψ] ↥(ofFixingSubgroup N t) := { toFun := fun x ↦ ⟨f ↑x, ⋯⟩, map_smul' := ⋯ }
y : α
hx : f y ∈ ofFixingSubgroup N t
⊢ y ∈ ofFixingSubgroup M s
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
g : Perm ↑s
⊢ ∃ a, toPerm a = g

Tactic:
obtain ⟨⟨k, hk⟩, rfl⟩ := stabilizer.surjective_toPerm s g

Goal state after:
α : Type u_2
s B : Set α
G : Subgroup (Perm α)
hB : IsBlock (↥G) B
hB_ss_sc : B ⊂ s
hG : stabilizer (Perm α) s ≤ G
k : Perm α
hk : k ∈ stabilizer (Perm α) s
⊢ ∃ a, toPerm a = toPerm ⟨k, hk⟩
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s B : Set α
G : Subgroup M
inst✝ : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
hB : IsBlock (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = Set.univ
⊢ B.Subsingleton

Tactic:
have hBs' : B = s := Set.Subset.antisymm hBs (by simp_all)

Goal state after:
case inr
M : Type u_1
α : Type u_2
inst✝² : Group M
inst✝¹ : MulAction M α
s B : Set α
G : Subgroup M
inst✝ : IsPreprimitive ↥(stabilizer (↥G) s) ↑s
hB : IsBlock (↥G) B
hB_not_le_sc : ∀ (B : Set α), IsBlock (↥G) B → B ⊆ sᶜ → B.Subsingleton
hG : stabilizer M s < G
hBs : B ⊆ s
hB' : Subtype.val ⁻¹' B = Set.univ
hBs' : B = s
⊢ B.Subsingleton
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: n : ℕ
hrec :
  ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α],
    IsPreprimitive G α →
      ∀ {s : Set α},
        s.ncard = n + 1 →
          n + 2 < Nat.card α →
            IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) → Finite α → IsMultiplyPreprimitive G α (n + 2)
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
hG : IsPreprimitive G α
s : Set α
hsn : s.ncard = n + 1 + 1
hsn' : n + 1 + 2 < Nat.card α
hprim : IsPreprimitive ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s)
hα : Finite α
this : ∃ a t, a ∈ s ∧ s = insert a (Subtype.val '' t)
⊢ IsMultiplyPreprimitive G α (n + 1 + 2)

Tactic:
by
      obtain ⟨a, t, _, hst⟩ := this
      have ha' : a ∉ Subtype.val '' t := by
        intro h; rw [Set.mem_image] at h; obtain ⟨x, hx⟩ := h
        apply x.prop; rw [hx.right]; exact Set.mem_singleton a
      have ht_prim : IsPreprimitive (stabilizer G a) (SubMulAction.ofStabilizer G a) := by
        rw [← is_one_preprimitive_iff]
        rw [← isMultiplyPreprimitive_succ_iff_ofStabilizer]
        · apply is_two_preprimitive hG hsn hsn' hprim
        · norm_num
      have : IsPreprimitive ↥(fixingSubgroup G (insert a (Subtype.val '' t)))
          (ofFixingSubgroup G (insert a (Subtype.val '' t))) :=
        IsPreprimitive.of_surjective
          (ofFixingSubgroup_of_eq_bijective (hst := hst)).surjective
      have hGs' : IsPreprimitive (fixingSubgroup (stabilizer G a) t)
        (ofFixingSubgroup (stabilizer G a) t) :=
        IsPreprimitive.of_surjective
          ofFixingSubgroup_insert_map_bijective.surjective
      rw [isMultiplyPreprimitive_succ_iff_ofStabilizer G (a := a) _ (Nat.le_add_left 1 (n + 1))]
      refine hrec ht_prim ?_ ?_ hGs' Subtype.finite
      · -- t.card = Nat.succ n
        rw [← Set.ncard_image_of_injective t Subtype.val_injective]
        apply Nat.add_right_cancel
        rw [← Set.ncard_insert_of_notMem ha', ← hst, hsn]
      · -- n + 2 < Nat.card (SubMulAction.ofStabilizer G α a)
        rw [← Nat.add_lt_add_iff_right, nat_card_ofStabilizer_add_one_eq]
        exact hsn'

Goal state after:
Module: Mathlib.GroupTheory.GroupExtension.Basic

Goal state before:
pp: N : Type u_1
G : Type u_2
inst✝² : Group N
inst✝¹ : Group G
E : Type u_3
inst✝ : Group E
S : GroupExtension N E G
σ σ' : S.Section
g : G
n : N
hn : S.inl n = σ g * (σ' g)⁻¹
⊢ σ g = S.inl n * σ' g

Tactic:
rw [hn, inv_mul_cancel_right]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

Goal state before:
pp: G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ Finset.map (f.trans (Equiv.toEmbedding (toPerm g))) Finset.univ = id g • Finset.map f Finset.univ

Tactic:
smul_finset_def,

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
s t : ↑(powersetCard α n)
inst✝ : DecidableEq α
g : G
f : Fin n ↪ α
⊢ Finset.map (f.trans (Equiv.toEmbedding (toPerm g))) Finset.univ =
    Finset.image (fun x ↦ id g • x) (Finset.map f Finset.univ)
Module: Mathlib.GroupTheory.IsPerfect

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : Nontrivial G
inst✝ : IsPerfect G
h : IsSolvable G
⊢ False

Tactic:
exact (h.commutator_lt_top_of_nontrivial G).ne commutator_eq_top

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : CommMonoidWithZero M
inst✝¹ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
inst✝ : UniqueFactorizationMonoid M
this : IsCancelMulZero N
n : N
hn : n ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated f.prod n

Tactic:
have ⟨⟨m, s⟩, eq⟩ := f.surj n
    use ((factors m).map f).filter (¬ IsUnit ·)
    rw [Ne, ← (f.map_units s).mul_left_eq_zero, eq] at hn
    refine ⟨fun x hx ↦ ?_, .trans (eq ▸ ?_) ((associated_mul_unit_left _ _ (f.map_units s)))⟩
    · rw [Multiset.mem_filter, Multiset.mem_map] at hx
      obtain ⟨p, hp, rfl⟩ := hx.1
      exact f.map_prime (prime_of_factor _ hp)
        (mt (fun h ↦ eq_zero_of_zero_dvd <| h ▸ map_dvd f (dvd_of_mem_factors hp)) hn) hx.2
    · exact .trans (.trans (associated_unit_mul_right _ _ <|
        IsUnit.multisetProd_iff.mpr fun x hx ↦ (Multiset.mem_filter.mp hx).2) <| .of_eq <|
        (Multiset.prod_filter_mul_prod_filter_not _).trans (f.toMonoidHom.map_multiset_prod _).symm)
        ((factors_prod (mt (by simp [·]) hn)).map f)

Goal state after:
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 : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
| (g ^ m) (a (↑τ c)) ≠ x

Tactic:
rw [← hm]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
τ : ↥(range_toPermHom' g)
x : α
c : ↥g.cycleFactorsFinset
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
| (g ^ m) (a (↑τ c)) ≠ (g ^ m) (a c)
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.Centralizer

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
i : ℕ
hi : ∃ a ∈ g.cycleFactorsFinset.val, (card ∘ support) a = i
⊢ Odd i

Tactic:
obtain ⟨c, hc, rfl⟩ := hi

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
h : Subgroup.centralizer {g} ≤ alternatingGroup α
c : Perm α
hc : c ∈ g.cycleFactorsFinset.val
⊢ Odd ((card ∘ support) c)
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case intro
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝² : Monoid K
inst✝¹ : (i : ι) → Monoid (G i)
inst✝ : Monoid H
φ : (i : ι) → H →* G i
f g : PushoutI φ →* K
h : ∀ (i : ι), f.comp (of i) = g.comp (of i)
i : ι
x✝ : H
⊢ (f.comp (base φ)) x✝ = (g.comp (base φ)) x✝

Tactic:
rw [← of_comp_eq_base i, ← MonoidHom.comp_assoc, h, MonoidHom.comp_assoc]

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ Function.Injective ⇑(noncommPiCoprod ⋯)

pp: case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range

Tactic:
· apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
    · intro a
      simp only [range_subtype, ne_eq]
      simp only [zpowers_eq_closure, ← closure_iUnion]
      apply disjoint_closure_of_disjoint_support
      rintro - ⟨-⟩ - ⟨-, ⟨b, rfl⟩, -, ⟨h, rfl⟩, ⟨-⟩⟩
      rw [← disjoint_iff_disjoint_support]
      apply cycleFactorsFinset_pairwise_disjoint g a.2 b.2
      simp only [ne_eq, ← Subtype.ext_iff]
      exact ne_comm.mp h
    · exact fun i ↦ subtype_injective _

Goal state after:
case refine_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
⊢ _root_.Disjoint ofSubtype.range (noncommPiCoprod ⋯).range
Module: Mathlib.GroupTheory.SchurZassenhaus

Goal state before:
pp: G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
⊢ (Nat.card ↥(comap K.subtype N)).Coprime (comap K.subtype N).index

Tactic:
rw [h4]

Goal state after:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
inst✝ : Finite G
K : Subgroup G
hK : K ⊔ N = ⊤
h3 : K ≠ ⊤
h4 : (comap K.subtype N).index = N.index
h5 : Nat.card ↥K < Nat.card G
⊢ (Nat.card ↥(comap K.subtype N)).Coprime N.index