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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H K : Subgroup G
a : G
⊢ ⋃ k, op (a * ↑k) • ↑H = doubleCoset a ↑H ↑K

Tactic:
by
  ext x
  simp only [mem_rightCoset_iff, mul_inv_rev, Set.mem_iUnion, mem_doubleCoset,
    SetLike.mem_coe]
  constructor
  · rintro ⟨y, h_h⟩
    refine ⟨x * (y⁻¹ * a⁻¹), h_h, y, y.2, ?_⟩
    simp only [← mul_assoc, inv_mul_cancel_right, InvMemClass.coe_inv]
  · rintro ⟨x, hx, y, hy, hxy⟩
    refine ⟨⟨y, hy⟩, ?_⟩
    simp only [hxy, ← mul_assoc, hx, mul_inv_cancel_right]

Goal state after:
Module: Mathlib.GroupTheory.DivisibleHull

Goal state before:
pp: M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
m : M
s s' : ℕ+
this : ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')
⊢ ArchimedeanClass.mk (mk m s) = ArchimedeanClass.mk (mk m s')

Tactic:
exact this

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
inst✝¹ : LinearOrder M
inst✝ : IsOrderedAddMonoid M
a b : DivisibleHull M
h : ArchimedeanClass.mk a ≤ ArchimedeanClass.mk b
⊢ a.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯ ≤ b.liftOn (fun m s ↦ ArchimedeanClass.mk m) ⋯

Tactic:
by
      induction a with | mk _ _
      induction b with | mk _ _
      simp_rw [aux_archimedeanClassMk_mk] at h
      simpa using ((archimedeanClassOrderHom M).monotone.strictMono_of_injective
        aux_archimedeanClassOrderHom_injective).le_iff_le.mp h

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)
H : Subgroup G
x : G
⊢ x ∈
      (fun Φ ↦ (monoidHomMonoidHomEquiv G M).mapSubgroup (domRestrictHom (OrderDual.ofDual Φ) Mˣ).ker)
        ((fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker) H) ↔
    x ∈ H

Tactic:
rw [MulEquiv.coe_mapSubgroup, Subgroup.mem_map_equiv, MonoidHom.mem_ker]

Goal state after:
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
x : G
⊢ (domRestrictHom (OrderDual.ofDual ((fun H ↦ OrderDual.toDual (domRestrictHom H Mˣ).ker) H)) Mˣ)
        ((monoidHomMonoidHomEquiv G M).symm x) =
      1 ↔
    x ∈ H
Module: Mathlib.GroupTheory.Transfer

Goal state before:
pp: case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
⊢ g ^ H.index ∈ H

Tactic:
replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
      (congr_arg (· ∈ H) (key k g₀ hk)).mp hk

Goal state after:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
hH : ¬H.index = 0
this : Fintype (G ⧸ H) := fintypeOfIndexNeZero hH
key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H
⊢ g ^ H.index ∈ H
Module: Mathlib.GroupTheory.Schreier

Goal state before:
pp: case neg
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite ↑(commutatorSet G)
hG : ¬(center G).index = 0
this✝¹ : (center G).FiniteIndex
h1 : (center G).relIndex (_root_.commutator G) ∣ (center G).index
this✝ : ((center G).subgroupOf (_root_.commutator G)).FiniteIndex
h2 :
  Group.rank ↥((center G).subgroupOf (_root_.commutator G)) ≤
    ((center G).subgroupOf (_root_.commutator G)).index * Group.rank ↥(_root_.commutator G)
h3 :
  (center G).relIndex (_root_.commutator G) * Group.rank ↥(_root_.commutator G) ≤
    (center G).index * Nat.card ↑(commutatorSet G)
g : ↥((center G).subgroupOf (_root_.commutator G))
this : ↑↑g ∈ (MonoidHom.transferCenterPow G).ker
⊢ g ^ (center G).index = 1

Tactic:
simpa only [MonoidHom.mem_ker, Subtype.ext_iff] using! this

Goal state after:
Module: Mathlib.GroupTheory.FinitelyPresentedGroup

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
hG : IsFinitelyPresented G
f : G →* H
hf_surj : Function.Surjective ⇑f
hf_ker : f.ker.IsFinitelyNormallyGenerated
n : ℕ
φ : FreeGroup (Fin n) →* G
hφ_surj : Function.Surjective ⇑φ
hφ_ker : φ.ker.IsFinitelyNormallyGenerated
⊢ (f.comp φ).ker.IsFinitelyNormallyGenerated

Tactic:
← MonoidHom.comap_ker

Goal state after:
G : Type u_1
H : Type u_2
inst✝¹ : Group G
inst✝ : Group H
hG : IsFinitelyPresented G
f : G →* H
hf_surj : Function.Surjective ⇑f
hf_ker : f.ker.IsFinitelyNormallyGenerated
n : ℕ
φ : FreeGroup (Fin n) →* G
hφ_surj : Function.Surjective ⇑φ
hφ_ker : φ.ker.IsFinitelyNormallyGenerated
⊢ (Subgroup.comap φ f.ker).IsFinitelyNormallyGenerated
Module: Mathlib.GroupTheory.Frattini

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal

Tactic:
intro p

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : Finite G
p : ℕ
⊢ Fact (Nat.Prime p) → ∀ (P : Sylow p ↥(frattini G)), (↑P).Normal
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ : G
⊢ x✝ ∈ N.upperCentralSeriesStep ↔ (mk' N) x✝ ∈ center (G ⧸ N)

Tactic:
mem_center_iff,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
x✝ : G
⊢ x✝ ∈ N.upperCentralSeriesStep ↔ ∀ (g : G ⧸ N), g * (mk' N) x✝ = (mk' N) x✝ * g
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
n : ℕ
x : G
hx : x ∈ H (n + 1)
⊢ ∀ (y : G), ⁅x, y⁆ ∈ upperCentralSeries G n

Tactic:
exact fun y => ascending_central_series_le_upper H hH n (hH.2 x n hx y)

Goal state after:
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → Group.IsNilpotent G

Tactic:
rintro ⟨n, H, hH, hn⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ Group.IsNilpotent G
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: case left
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := fun e ↦ ⟨fun b ↦ f ⟨e, ⋯⟩, IsFreeGroup.of e⟩
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
e : IsFreeGroup.Generators G
x✝ : A
⊢ ((curry E) (IsFreeGroup.of e)).left x✝ = (f' e).left x✝

pp: case right
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := ⋯
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
e : IsFreeGroup.Generators G
⊢ ((curry E) (IsFreeGroup.of e)).right = (f' e).right

Tactic:
· convert! hE _ _ _
          rfl

Goal state after:
case right
G A : Type u
inst✝³ : Group G
inst✝² : IsFreeGroup G
inst✝¹ : MulAction G A
X : Type u
inst✝ : Group X
f : Labelling (Generators (ActionCategory G A)) X
f' : IsFreeGroup.Generators G → (A → X) ⋊[mulAutArrow] G := ⋯
F' : G →* (A → X) ⋊[mulAutArrow] G
hF' : ∀ (a : IsFreeGroup.Generators G), F' (IsFreeGroup.of a) = f' a
uF' :
  ∀ (y : G →* (A → X) ⋊[mulAutArrow] G),
    (fun F ↦ ∀ (a : IsFreeGroup.Generators G), F (IsFreeGroup.of a) = f' a) y → y = F'
E : ActionCategory G A ⥤ CategoryTheory.SingleObj X
hE : ∀ (a b : Generators (ActionCategory G A)) (g : a ⟶ b), E.map ⟨IsFreeGroup.of ↑g, ⋯⟩ = f g
e : IsFreeGroup.Generators G
⊢ ((curry E) (IsFreeGroup.of e)).right = (f' e).right
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mp
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤) → ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥

Tactic:
rintro ⟨n, H, hH, hn⟩

Goal state after:
case mp
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsAscendingCentralSeries H
hn : H n = ⊤
⊢ ∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case mpr
G : Type u_1
inst✝ : Group G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤

Tactic:
rintro ⟨n, H, hH, hn⟩

Goal state after:
case mpr
G : Type u_1
inst✝ : Group G
n : ℕ
H : ℕ → Subgroup G
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ∃ n H, IsAscendingCentralSeries H ∧ H n = ⊤
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: case refine_1
G : Type u_1
inst✝ : Group G
S : Subgroup G
⊢ (∃ n H, IsDescendingCentralSeries H ∧ H n = ⊥) → ∃ n, S.lowerCentralSeries n = ⊥

Tactic:
rintro ⟨n, H, hH, hn⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
S : Subgroup G
n : ℕ
H : ℕ → Subgroup ↥S
hH : IsDescendingCentralSeries H
hn : H n = ⊥
⊢ ∃ n, S.lowerCentralSeries n = ⊥
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = nilpotencyClass G

Tactic:
rw [← least_descending_central_series_length_eq_nilpotencyClass]

Goal state after:
G : Type u_1
inst✝ : Group G
hG : Group.IsNilpotent G
⊢ Nat.find ⋯ = Nat.find ⋯
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
inst✝ : Group G
n : ℕ
⊢ ⊤.lowerCentralSeries n = ⊥ ↔ upperCentralSeries G n = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝ : Group G
n : ℕ
h : ⊤.lowerCentralSeries n = ⊥
⊢ upperCentralSeries G n = ⊤

case refine_2
G : Type u_1
inst✝ : Group G
n : ℕ
h : upperCentralSeries G n = ⊤
⊢ ⊤.lowerCentralSeries n = ⊥
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'
⊢ nilpotencyClass G' ≤ nilpotencyClass G

Tactic:
rw [nilpotencyClass_def, nilpotencyClass_def]

Goal state after:
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'
⊢ Nat.find ⋯ ≤ Nat.find ⋯
Module: Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Goal state before:
pp: G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ Nonempty (Path (symgen a) (symgen b))

Tactic:
rw [← @WeaklyConnectedComponent.eq (Generators G), eq_comm, ← FreeGroup.of_injective.eq_iff, ←
    mul_inv_eq_one]

Goal state after:
G : Type u
inst✝¹ : Groupoid G
inst✝ : IsFreeGroupoid G
a b : G
p : a ⟶ b
⊢ FreeGroup.of (WeaklyConnectedComponent.mk (symgen b)) * (FreeGroup.of (WeaklyConnectedComponent.mk (symgen a)))⁻¹ = 1
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ ⊤.lowerCentralSeries n ≤ pi Set.univ fun i ↦ ⊤.lowerCentralSeries n

Tactic:
rw [← pi_top (I := Set.univ)]

Goal state after:
η : Type u_2
Gs : η → Type u_3
inst✝ : (i : η) → Group (Gs i)
n : ℕ
⊢ (pi Set.univ fun i ↦ ⊤).lowerCentralSeries n ≤ pi Set.univ fun i ↦ ⊤.lowerCentralSeries n
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ Nat.card (G ⧸ center G) < Nat.card (G ⧸ center G) * Nat.card ↥(center G)

Tactic:
apply lt_mul_of_one_lt_right Nat.card_pos

Goal state after:
G✝ : Type u_1
inst✝² : Finite G✝
p : ℕ
hp : Fact (Nat.Prime p)
G : Type u_1
inst✝¹ : Finite G
inst✝ : Nontrivial G
ih : ∀ (β : Type u_1) [Finite β], Nat.card β < Nat.card G → ∀ [hG : Group β], IsPGroup p β → Group.IsNilpotent β
hG : Group G
h : IsPGroup p G
⊢ 1 < Nat.card ↥(center G)
Module: Mathlib.GroupTheory.Nilpotent

Goal state before:
pp: G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
⊢ ∀ (p : ↥ps) (P : Sylow (↑p) G), IsNilpotent ↥↑P

Tactic:
intro p

Goal state after:
G : Type u_1
hG : Group G
inst✝ : Finite G
e : ((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G
ps : Finset ℕ := (Nat.card G).primeFactors
p : ↥ps
⊢ ∀ (P : Sylow (↑p) G), IsNilpotent ↥↑P
Module: Mathlib.GroupTheory.GroupAction.Blocks

Goal state before:
pp: case inr.«1»
G : Type u_1
inst✝² : Group G
X : Type u_2
inst✝¹ : MulAction G X
inst✝ : IsPretransitive G X
B : Set X
hX : Finite X
hB : IsBlock G B
hB_ne : B.Nonempty
hB' : 1 < 2
key : B.ncard * 1 = Nat.card X
⊢ B = Set.univ

Tactic:
· rw [mul_one, ← Set.ncard_univ] at key
    rw [Set.eq_of_subset_of_ncard_le (Set.subset_univ B) key.ge]

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

Goal state before:
pp: α : 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π : π * σ * π⁻¹ = τ
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

Tactic:
rcases Int.units_eq_one_or (Perm.sign π) with h | h

Goal state after:
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
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩

case inr
α : 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
⊢ IsConj ⟨σ, hσ✝⟩ ⟨τ, hτ⟩
Module: Mathlib.GroupTheory.GroupAction.Primitive

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ b ∉ B

Tactic:
suffices B = {a} by rw [this]; rw [Set.mem_singleton_iff]; exact Ne.symm h

Goal state after:
G : Type u_1
X : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G X
inst✝ : IsPreprimitive G X
A : Set X
hfA : A.Finite
hA : A.Nonempty
hA' : A ≠ Set.univ
a b : X
h : a ≠ b
B : Set X := ⋂ g, ⋂ (_ : a ∈ g • A), g • A
⊢ B = {a}
Module: Mathlib.GroupTheory.SpecificGroups.Alternating

Goal state before:
pp: c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ g'.cycleType.lcm ∣ 2

Tactic:
Multiset.lcm_dvd

Goal state after:
c g' : Perm (Fin 5)
h : 3 ∈ (c * g').cycleType
hd : c.Disjoint g'
left✝ : c.IsCycle
h3 : c.support.card = 3
⊢ ∀ b ∈ g'.cycleType, b ∣ 2
Module: Mathlib.GroupTheory.GroupAction.MultipleTransitivity

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
m p : ℕ
inst✝ : IsMultiplyPretransitive G α (m + p)
hmn : m ≤ m + p
hα : ↑(m + p) ≤ ENat.card α
⊢ IsMultiplyPretransitive G α m

Tactic:
exact IsPretransitive.of_surjective_map
    (f := embMap G α (castAddEmb p))
    (Fin.Embedding.restrictSurjective_of_add_le_ENatCard hα) inferInstance

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 α
m n : ℕ
Hn : IsMultiplyPretransitive G α n
s : Set α
inst✝ : Finite ↑s
hmn : s.ncard + m = n
x y : Fin m ↪ ↥(ofFixingSubgroup G s)
⊢ ∃ g, g • x = y

Tactic:
by
    have : IsMultiplyPretransitive G α (s.ncard + m) := by rw [hmn]; infer_instance
    have Hs : Nonempty (Fin (s.ncard) ≃ s) :=
      Finite.card_eq.mp (by simp [Nat.card_coe_set_eq])
    set x' := ofFixingSubgroup.append x with hx
    set y' := ofFixingSubgroup.append y with hy
    obtain ⟨g, hg⟩ := exists_smul_eq G x' y'
    suffices g ∈ fixingSubgroup G s by
      use ⟨g, this⟩
      ext i
      rw [smul_apply, SetLike.val_smul, Subgroup.mk_smul]
      simp [← ofFixingSubgroup.append_right, ← smul_apply, ← hx, ← hy, hg]
    intro a
    set i := (Classical.choice Hs).symm a
    have ha : (Classical.choice Hs) i = a := by simp [i]
    rw [← ha]
    nth_rewrite 1 [← ofFixingSubgroup.append_left x i]
    rw [← ofFixingSubgroup.append_left y i, ← hy, ← hg, smul_apply, ← hx]

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

Goal state before:
pp: case mpr
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 α := ⋯
hs' : s' = g • s
t : Set ↥(ofStabilizer M a) := ⋯
x : α
⊢ x ∈ insert a (Subtype.val '' t) → x ∈ s'

Tactic:
Set.mem_insert_iff

Goal state after:
case mpr
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'
x : α
⊢ x = a ∨ x ∈ Subtype.val '' t → x ∈ s'
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
⊢ φ g • y = y

Tactic:
suffices ∃ x ∈ s, y = f x by
        obtain ⟨x, hx, rfl⟩ := this
        rwa [← map_smulₛₗ, hg]

Goal state after:
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
⊢ ∃ x ∈ s, y = f x
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝³ : Group M
inst✝² : MulAction M α
s : Set α
inst✝¹ : Finite α
inst✝ : IsMultiplyPretransitive M α (s.ncard + 1)
G : Subgroup M
hG : stabilizer M s ≤ G
B : Set α
hBs : ¬B ⊆ s
hBsc : ¬B ⊆ sᶜ
hB : IsBlock (↥G) B
a : α
ha : a ∈ B
ha' : a ∈ s
b : α
hb : b ∈ B
hb' : b ∈ sᶜ
x : α
hx' : x ∈ sᶜ
⊢ ∃ k, k • b = x

Tactic:
suffices h : IsPretransitive (fixingSubgroup M s) (ofFixingSubgroup M s) by
      obtain ⟨k, hk⟩ := h.exists_smul_eq (⟨b, hb'⟩ : ofFixingSubgroup M s) ⟨x, hx'⟩
      rw [← Subtype.coe_inj, val_smul] at hk
      exact ⟨k, hk⟩
    -- Prove pretransitivity…
    rw [← is_one_pretransitive_iff]
    apply ofFixingSubgroup.isMultiplyPretransitive M s rfl

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

Goal state before:
pp: α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝² : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this✝¹ : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this✝ : sᶜ ⊆ B
this : sᶜ.ncard ≤ B.ncard
⊢ Nat.card α < B.ncard * 2

Tactic:
← Set.ncard_add_ncard_compl s

Goal state after:
α : Type u_2
inst✝ : Finite α
s : Set α
h0 : s.Nonempty
hα : s.ncard < sᶜ.ncard
h1 : sᶜ.Nonempty
this✝² : Fintype α
G : Subgroup (Perm α)
hG : stabilizer (Perm α) s < G
hG' : stabilizer (Perm α) sᶜ < G
g : Perm α
hg_swap : g.IsSwap
hg : g ∈ G
this✝¹ : IsPretransitive (↥G) α
B : Set α
hB : IsBlock (↥G) B
hB' : ¬B.Subsingleton
this✝ : sᶜ ⊆ B
this : sᶜ.ncard ≤ B.ncard
⊢ s.ncard + sᶜ.ncard < B.ncard * 2
Module: Mathlib.GroupTheory.Perm.MaximalSubgroups

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

Tactic:
apply MulAction.IsBlock.compl_subset_of_stabilizer_le_of_not_subset_of_not_subset_compl hG.le <;>
    grind

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

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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

case refine_2
α : Type u_2
inst✝² : DecidableEq α
G : Type u_3
inst✝¹ : AddGroup G
inst✝ : AddAction G α
n : ℕ
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : AddAction.toPerm g = 1
⊢ AddAction.toPerm g = 1
Module: Mathlib.GroupTheory.GroupAction.SubMulAction.Combination

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

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Goal state after:
case refine_1
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : toPerm g = 1
⊢ toPerm g = 1

case refine_2
G : Type u_1
inst✝² : Group G
α : Type u_2
inst✝¹ : MulAction G α
n : ℕ
inst✝ : DecidableEq α
hn : 1 ≤ n
hα : ↑n < ENat.card α
g : G
h : toPerm g = 1
⊢ toPerm g = 1
Module: Mathlib.GroupTheory.MonoidLocalization.UniqueFactorization

Goal state before:
pp: case inl
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 ∣ s * (m₁, s₁).1
this : f m ∣ n₁
⊢ f m ∣ n₁ ∨ f m ∣ n₂

Tactic:
exact .inl this

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

Goal state before:
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:
intro i _
      apply congr_arg
      apply Fintype.card_congr
      apply Equiv.subtypeEquiv (Equiv.refl α)
      intro a
      rw [refl_apply, ← Subtype.coe_inj]
      simp only [φ, Set.val_codRestrict_apply]

Goal state after: