mathlib-initiative/mathlib-tactics huggingface dataset:
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 ω
⊢ (cs.leftInvSeq ω).Nodup

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, nodup_reverse]

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 ω
⊢ (cs.rightInvSeq ω.reverse).Nodup
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 - b, ⋯⟩

Tactic:
simpa [← NNRat.coe_pos] using! h

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

Goal state before:
pp: α : Type u
L₁ L₂ L₃ : List (α × Bool)
h₁ : IsCyclicallyReduced L₂
h₂ : IsReduced (L₁ ++ L₂ ++ L₃)
n✝ n : ℕ
hn : n + 1 ≠ 0
h : ¬L₂ = []
⊢ IsReduced (L₁ ++ (replicate (n + 1) L₂).flatten ++ L₃)

Tactic:
have h' : (replicate (n + 1) L₂).flatten ≠ [] := by simp [h]
    refine IsReduced.append_overlap ?_ ?_ (hn := h')
    · rw [replicate_succ, flatten_cons, ← append_assoc]
      refine IsReduced.append_overlap (h₂.infix ⟨[], L₃, by simp⟩) ?_ h
      rw [← flatten_cons, ← replicate_succ]
      exact (h₁.flatten_replicate _).isReduced
    · rw [replicate_succ', flatten_concat]
      refine IsReduced.append_overlap ?_ (h₂.infix ⟨L₁, [], by simp⟩) h
      rw [← flatten_concat, ← replicate_succ']
      exact (h₁.flatten_replicate _).isReduced

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
⊢ IsNilpotent G ↔ IsNilpotent H

Tactic:
isNilpotent_iff

Goal state after:
G : Type u_1
inst✝¹ : Group G
H : Type u_2
inst✝ : Group H
e : G ≃* H
⊢ (∃ n, upperCentralSeries G n = ⊤) ↔ ∃ n, upperCentralSeries H n = ⊤
Module: Mathlib.GroupTheory.Goursat

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
I : Subgroup (G × H)
g : G
⊢ g ∈ I.goursatFst ↔ (g, 1) ∈ I

Tactic:
by simp [goursatFst]

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_3
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ upperCentralSeries G i = upperCentralSeries G j → i = j

Tactic:
refine (upperCentralSeries.StrictMonoOn G).injOn ?_ ?_

Goal state after:
case refine_3.refine_1
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ i ∈ Set.Iic (nilpotencyClass G)

case refine_3.refine_2
G : Type u_1
inst✝ : Group G
a : ℕ
h2 : a ≤ nilpotencyClass G
i j : ℕ
hi : i < a + 1
hj : j < a + 1
⊢ j ∈ Set.Iic (nilpotencyClass G)
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ IsBlock (↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)) (g • B)

Tactic:
rw [isBlock_iff_smul_eq_or_disjoint]

Goal state after:
G : Type u_1
inst✝¹ : Group G
X : Type u_2
inst✝ : MulAction G X
B : Set X
H : Subgroup G
hB : IsBlock (↥H) B
g : G
⊢ ∀ (g_1 : ↥(Subgroup.map (MulEquiv.toMonoidHom (MulAut.conj g)) H)),
    g_1 • g • B = g • B ∨ Disjoint (g_1 • g • B) (g • B)
Module: Mathlib.GroupTheory.GroupAction.Blocks

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

Tactic:
smul_smul (g * h * g⁻¹) g B,

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ IsBlock G (orbit (↥N) a)

Tactic:
rw [isBlock_iff_smul_eq_or_disjoint]

Goal state after:
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
N : Subgroup G
inst✝ : N.Normal
a : X
⊢ ∀ (g : G), g • orbit (↥N) a = orbit (↥N) a ∨ Disjoint (g • orbit (↥N) a) (orbit (↥N) a)
Module: Mathlib.GroupTheory.Perm.ConjAct

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
k : ConjAct (Perm α)
g c : Perm α
⊢ ConjAct.ofConjAct k * c * (ConjAct.ofConjAct k)⁻¹ ∈
      (ConjAct.ofConjAct k * g * (ConjAct.ofConjAct k)⁻¹).cycleFactorsFinset ↔
    c ∈ g.cycleFactorsFinset

Tactic:
apply mem_cycleFactorsFinset_conj g k

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 α
a : α
⊢ Cardinal.toENat (Cardinal.mk ↥(ofStabilizer G a)) + 1 = Cardinal.toENat (Cardinal.mk α)

Tactic:
rw [← Cardinal.mk_sum_compl {a}, map_add, add_comm, eq_comm]

Goal state after:
G : Type u_1
inst✝¹ : Group G
α : Type u_2
inst✝ : MulAction G α
a : α
⊢ Cardinal.toENat (Cardinal.mk ↑{a}) + Cardinal.toENat (Cardinal.mk ↑{a}ᶜ) =
    1 + Cardinal.toENat (Cardinal.mk ↥(ofStabilizer G a))
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
hσ✝ : σ ∈ alternatingGroup α
hσ : (↑⟨σ, hσ✝⟩).support.card + 2 ≤ card α
τ : Perm α
hτ : τ ∈ alternatingGroup α
hc : IsConj ↑⟨σ, hσ✝⟩ ↑⟨τ, hτ⟩
π : Perm α
hπ : π * σ * π⁻¹ = τ
h : sign π = 1
⊢ ↑(⟨π, ⋯⟩ * ⟨σ, hσ✝⟩ * ⟨π, ⋯⟩⁻¹) = ↑⟨τ, hτ⟩

Tactic:
simpa only [Subtype.val, Subgroup.coe_mul, coe_inv, coe_mk] using! 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 α
g : G
a b : α
hg : b = g • a
⊢ Function.Bijective ⇑(conjMap hg)

Tactic:
by
  constructor
  · rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy
    simp only [Subtype.mk_eq_mk]
    apply (MulAction.injective g)
    rwa [← SetLike.coe_eq_coe, conjMap_apply] at hxy
  · intro x
    exact ⟨conjMap _ x, inv_conjMap_comp_apply _ x⟩

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 α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
i : Fin n
⊢ (Fin.Embedding.init (g • x)) i ∈ ofStabilizer G a

Tactic:
simp only [mem_ofStabilizer_iff,
      Nat.succ_eq_add_one, ← hgx, ← smul_apply, ne_eq]

Goal state after:
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
x : Fin n.succ ↪ α
g : G
hgx : g • x (Fin.last n) = a
i : Fin n
⊢ ¬(Fin.Embedding.init (g • x)) i = (g • x) (Fin.last n)
Module: Mathlib.Topology.VectorBundle.Riemannian

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

Tactic:
← hgx,

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

Goal state after:
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 • (embFinTwo h) 1 = d
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: case neg
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
a b : α
h : ¬a = b
⊢ ∃ g, g • a = b

Tactic:
obtain ⟨g, h, _⟩ := h2 h (Ne.symm h)

Goal state after:
case neg
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
a b : α
h✝ : ¬a = b
g : G
h : g • a = b
right✝ : g • b = a
⊢ ∃ g, g • a = b
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
h2 : IsMultiplyPretransitive G α 2
a b : α
⊢ ∃ g, g • a = b

Tactic:
by
    by_cases h : a = b
    · exact ⟨1, by simp [h]⟩
    · rw [is_two_pretransitive_iff] at h2
      obtain ⟨g, h, _⟩ := h2 h (Ne.symm h)
      exact ⟨g, h⟩

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 α
inst✝ : IsPretransitive G α
n : ℕ
a : α
⊢ IsMultiplyPretransitive G α n.succ ↔ IsMultiplyPretransitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) n

Tactic:
refine ⟨fun hn ↦ ⟨fun x y ↦ ?_⟩, fun hn ↦ ⟨fun x y ↦ ?_⟩⟩

Goal state after:
case refine_1
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive G α n.succ
x y : Fin n ↪ ↥(ofStabilizer G a)
⊢ ∃ g, g • x = y

case refine_2
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : IsPretransitive G α
n : ℕ
a : α
hn : IsMultiplyPretransitive (↥(stabilizer G a)) (↥(ofStabilizer G a)) n
x y : Fin n.succ ↪ α
⊢ ∃ g, g • x = y
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 α
a : α
s : Set ↥(ofStabilizer M a)
m : ↥(fixingSubgroup M (insert a (Subtype.val '' s)))
x✝ : ↑s
x : ↥(ofStabilizer M a)
hx : x ∈ s
⊢ ↑x ∈ Subtype.val '' s

Tactic:
exact ⟨⟨x, (SubMulAction.mem_ofStabilizer_iff  M a).mp x.prop⟩, hx, rfl⟩

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

Goal state before:
pp: case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
⊢ Injective ⇑(conjMap_ofFixingSubgroup hst)

Tactic:
rintro x y hxy

Goal state after:
case left
M : Type u_1
α : Type u_2
inst✝¹ : Group M
inst✝ : MulAction M α
s t : Set α
g : M
hst : g • s = t
x y : ↥(ofFixingSubgroup M s)
hxy : (conjMap_ofFixingSubgroup hst) x = (conjMap_ofFixingSubgroup hst) y
⊢ x = y
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 : s.encard + 1 = ↑n.succ
b : α
hb : b ∈ s
g : M
hg : g • b = a
s' : Set α := g • s
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := Subtype.val ⁻¹' s'
hst : s' = insert a (Subtype.val '' t)
⊢ s = g⁻¹ • s'

Tactic:
simp [hs']

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

Goal state before:
pp: 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
hn1 : 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
ht : t.Finite
⊢ t.ncard = t.ncard - 1 + 1

Tactic:
apply (Nat.sub_eq_iff_eq_add ?_).mp rfl

Goal state after:
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
hn1 : 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
ht : t.Finite
⊢ 1 ≤ t.ncard
Module: Mathlib.GroupTheory.GroupAction.Jordan

Goal state before:
pp: 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
⊢ t.ncard = t.ncard - 1 + 1

Tactic:
apply (Nat.sub_eq_iff_eq_add ?_).mp rfl

Goal state after:
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
⊢ 1 ≤ t.ncard
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

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

Tactic:
by
  rw [mem_stabilizer_iff]
  ext g'
  simp_rw [mem_smul_set, Perm.smul_def]
  refine ⟨?_, fun a ↦ ?_⟩
  · rintro ⟨w, hs, rfl⟩
    simp [ofSubtype_apply_of_mem _ hs]
  · use (g⁻¹ ⟨g', a⟩)
    simp

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

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

pp: case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
⊢ IsTrivialBlock B

Tactic:
· replace h3 : Nat.card α = 3 := le_antisymm h3 h2
    have : IsPretransitive (alternatingGroup α) α := isPretransitive_of_three_le_card α h3.ge
    have : IsPreprimitive (alternatingGroup α) α := IsPreprimitive.of_prime_card (h3 ▸ prime_three)
    exact this.isTrivialBlock_of_isBlock hB

Goal state after:
case inr.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
B : Set α
hB : IsBlock (↥(alternatingGroup α)) B
h2 : 2 < Nat.card α
h4 : 3 < Nat.card α
⊢ IsTrivialBlock B
Module: Mathlib.GroupTheory.GroupExtension.Defs

Goal state before:
pp: N : Type u_1
E : Type u_2
G : Type u_3
inst✝³ : Group N
inst✝² : Group E
inst✝¹ : Group G
S : GroupExtension N E G
E' : Type u_4
inst✝ : Group E'
S' : GroupExtension N E' G
x✝² x✝¹ : S.Equiv S'
toMulEquiv✝¹ : E ≃* E'
inl_comm✝¹ : ⇑toMulEquiv✝¹ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝¹ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝¹ = ⇑S.rightHom
toMulEquiv✝ : E ≃* E'
inl_comm✝ : ⇑toMulEquiv✝ ∘ ⇑S.inl = ⇑S'.inl
rightHom_comm✝ : ⇑S'.rightHom ∘ ⇑toMulEquiv✝ = ⇑S.rightHom
h :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.toMulEquiv =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.toMulEquiv
x✝ :
  ⇑{ toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ }.symm =
    ⇑{ toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }.symm
⊢ { toMulEquiv := toMulEquiv✝¹, inl_comm := inl_comm✝¹, rightHom_comm := rightHom_comm✝¹ } =
    { toMulEquiv := toMulEquiv✝, inl_comm := inl_comm✝, rightHom_comm := rightHom_comm✝ }

Tactic:
congr
    rw [MulEquiv.ext_iff]
    exact congrFun h

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

Goal state before:
pp: case pos
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : n ≤ 2
⊢ IsMultiplyPretransitive K α n

Tactic:
apply MulAction.isMultiplyPretransitive_of_le' hn

Goal state after:
case pos
α : Type u_1
K : Type u_2
inst✝¹ : Group K
inst✝ : MulAction K α
hα : Nat.card α = 2
hK : fixedPoints K α ≠ _root_.Set.univ
n : ℕ
this✝ : Finite α
this : Fintype α
h2 : IsMultiplyPretransitive K α 2
hn : n ≤ 2
⊢ ↑2 ≤ ENat.card α
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 : S.Splitting
⊢ ⇑{
          toFun := fun x ↦
            match x with
            | ⟨n, g⟩ => S.inl n * s g,
          invFun := fun e ↦ ⟨Function.invFun (⇑S.inl) (e * (s (S.rightHom e))⁻¹), S.rightHom e⟩, left_inv := ⋯,
          right_inv := ⋯, map_mul' := ⋯ } ∘
      ⇑(SemidirectProduct.toGroupExtension s.conjAct).inl =
    ⇑S.inl

Tactic:
by
    ext n
    simp only [SemidirectProduct.toGroupExtension, Function.comp_apply, MulEquiv.coe_mk,
      Equiv.coe_fn_mk, SemidirectProduct.left_inl, SemidirectProduct.right_inl, map_one, mul_one]

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

Goal state before:
pp: case inr.inr
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n

Tactic:
have := alternatingGroup.isMultiplyPretransitive α

Goal state after:
case inr.inr
α✝ : Type u_2
n✝ : ℕ
inst✝² : DecidableEq α✝
α : Type u_2
n : ℕ
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hα : 3 ≤ Nat.card α
hn : 2 * n ≤ Nat.card α
hn0 : n ≠ 0
hn1 : n ≠ 1
this : IsMultiplyPretransitive (↥(alternatingGroup α)) α (Nat.card α - 2)
⊢ IsMultiplyPretransitive (↥(alternatingGroup α)) α n
Module: Mathlib.GroupTheory.IsSubnormal

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
hH : H.IsSubnormal
hK : K.IsSubnormal
⊢ (H ⊓ K).IsSubnormal

Tactic:
by
  simpa using hH.subgroupOf.trans' hK

Goal state after:
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
g : ↥A
w : NormalWord d
this : Cancels 1 (↑g • w) ↔ Cancels 1 w
hcan : ¬Cancels 1 w
⊢ (if h : Cancels 1 (↑g • w) then unitsSMulWithCancel φ 1 (↑g • w) h
    else
      let g' := unitsSMulGroup φ d 1 (↑g • w).head;
      cons (↑g'.1) 1 ((↑g'.2 * (↑g • w).head⁻¹) • ↑g • w) ⋯ ⋯) =
    ↑(φ g) •
      if h : Cancels 1 w then unitsSMulWithCancel φ 1 w h
      else
        let g' := unitsSMulGroup φ d 1 w.head;
        cons (↑g'.1) 1 ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯

Tactic:
rw [dif_neg (mt this.1 hcan), dif_neg hcan]
    -- Before https://github.com/leanprover/lean4/pull/2644, all this was just
    -- `simp [← mul_smul, mul_assoc, unitsSMulGroup]`
    simp +instances only [toSubgroup_neg_one, unitsSMulGroup, toSubgroup_one, toSubgroupEquiv_one,
      SetLike.coe_sort_coe, group_smul_head, mul_inv_rev, ← mul_smul, mul_assoc, inv_mul_cancel,
      mul_one, smul_cons]
    -- This used to be the end of the proof before https://github.com/leanprover/lean4/pull/2644
    congr 1
    · conv_lhs => erw [IsComplement.equiv_mul_left]
      simp_rw [toSubgroup_one]
      simp only [SetLike.coe_sort_coe, map_mul, Subgroup.coe_mul]
    conv_lhs => erw [IsComplement.equiv_mul_left]
    rfl

Goal state after:
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
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

Tactic:
have := ne_of_mem_of_not_mem ha hσa

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}
this : a ≠ Equiv.swap z w • a
⊢ False
Module: Mathlib.GroupTheory.Perm.ClosureSwap

Goal state before:
pp: case refine_3
α : 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.refl α ∈ closure S

Tactic:
apply one_mem

Goal state after: