awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
apply :
  (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)).encard +
      1 =
    (↑n.succ : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))
    ↥(ofFixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))

Tactic:
apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup M n.succ

Premises used: MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup, Nat.succ
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
rw :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
      s
⊢ (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)).encard +
      1 =
    (↑n.succ : ℕ∞)

Tactic:
rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, hs, Nat.cast_succ]

Premises used: Nat.cast_succ, Subtype.coe_injective, Function.Injective.encard_image, Set.encard_insert_of_notMem
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
⊢ a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
      s

Tactic:
aesop
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))
    ↥(ofFixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))

Tactic:
have : IsPreprimitive ↥(fixingSubgroup M (insert a (Subtype.val '' s)))
      ↥(ofFixingSubgroup M (insert a (Subtype.val '' s))) := by
      apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup M n.succ
      rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, hs, Nat.cast_succ]
      aesop
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
this :
  IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))
    ↥(ofFixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)

Tactic:
IsPreprimitive.of_surjective ofFixingSubgroup_insert_map_bijective.surjective

Premises used: MulAction.IsPreprimitive.of_surjective, Set.Mem, Function.Bijective.surjective, SubMulAction.ofFixingSubgroup_insert_map_bijective
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
s : Set ↥(ofStabilizer M a)
hs : s.encard + 1 = (↑n : ℕ∞)
this :
  IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))
    ↥(ofFixingSubgroup M
        (insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            s)))
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)

Tactic:
exact IsPreprimitive.of_surjective ofFixingSubgroup_insert_map_bijective.surjective

Premises used: MulAction.IsPreprimitive.of_surjective
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
mp : IsMultiplyPreprimitive M α n.succ → IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
mpr : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n → IsMultiplyPreprimitive M α n.succ
⊢ IsMultiplyPreprimitive M α n.succ ↔ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
⊢ IsMultiplyPreprimitive M α n.succ → IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
apply isMultiplyPreprimitive_ofStabilizer

Premises used: MulAction.isMultiplyPreprimitive_ofStabilizer
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
mpr :
  IsMultiplyPretransitive M α n.succ ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n.succ : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsMultiplyPreprimitive M α n.succ

Tactic:
rw [isMultiplyPreprimitive_iff]

Premises used: MulAction.isMultiplyPreprimitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
mpr : IsMultiplyPretransitive M α n.succ
mpr₁ :
  ∀ {s : Set α} (hs : s.encard + 1 = (↑n.succ : ℕ∞)),
    IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsMultiplyPretransitive M α n.succ ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n.succ : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ IsMultiplyPretransitive M α n.succ

Tactic:
ofStabilizer.isMultiplyPretransitive.mpr H.isMultiplyPretransitive

Premises used: Iff.mpr, MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive, SubMulAction.ofStabilizer.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ IsMultiplyPretransitive M α n.succ

Tactic:
exact ofStabilizer.isMultiplyPretransitive.mpr H.isMultiplyPretransitive

Premises used: Iff.mpr, MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive, SubMulAction.ofStabilizer.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
rw : s ≠ ∅
⊢ ∃ (b : α), b ∈ s

Tactic:
rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]

Premises used: Set.nonempty_def, Set.nonempty_iff_ne_empty
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
h : s = ∅
apply : n < 1
⊢ False

Tactic:
apply not_lt.mpr hn

Premises used: Iff.mpr, not_lt
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
h : s = ∅
⊢ 0 = n

Tactic:
rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs

Premises used: Nat.succ_inj, Set.encard_empty, Nat.cast_inj, zero_add, Nat.cast_one
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
h : s = ∅
hs₁ : 0 = n
⊢ s = ∅

Tactic:
rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs

Premises used: Nat.succ_inj, Set.encard_empty, Nat.cast_inj, zero_add, Nat.cast_one
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : 0 = n
h : s = ∅
⊢ n < 1

Tactic:
simp only [← hs, zero_lt_one]

Premises used: zero_lt_one
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
⊢ ∃ (b : α), b ∈ s

