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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : Nontrivial α
⊢ Nat.card ↥(alternatingGroup α) = (Nat.card α).factorial / 2

Tactic:
simp only [Nat.card_eq_fintype_card, card_alternatingGroup]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
h5 : 5 ≤ Nat.card α
⊢ closure {g | (↑g).cycleType = {2, 2}} = ⊤

Tactic:
by
  rw [← map_subtype_inj, MonoidHom.map_closure]
  have : (alternatingGroup α).subtype '' _ = {g : Perm α | g.cycleType = {2, 2}} :=
    Subtype.coe_image_of_subset cycleType_eq_two_two_subset_alternatingGroup
  have := closure_cycleType_eq_two_two_eq_alternatingGroup h5
  aesop

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
⊢ {2} + {2} = Multiset.replicate 2 2

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).Disjoint (swap 1 3)

Tactic:
· simp

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).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
⊢ g a ≠ a

Tactic:
← mem_support

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 : α
ha : a ∈ g.support
⊢ a ∈ g.support
Module: Mathlib.Topology.VectorBundle.Riemannian

Goal state before:
pp: case inl
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 : RiemannianMetric E
b : B
⊢ 0 ≤ RCLike.re (((g.inner b) 0) 0)

pp: case inr
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 : RiemannianMetric E
b : B
v : E b
hv : v ≠ 0
⊢ 0 ≤ RCLike.re (((g.inner b) v) v)

Tactic:
· simp

Goal state after:
case inr
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 : RiemannianMetric E
b : B
v : E b
hv : v ≠ 0
⊢ 0 ≤ RCLike.re (((g.inner b) v) v)
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)
⊢ ∃ g, g • x = y

Tactic:
have Hs : Nonempty (Fin (s.ncard) ≃ s) :=
      Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])

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)
⊢ ∃ g, g • x = y
Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s.encard + ↑m = ↑(s.ncard + m)

Tactic:
Nat.cast_add,

Goal state after:
M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
m n : ℕ
inst✝¹ : IsMultiplyPreprimitive M α n
s : Set α
inst✝ : Finite ↑s
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = ↑m
t' : Set α := Subtype.val '' t
htt' : t = Subtype.val ⁻¹' t'
⊢ s.encard + ↑m = ↑s.ncard + ↑m
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s : Set α
hs : IsPretransitive ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
g : M
ha : s ∪ g • s ≠ ⊤
⊢ IsPretransitive ↥(fixingSubgroup M (s ∩ g • s)) ↥(ofFixingSubgroup M (s ∩ g • s))

Tactic:
rw [Ne, Set.top_eq_univ, ← Set.compl_empty_iff, ← Ne, ← Set.nonempty_iff_ne_empty] at ha
  obtain ⟨a, ha⟩ := ha
  rw [Set.compl_union] at ha
  have ha' : a ∈ (s ∩ g • s)ᶜ := by
    rw [Set.compl_inter]
    exact Set.mem_union_left _ ha.1
  rw [MulAction.isPretransitive_iff_base (⟨a, ha'⟩ : ofFixingSubgroup M (s ∩ g • s))]
  rintro ⟨x, hx⟩
  rw [mem_ofFixingSubgroup_iff, Set.mem_inter_iff, not_and_or] at hx
  rcases hx with hx | hx
  · obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨a, ha.1⟩ ⟨x, hx⟩
    use ⟨k, fun ⟨y, hy⟩ ↦ hk ⟨y, hy.1⟩⟩
    rwa [Subtype.ext_iff] at hkax ⊢
  · have hg'x : g⁻¹ • x ∈ ofFixingSubgroup M s := mt Set.mem_smul_set_iff_inv_smul_mem.mpr hx
    have hg'a : g⁻¹ • a ∈ ofFixingSubgroup M s := mt Set.mem_smul_set_iff_inv_smul_mem.mpr ha.2
    obtain ⟨⟨k, hk⟩, hkax⟩ := hs.exists_smul_eq ⟨g⁻¹ • a, hg'a⟩ ⟨g⁻¹ • x, hg'x⟩
    use ⟨g * k * g⁻¹, ?_⟩
    · simp only [← SetLike.coe_eq_coe] at hkax ⊢
      rwa [SetLike.val_smul, Subgroup.mk_smul, eq_inv_smul_iff, smul_smul, smul_smul] at hkax
    · rw [mem_fixingSubgroup_iff] at hk ⊢
      intro y hy
      rw [mul_smul, mul_smul, smul_eq_iff_eq_inv_smul g]
      exact hk _ (Set.mem_smul_set_iff_inv_smul_mem.mp hy.2)

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 α
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
x✝ : ↥(fixingSubgroup M s)
g : M
hg : ∀ y ∈ s, g • y = y
y : β
hy : y ∈ t
this : ∃ x ∈ s, y = f x
⊢ φ g • y = y

Tactic:
obtain ⟨x, hx, rfl⟩ := this
        rwa [← map_smulₛₗ, hg]

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

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

Tactic:
intro k hk

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
s : Set α
k : G
hk : k ∈ fixingSubgroup G s
⊢ k ∈ stabilizer G s
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ 2 < sᶜ.ncard

Tactic:
by grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
⊢ Function.Surjective toPerm

Tactic:
have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s ↑k.support
hks : k • s = s
⊢ Function.Surjective toPerm
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
hα : 4 ≤ Nat.card α
t : Set α
a : α
ha : a ∈ t
b : α
hb : b ∈ t
hab : ¬a = b
ht : ¬2 < t.ncard
this : t.ncard + tᶜ.ncard = Nat.card α
⊢ 1 < tᶜ.ncard

Tactic:
by grind

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

Goal state before:
pp: case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < 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
⊢ sᶜ ⊆ B

Tactic:
have hB_not_le_s (B : Set α) (hB : IsBlock G B) (hBs : B ⊆ s) :
      B.Subsingleton :=
    have : IsPreprimitive (stabilizer G s) s :=
      stabilizer_subgroup_isPreprimitive h1 hG.le
    hB.subsingleton_of_stabilizer_lt_of_subset hB_not_le_sc hG hBs

Goal state after:
case right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nontrivial
hs : s.ncard < sᶜ.ncard
this✝ : s.ncard + sᶜ.ncard = Nat.card α
h1 : sᶜ.Nontrivial
hα : 4 < Nat.card α
G : Subgroup ↥(alternatingGroup α)
hG : stabilizer (↥(alternatingGroup α)) s < 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
⊢ sᶜ ⊆ B
Module: Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups

Goal state before:
pp: case pos
α✝ : Type u_1
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : s.Nontrivial
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

pp: case neg
α✝ : Type u_1
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : ¬s.Nontrivial
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)

Tactic:
· apply isCoatom_stabilizer_of_ncard_lt_ncard_compl h0' hs'

Goal state after:
case neg
α✝ : Type u_1
inst✝³ : Fintype α✝
inst✝² : DecidableEq α✝
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Set α
h0 : s.Nonempty
h1 : sᶜ.Nonempty
hs : ¬sᶜ.ncard = s.ncard
hs' : s.ncard < sᶜ.ncard
h0' : ¬s.Nontrivial
⊢ IsCoatom (stabilizer (↥(alternatingGroup α)) s)
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
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
f : E →* E'
comp_inl : f.comp S.inl = S'.inl
rightHom_comp : S'.rightHom.comp f = S.rightHom
e' : E'
⊢ (↑f).toFun
      ((fun e' ↦
          let e := Function.surjInv ⋯ (S'.rightHom e');
          e * S.inl (Function.invFun (⇑S'.inl) ((f e)⁻¹ * e')))
        e') =
    e'

Tactic:
by
    simp only [OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, map_mul]
    rw [← eq_inv_mul_iff_mul_eq, ← MonoidHom.comp_apply, comp_inl]
    apply Function.invFun_eq
    rw [← MonoidHom.mem_range, S'.range_inl_eq_ker_rightHom, MonoidHom.mem_ker, map_mul, map_inv,
      ← MonoidHom.comp_apply, rightHom_comp]
    simpa only [Function.surjInv_eq] using inv_mul_cancel (S'.rightHom e')

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

Goal state before:
pp: case inl
α : 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
⊢ G = ⊤

Tactic:
rw [Nat.lt_succ_iff] at hα3

Goal state after:
case inl
α : 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 α ≤ 2
⊢ G = ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step.inl.inl
G : Type u_1
inst✝ : Group G
H : Subgroup G
hS : ⊤.IsSubnormal
HK : ⊤ ≤ ⊤
hN : (⊤.subgroupOf ⊤).Normal
⊢ ⊤ = ⊤ ∨ ∃ K, ⊤ < K ∧ K.IsSubnormal ∧ (⊤.subgroupOf K).Normal

pp: case step.inl.inr
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
hH : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal

Tactic:
· simp

Goal state after:
case step.inl.inr
G : Type u_1
inst✝ : Group G
H✝ H : Subgroup G
HK : H ≤ ⊤
hS : ⊤.IsSubnormal
hN : (H.subgroupOf ⊤).Normal
hH : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, H < K ∧ K.IsSubnormal ∧ (H.subgroupOf K).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case inl
G : Type u_1
inst✝ : Group G
hN : ⊤.IsSubnormal
⊢ ⊤ = ⊤ ∨ ∃ K, K.Normal ∧ ⊤ ≤ K ∧ K < ⊤

pp: case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hN : H.IsSubnormal
H_ne : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤

Tactic:
· simp

Goal state after:
case inr
G : Type u_1
inst✝ : Group G
H : Subgroup G
hN : H.IsSubnormal
H_ne : H ≠ ⊤
⊢ H = ⊤ ∨ ∃ K, K.Normal ∧ H ≤ K ∧ K < ⊤
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : (A.subgroupOf B).Normal
ih : (map K.subtype B).IsSubnormal
⊢ ((map K.subtype A).subgroupOf (map K.subtype B)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Goal state after:
case step
G : Type u_1
inst✝ : Group G
K : Subgroup G
H : Subgroup ↥K
Ksn : K.IsSubnormal
A B : Subgroup ↥K
h_le : A ≤ B
hSubn : B.IsSubnormal
hN : B ≤ normalizer ↑A
ih : (map K.subtype B).IsSubnormal
⊢ ((map K.subtype A).subgroupOf (map K.subtype B)).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (map f K).IsSubnormal
⊢ ((map f H).subgroupOf (map f K)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Goal state after:
case step
G : Type u_1
inst✝¹ : Group G
H✝ : Subgroup G
G' : Type u_2
inst✝ : Group G'
f : G →* G'
hf : Function.Surjective ⇑f
H K : Subgroup G
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (map f K).IsSubnormal
⊢ ((map f H).subgroupOf (map f K)).Normal
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : (H.subgroupOf K).Normal
ih : (comap f K).IsSubnormal
⊢ ((comap f H).subgroupOf (comap f K)).Normal

Tactic:
rw [normal_subgroupOf_iff_le_normalizer h_le] at hN

Goal state after:
case step
G : Type u_1
inst✝¹ : Group G
G' : Type u_2
inst✝ : Group G'
H' : Subgroup G'
f : G →* G'
H K : Subgroup G'
h_le : H ≤ K
hSubn : K.IsSubnormal
hN : K ≤ normalizer ↑H
ih : (comap f K).IsSubnormal
⊢ ((comap f H).subgroupOf (comap f K)).Normal
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inr
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoidWithZero M
inst✝ : CommMonoidWithZero N
S : Submonoid M
f : S.LocalizationMap N
m : M
prime : Prime m
n0 : f m ≠ 0
nu : ¬IsUnit (f m)
n₁ n₂ : N
dvd✝¹ : f m ∣ n₁ * n₂
m₁ : M
s₁ : ↥S
eq₁ : n₁ * f ↑(m₁, s₁).2 = f (m₁, s₁).1
m₂ : M
s₂ : ↥S
eq₂ : n₂ * f ↑(m₂, s₂).2 = f (m₂, s₂).1
this✝ : ∃ s ∈ S, m ∣ s * ((m₁, s₁).1 * (m₂, s₂).1)
s : M
hs : s ∈ S
dvd✝ : m ∣ s * (m₁, s₁).1 * (m₂, s₂).1
dvd : m ∣ (m₂, s₂).1
this : f m ∣ f (m₂, s₂).1
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
· rw [← eq₂, (f.map_units s₂).dvd_mul_right] at this; exact .inr this

Goal state after:
Module: Mathlib.GroupTheory.Perm.Cycle.PossibleTypes

Goal state before:
pp: α : 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
a : List ℕ
ha : a ∈ c.ranges
⊢ map (⇑Fin.valEmbedding) (klift' a ⋯) = map id a

Tactic:
List.map_pmap

Goal state after:
α : 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
a : List ℕ
ha : a ∈ c.ranges
⊢ pmap (fun a h ↦ Fin.valEmbedding (klift a h)) a ⋯ = map id a
Module: Mathlib.GroupTheory.Perm.DomMulAct

Goal state before:
pp: α : Type u_1
ι : Type u_2
f : α → ι
g : (i : ι) → Perm { a // f a = i }
a : α
⊢ ↑((Equiv.symm (g (f a))) ⟨stabilizerEquiv_invFun g a, ⋯⟩) = a

Tactic:
exact congr_arg Subtype.val ((g <| f a).left_inv _)

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

Goal state before:
pp: case i_surj
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ b ∈ Finset.image f Finset.univ, ∃ a, ∃ (_ : a ∈ Finset.univ), ↑a = b

pp: case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a ∈ Finset.univ, (Fintype.card { a_1 // φ a_1 = a })! = (Fintype.card { a_1 // f a_1 = ↑a })!

Tactic:
· simp

Goal state after:
case h
α : Type u_1
ι : Type u_2
f : α → ι
inst✝² : Fintype α
inst✝¹ : DecidableEq α
inst✝ : DecidableEq ι
φ : α → ↥(Finset.image f Finset.univ) := ⋯
this : ∀ (g : Perm α), f ∘ ⇑g = f ↔ φ ∘ ⇑g = φ
⊢ ∀ a ∈ Finset.univ, (Fintype.card { a_1 // φ a_1 = a })! = (Fintype.card { a_1 // f a_1 = ↑a })!
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ (g •
      let g' := unitsSMulGroup φ d u w.head;
      cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯) =
    cons g u w h1 h2

Tactic:
simp only [unitsSMulGroup, (d.compl _).equiv_fst_eq_one_of_mem_of_one_mem (one_mem _) h1,
      (d.compl _).equiv_snd_eq_inv_mul, inv_one, one_mul, mul_inv_cancel, one_smul, smul_cons]

Goal state after:
case cons
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
g : G
u : ℤˣ
w : NormalWord d
h1 : w.head ∈ d.set u
h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ toSubgroup A B u → u = u'
ih : ReducedWord.prod φ w.toReducedWord • empty = w
⊢ cons (g * ↑((toSubgroupEquiv φ u) ⟨1, ⋯⟩)) u w ⋯ ⋯ = cons g u w h1 h2
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_4
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
σ : Equiv.Perm α
hσ : σ ∈ S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
hσa : σ • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ False

Tactic:
obtain ⟨z, w, hzw, rfl⟩ := hS σ hσ

Goal state after:
case refine_4
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : Equiv.swap x y ∉ closure S
a : α
ha : a ∈ {x | Equiv.swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : Equiv.swap z w ∈ S
hσa : Equiv.swap z w • a ∉ {x | Equiv.swap x y ∈ closure S}
⊢ False
Module: Mathlib.GroupTheory.HNNExtension

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ w',
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
hw1 : ¬w.head = 1
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)

Tactic:
rcases this ⟨1, w.toList, w.chain⟩ rfl with ⟨w', hw'⟩

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
d : TransversalPair G A B
w : ReducedWord G A B
this :
  ∀ (w : ReducedWord G A B),
    w.head = 1 →
      ∃ w',
        ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
          List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
            ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head ∈ toSubgroup A B (-u)
hw1 : ¬w.head = 1
w' : NormalWord d
hw' :
  ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ { head := 1, toList := w.toList, chain := ⋯ } ∧
    List.map Prod.fst w'.toList = List.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ }.toList ∧
      ∀ u ∈ Option.map Prod.fst { head := 1, toList := w.toList, chain := ⋯ }.toList.head?,
        w'.head ∈ toSubgroup A B (-u)
⊢ ∃ w',
    ReducedWord.prod φ w'.toReducedWord = ReducedWord.prod φ w ∧
      List.map Prod.fst w'.toList = List.map Prod.fst w.toList ∧
        ∀ u ∈ Option.map Prod.fst w.toList.head?, w'.head⁻¹ * w.head ∈ toSubgroup A B (-u)
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x✝ : α
h : ¬f x✝ = 1 x✝
⊢ False

Tactic:
exact emp h

Goal state after: