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 : ℕ
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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
mpr : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) t) ↥(ofFixingSubgroup (↥(stabilizer M a)) t)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s') ↥(ofFixingSubgroup M s')

Tactic:
rw [hst, isPreprimitive_fixingSubgroup_insert_iff]

Premises used: MulAction.isPreprimitive_fixingSubgroup_insert_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
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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
mpr : t.encard + 1 = (↑n : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) t) ↥(ofFixingSubgroup (↥(stabilizer M a)) t)

Tactic:
apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n

Premises used: MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup
-- 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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
mpr : Eq (α := ℕ∞) ((fun (x : ℕ∞) ↦ x + 1) (t.encard + 1)) ((fun (x : ℕ∞) ↦ x + 1) (↑n : ℕ∞))
⊢ t.encard + 1 = (↑n : ℕ∞)

Tactic:
apply ENat.add_left_injective_of_ne_top ENat.one_ne_top

Premises used: ENat.one_ne_top, ENat.add_left_injective_of_ne_top
-- 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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
mpr : t.encard + (↑1 : ℕ∞) + (↑1 : ℕ∞) = s.encard + 1
⊢ t.encard + 1 + 1 = HAdd.hAdd (α := ℕ∞) (↑n : ℕ∞) 1

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, ← hs]

Premises used: Nat.cast_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 : ℕ∞)
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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
apply : t.encard + (↑1 : ℕ∞) = s.encard
⊢ t.encard + (↑1 : ℕ∞) + (↑1 : ℕ∞) = s.encard + 1

Tactic:
apply congr_arg₂ _ _ rfl

Premises used: rfl, congr_arg₂
-- 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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ s = g⁻¹ • s'

Tactic:
simp [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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
rw :
  t.encard + (↑1 : ℕ∞) =
    (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)).encard
⊢ t.encard + (↑1 : ℕ∞) = s.encard

Tactic:
rw [show s = g⁻¹ • s' from by simp [hs'],
        ← Set.image_smul, (MulAction.injective g⁻¹).encard_image, hst]

Premises used: Set.image_smul, Function.Injective.encard_image, Inv.inv, MulAction.injective
-- 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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
rw :
  a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
      t
⊢ t.encard + (↑1 : ℕ∞) =
    (insert a
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
          t)).encard

Tactic:
rw [Set.encard_insert_of_notMem, Subtype.coe_injective.encard_image, ENat.coe_one]

Premises used: ENat.coe_one, 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 : ℕ
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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
      t

Tactic:
notMem_val_image M t

Premises used: SubMulAction.notMem_val_image
-- 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'
hst :
  s' =
    insert a
      (Subtype.val (p := fun (x : α) ↦
          Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
        t)
⊢ a ∉
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer M a)) α) (ofStabilizer M a) x) ''
      t

Tactic:
exact notMem_val_image M t

Premises used: SubMulAction.notMem_val_image
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(fixingSubgroup M s)) (↥(ofFixingSubgroup M s)) m

Tactic:
apply ofFixingSubgroup.isMultiplyPretransitive _ s hs

Premises used: SubMulAction.ofFixingSubgroup.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
⊢ t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'

Tactic:
have htt' : t = Subtype.val ⁻¹' t' :=
      (Set.preimage_image_eq _ Subtype.coe_injective).symm
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
rw :
  IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t'))
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t'))
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(fixingSubgroup M s)) t) ↥(ofFixingSubgroup (↥(fixingSubgroup M s)) t)

Tactic:
rw [htt']
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
this : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (s ∪ t')) ↥(ofFixingSubgroup M (s ∪ t'))
⊢ IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t'))
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t'))

Tactic:
apply IsPreprimitive.of_surjective map_ofFixingSubgroupUnion_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 α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
suffices : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (s ∪ t')) ↥(ofFixingSubgroup M (s ∪ t'))
⊢ IsPreprimitive.{u_1, u_2}
    ↥(fixingSubgroup ↥(fixingSubgroup M s) (α := ↥(ofFixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t'))
    ↥(ofFixingSubgroup (↥(fixingSubgroup M s))
        (Subtype.val (p := fun (x : α) ↦
            Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
          t'))

Tactic:
suffices IsPreprimitive (fixingSubgroup M (s ∪ t')) (ofFixingSubgroup M (s ∪ t')) by
      apply IsPreprimitive.of_surjective map_ofFixingSubgroupUnion_bijective.surjective
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
apply : (s ∪ t').encard + 1 = (↑n : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M (s ∪ t')) ↥(ofFixingSubgroup M (s ∪ t'))

Tactic:
apply IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup _ n

Premises used: MulAction.IsMultiplyPreprimitive.isPreprimitive_ofFixingSubgroup
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
rw : s.encard + t'.encard + 1 = (↑n : ℕ∞)
rw₁ : Disjoint s t'
⊢ (s ∪ t').encard + 1 = (↑n : ℕ∞)

Tactic:
rw [Set.encard_union_eq _]

Premises used: Set.encard_union_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
rw : s.Finite
⊢ s.encard + t'.encard + 1 = (↑n : ℕ∞)

Tactic:
rw [Subtype.coe_injective.encard_image, add_assoc, ht,
        ← hs, Nat.cast_add, Set.Finite.cast_ncard_eq]

Premises used: add_assoc, Subtype.coe_injective, Nat.cast_add, Function.Injective.encard_image, Set.Finite.cast_ncard_eq
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
⊢ s.Finite

Tactic:
Set.toFinite s

Premises used: Set.toFinite
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
⊢ s.Finite

Tactic:
exact Set.toFinite s

Premises used: Set.toFinite
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
m n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
s : Set α
inst_3 : Finite.{u_2 + 1} (↑s : Type u_2)
hs : s.ncard + m = n
t : Set ↥(ofFixingSubgroup M s)
ht : t.encard + 1 = (↑m : ℕ∞)
t' : Set α :=
  Subtype.val (p := fun (x : α) ↦
      Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ''
    t
htt' :
  t =
    Subtype.val (p := fun (x : α) ↦
        Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(fixingSubgroup M s)) α) (ofFixingSubgroup M s) x) ⁻¹'
      t'
⊢ Disjoint s t'

Tactic:
apply disjoint_val_image

Premises used: SubMulAction.disjoint_val_image
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
inl : ∀ (hn : n = 0), IsMultiplyPreprimitive M α n
inr : ∀ (hn : n > 0), IsMultiplyPreprimitive M α n
⊢ IsMultiplyPreprimitive M α n

Tactic:
rcases Nat.eq_zero_or_pos n with hn | hn

Premises used: Nat.eq_zero_or_pos
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n = 0
inl : IsMultiplyPreprimitive M α 0
⊢ IsMultiplyPreprimitive M α n

Tactic:
rw [hn]
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n = 0
⊢ IsMultiplyPreprimitive M α 0

Tactic:
is_zero_preprimitive M α

Premises used: MulAction.is_zero_preprimitive
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n = 0
⊢ IsMultiplyPreprimitive M α 0

Tactic:
exact is_zero_preprimitive M α

Premises used: MulAction.is_zero_preprimitive
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
inr :
  IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsMultiplyPreprimitive M α n

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 α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
inr : IsMultiplyPretransitive M α n
inr₁ :
  ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsMultiplyPretransitive M α n ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑n : ℕ∞)),
      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 α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
⊢ IsMultiplyPretransitive M α n

Tactic:
isMultiplyPretransitive_of_le' (Nat.le_succ n) hα

Premises used: Nat.le_succ, MulAction.isMultiplyPretransitive_of_le'
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
⊢ IsMultiplyPretransitive M α n

Tactic:
exact isMultiplyPretransitive_of_le' (Nat.le_succ n) hα

Premises used: Nat.le_succ, MulAction.isMultiplyPretransitive_of_le'
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
n : ℕ
hα : (↑n.succ : ℕ∞) ≤ ENat.card α
inst_2 : IsMultiplyPretransitive M α n.succ
hn : n > 0
s : Set α
hs : s.encard + 1 = (↑n : ℕ∞)
inr : ∀ (m : ℕ) (hm : n = Nat.succ 0 + m), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
obtain ⟨m, hm⟩ := Nat.exists_eq_add_of_le hn

Premises used: Nat.exists_eq_add_of_le