Tactic:
have : ∃ b : α, b ∈ s := by
        rw [← Set.nonempty_def, Set.nonempty_iff_ne_empty]
        intro h
        apply not_lt.mpr hn
        rw [h, Set.encard_empty, zero_add, ← Nat.cast_one, Nat.cast_inj, Nat.succ_inj] at hs
        simp only [← hs, zero_lt_one]
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
this : ∃ (b : α), b ∈ s
mpr : ∀ (b : α) (hb : b ∈ s), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
obtain ⟨b, hb⟩ := this
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
mpr : ∀ (g : M) (hg : g • b = a), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
obtain ⟨g, hg : g • b = a⟩ := exists_smul_eq M b a

Premises used: MulAction.exists_smul_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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
mpr : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (g • s)) ↥(ofFixingSubgroup M (g • s))
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
rw [isPreprimitive_ofFixingSubgroup_conj_iff (g := g)]

Premises used: MulAction.isPreprimitive_ofFixingSubgroup_conj_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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
mpr :
  let s' := g • s;
  ∀ (hs' : s' = g • s), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s') ↥(ofFixingSubgroup M s')
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (g • s)) ↥(ofFixingSubgroup M (g • s))

Tactic:
set s' := g • s with hs'
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
h :
  ∀ (x : α),
    x ∈ s' ↔
      x ∈
        insert a
          (Subtype.val (p := fun (x : α) ↦
              Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
            t)
⊢ s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
h :
  x ∈ s' →
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)
h₁ :
  x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t) →
    x ∈ s'
⊢ x ∈ s' ↔
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
hxs : x ∈ s'
pos :
  ∀ (hxa : x = a),
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)
neg :
  ∀ (hxa : ¬x = a),
    x ∈
      insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)
⊢ x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)

Tactic:
by_cases hxa : x = a
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
hxs : x ∈ s'
hxa : x = a
⊢ x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)

Tactic:
simp [hxa]
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
hxs : x ∈ s'
hxa : ¬x = a
simp : x ∈ s'
⊢ Subtype.mk (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) x hxa ∈
    t

Tactic:
simp only [t, Set.mem_preimage]

Premises used: Set.mem_preimage
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
hxs : x ∈ s'
hxa : ¬x = a
⊢ x ∈ s'

Tactic:
hxs
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
hxs : x ∈ s'
hxa : ¬x = a
⊢ x ∈ s'

Tactic:
exact hxs
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
x : α
hxs : x ∈ s'
hxa : ¬x = a
⊢ x ∈
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)

Tactic:
exact Set.mem_insert_of_mem _
              ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
s : Set α
hs : s.encard + 1 = (↑n.succ : ℕ∞)
b : α
hb : b ∈ s
g : M
s' : Set α := g • s
hs' : s' = g • s
x : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M x)) (↥(ofStabilizer M x)) n
hg : g • b = x
t : Set ↥(ofStabilizer M x) :=
  Subtype.val (p := fun (x_1 : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M x)) α) (ofStabilizer M x) x_1) ⁻¹'
    s'
⊢ x ∈ s'

Tactic:
simpa [s', ← hg]
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
y : ↥(ofStabilizer M a)
hy : y ∈ t
⊢ (↑y : α) ∈ s'

Tactic:
simpa only using hy
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
inst_2 : IsPretransitive M α
n : ℕ
hn : 1 ≤ n
a : α
H : IsMultiplyPreprimitive.{u_1, u_2} (↥(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 (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ⁻¹'
    s'
⊢ s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)

Tactic:
have hst : s' = insert a (Subtype.val '' t) := by
        ext x
        constructor
        · intro hxs
          by_cases hxa : x = a
          · simp [hxa]
          · exact Set.mem_insert_of_mem _
              ⟨⟨x, hxa⟩, by simp only [t, Set.mem_preimage]; exact hxs, rfl⟩
        · rw [Set.mem_insert_iff]
          rintro (⟨rfl⟩ | ⟨y, hy, rfl⟩)
          · simpa [s', ← hg]
          · simpa only using hy