awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
inl : (Nat.card α).factorial ≤ 2 * Nat.card.{u_1} ↥G
⊢ G.index ≤ 2

Tactic:
rw [← Nat.mul_le_mul_right_iff (k := Nat.card G) (Nat.card_pos),
      Subgroup.index_mul_card, Nat.card_perm]

Premises used: Nat.card_pos, Nat.card_perm, Subgroup.index_mul_card, Nat.mul_le_mul_right_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
inl : Nat.factorial 3 ≤ 2 * Nat.card.{u_1} ↥G
⊢ (Nat.card α).factorial ≤ 2 * Nat.card.{u_1} ↥G

Tactic:
apply le_trans (Nat.factorial_le hα4)

Premises used: Nat.factorial_le, le_trans
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ Nat.factorial 3 = HMul.hMul (α := ℕ) 2 3

Tactic:
simp [Nat.factorial]

Premises used: Nat.factorial
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
inl : 3 ≤ Nat.card.{u_1} ↥G
⊢ HMul.hMul (α := ℕ) 2 3 ≤ 2 * Nat.card.{u_1} ↥G

Tactic:
simp only [mul_le_mul_iff_right₀, Nat.succ_pos]

Premises used: Nat.succ_pos, mul_le_mul_iff_right₀
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
inl : 3 ∣ Nat.card.{u_1} ↥G
⊢ 3 ≤ Nat.card.{u_1} ↥G

Tactic:
apply Nat.le_of_dvd Nat.card_pos

Premises used: Nat.card_pos, Nat.le_of_dvd
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
this : 3 = orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
rw : orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg) ∣ Fintype.card.{u_1} ↥G
⊢ 3 ∣ Nat.card.{u_1} ↥G

Tactic:
rw [this, Nat.card_eq_fintype_card]

Premises used: Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
this : 3 = orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
⊢ orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg) ∣ Fintype.card.{u_1} ↥G

Tactic:
orderOf_dvd_card

Premises used: orderOf_dvd_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
this : 3 = orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
⊢ orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg) ∣ Fintype.card.{u_1} ↥G

Tactic:
exact orderOf_dvd_card

Premises used: orderOf_dvd_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
inl : 3 = orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
⊢ 3 ∣ Nat.card.{u_1} ↥G

Tactic:
suffices 3 = orderOf (⟨g, hg⟩ : G) by
      rw [this, Nat.card_eq_fintype_card]
      exact orderOf_dvd_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≤ 3
⊢ 3 = orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)

Tactic:
simp only [orderOf_mk, h3g.orderOf]

Premises used: Subgroup.orderOf_mk, Equiv.Perm.IsThreeCycle.orderOf
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
inr : ∀ (n : ℕ) (hn : Nat.card α = n + 4), alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G

Tactic:
obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα4

Premises used: Nat.exists_eq_add_of_le'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
inr : IsMultiplyPretransitive (↥G) α (Nat.card α - 2)
⊢ alternatingGroup α ≤ G

Tactic:
apply IsMultiplyPretransitive.alternatingGroup_le

Premises used: IsMultiplyPretransitive.alternatingGroup_le
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
inr : IsMultiplyPreprimitive (↥G) α (Nat.card α - 2)
⊢ IsMultiplyPretransitive (↥G) α (Nat.card α - 2)

Tactic:
suffices IsMultiplyPreprimitive G α (Nat.card α - 2) from
    IsMultiplyPreprimitive.isMultiplyPretransitive ..
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ Nat.card α - 2 = n + 2

Tactic:
grind
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
inr : IsMultiplyPreprimitive (↥G) α (n + 2)
⊢ IsMultiplyPreprimitive (↥G) α (Nat.card α - 2)

Tactic:
rw [show Nat.card α - 2 = n + 2 by grind]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
inr : (↑g.support : Set α)ᶜ.ncard = n + 1
inr₁ : n + 2 < Nat.card α
inr₂ : IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
⊢ IsMultiplyPreprimitive (↥G) α (n + 2)

Tactic:
apply hG.isMultiplyPreprimitive (s := (g.supportᶜ : Set α))

Premises used: MulAction.IsPreprimitive.isMultiplyPreprimitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
inr : (↑g.support : Set α).ncard + (↑g.support : Set α)ᶜ.ncard = (↑g.support : Set α).ncard + (n + 1)
inr₁ : ℕ
⊢ (↑g.support : Set α)ᶜ.ncard = n + 1

Tactic:
apply Nat.add_left_cancel

Premises used: Nat.add_left_cancel
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ n + 2 < Nat.card α

Tactic:
grind
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
⊢ IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)

Tactic:
have := isPretransitive_of_isCycle_mem h3g.isCycle hg
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this :
  IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
inr : Nat.Prime (Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ))
⊢ IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)

Tactic:
apply IsPreprimitive.of_prime_card

Premises used: MulAction.IsPreprimitive.of_prime_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this :
  IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
⊢ Nat.Prime 3

Tactic:
Nat.prime_three

Premises used: Nat.prime_three
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this :
  IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
h : Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) = 3
⊢ Nat.Prime (Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ))

Tactic:
convert! Nat.prime_three

Premises used: Nat.prime_three
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this :
  IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
h :
  Finset.card.{u_1} (α := α)
      {x : α |
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
    g.support.card
⊢ Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) = 3

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← h3g.card_support]

Premises used: Equiv.Perm.IsThreeCycle.card_support, Fintype.card_subtype, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this :
  IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
h :
  {x : α |
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
    g.support
⊢ Finset.card.{u_1} (α := α)
      {x : α |
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
    g.support.card

Tactic:
apply congr_arg

Premises used: congr_arg
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this :
  IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
h :
  ∀ (x : α),
    Membership.mem (γ := Finset α)
        {x : α |
          Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
            (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x}
        x ↔
      x ∈ g.support
⊢ {x : α |
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
    g.support

Tactic:
ext x
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
hG : IsPreprimitive (↥G) α
g : Perm α
h3g : g.IsThreeCycle
hg : g ∈ G
hα4 : Nat.card α ≥ 4
n : ℕ
hn : Nat.card α = n + 4
this :
  IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
x : α
⊢ Membership.mem (γ := Finset α)
      {x : α |
        Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
          (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x}
      x ↔
    x ∈ g.support

Tactic:
simp [SubMulAction.mem_ofFixingSubgroup_iff]

Premises used: SubMulAction.mem_ofFixingSubgroup_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup.{u_1, u_2} G (α := α) ∅) ↥(ofFixingSubgroup G ∅) ↔ IsPreprimitive G α

Tactic:
isPreprimitive_congr
    of_fixingSubgroupEmpty_mapScalars_surjective
    ofFixingSubgroupEmpty_equivariantMap_bijective

Premises used: Set.Mem, SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective, SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective, MulAction.isPreprimitive_congr
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
s : Set α
g : G
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G s) ↥(ofFixingSubgroup G s) ↔
    IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup G (g • s)) ↥(ofFixingSubgroup G (g • s))

Tactic:
isPreprimitive_congr
    (fixingSubgroupEquivFixingSubgroup rfl).surjective
    conjMap_ofFixingSubgroup_bijective

Premises used: Set.Mem, MulEquiv.surjective, SubMulAction.fixingSubgroupEquivFixingSubgroup, MulAction.isPreprimitive_congr, rfl, SubMulAction.conjMap_ofFixingSubgroup_bijective
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
G : Type u_1
inst : Group G
α : Type u_2
inst_1 : MulAction G α
a : α
t : Set ↥(ofStabilizer G a)
⊢ IsPreprimitive.{u_1, u_2}
      ↥(fixingSubgroup G
          (insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
              t)))
      ↥(ofFixingSubgroup G
          (insert a
            (Subtype.val (p := fun (x : α) ↦
                Membership.mem (γ := SubMulAction.{u_1, u_2} (↥(stabilizer G a)) α) (ofStabilizer G a) x) ''
              t))) ↔
    IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer G a)) t) ↥(ofFixingSubgroup (↥(stabilizer G a)) t)

Tactic:
isPreprimitive_congr (fixingSubgroupInsertEquiv a t).surjective
    ofFixingSubgroup_insert_map_bijective

Premises used: SubMulAction.fixingSubgroupInsertEquiv, Set.Mem, MulEquiv.surjective, MulAction.isPreprimitive_congr, 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 α
n : ℕ
inst_2 : IsMultiplyPreprimitive M α n
⊢ IsMultiplyPretransitive M α n

Tactic:
IsMultiplyPreprimitive.isMultiplyPretransitive M α n

Premises used: MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
s : Set α
hs : s.encard + 1 = (↑0 : ℕ∞)
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
simp at hs
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
mp : IsMultiplyPreprimitive M α 1 → IsPreprimitive M α
mpr : IsPreprimitive M α → IsMultiplyPreprimitive M α 1
⊢ IsMultiplyPreprimitive M α 1 ↔ IsPreprimitive M α

Tactic:
constructor
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
H1 : IsMultiplyPreprimitive M α 1
mp : IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup.{u_1, u_2} M (α := α) ∅) ↥(ofFixingSubgroup M ∅)
⊢ IsPreprimitive M α

Tactic:
rw [← isPreprimitive_of_fixingSubgroup_empty_iff]

Premises used: MulAction.isPreprimitive_of_fixingSubgroup_empty_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
H1 : IsMultiplyPreprimitive M α 1
⊢ Set.encard.{u_2} (α := α) ∅ + 1 = (↑1 : ℕ∞)

Tactic:
simp
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
H1 : IsMultiplyPreprimitive M α 1
⊢ IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup.{u_1, u_2} M (α := α) ∅) ↥(ofFixingSubgroup M ∅)

Tactic:
apply H1.isPreprimitive_ofFixingSubgroup (by simp)

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 α
h : IsPreprimitive M α
mpr :
  IsMultiplyPretransitive M α 1 ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑1 : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsMultiplyPreprimitive M α 1

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 α
h : IsPreprimitive M α
mpr : IsMultiplyPretransitive M α 1
mpr₁ :
  ∀ {s : Set α} (hs : s.encard + 1 = (↑1 : ℕ∞)), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)
⊢ IsMultiplyPretransitive M α 1 ∧
    ∀ {s : Set α} (hs : s.encard + 1 = (↑1 : ℕ∞)),
      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 α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1

Tactic:
is_one_pretransitive_iff.mpr h.toIsPretransitive

Premises used: Iff.mpr, MulAction.IsPreprimitive.toIsPretransitive, MulAction.is_one_pretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
h : IsPreprimitive M α
⊢ IsMultiplyPretransitive M α 1

Tactic:
exact is_one_pretransitive_iff.mpr h.toIsPretransitive

Premises used: Iff.mpr, MulAction.IsPreprimitive.toIsPretransitive, MulAction.is_one_pretransitive_iff
-- Module: Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
Goal:
M : Type u_1
α : Type u_2
inst : Group M
inst_1 : MulAction M α
h : IsPreprimitive M α
⊢ ∀ {s : Set α} (hs : s.encard + 1 = (↑1 : ℕ∞)), IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup M s) ↥(ofFixingSubgroup M s)

Tactic:
simpa using isPreprimitive_of_fixingSubgroup_empty_iff.mpr h

Premises used: MulAction.isPreprimitive_of_fixingSubgroup_empty_iff, Iff.mpr
-- 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
inl : ∀ (h0 : n < 1), IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
inr : ∀ (h1 : n ≥ 1), IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
rcases Nat.lt_or_ge n 1 with h0 | h1

Premises used: Nat.lt_or_ge, OfNat.ofNat
-- 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
h0 : n < 1
⊢ n = 0

Tactic:
rw [Nat.lt_one_iff] at h0

Premises used: Nat.lt_one_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 : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h0 : n = 0
inl : IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) 0
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
rw [h0]
-- 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
h0 : n = 0
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) 0

Tactic:
apply is_zero_preprimitive

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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
inr :
  IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n ∧
    ∀ {s : Set ↥(ofStabilizer M a)} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
⊢ IsMultiplyPreprimitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) 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 α
inst_2 : IsPretransitive M α
n : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
inr : IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n
inr₁ :
  ∀ {s : Set ↥(ofStabilizer M a)} (hs : s.encard + 1 = (↑n : ℕ∞)),
    IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) s)
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n ∧
    ∀ {s : Set ↥(ofStabilizer M a)} (hs : s.encard + 1 = (↑n : ℕ∞)),
      IsPreprimitive.{u_1, u_2} ↥(fixingSubgroup (↥(stabilizer M a)) s) ↥(ofFixingSubgroup (↥(stabilizer M a)) 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 : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
inr : IsMultiplyPretransitive M α n.succ
⊢ IsMultiplyPretransitive.{u_1, u_2} (↥(stabilizer M a)) (↥(ofStabilizer M a)) n

Tactic:
rw [← ofStabilizer.isMultiplyPretransitive]

Premises used: 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 : ℕ
a : α
inst_3 : IsMultiplyPreprimitive M α n.succ
h1 : n ≥ 1
⊢ IsMultiplyPretransitive M α n.succ

Tactic:
IsMultiplyPreprimitive.isMultiplyPretransitive M α n.succ

Premises used: MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive, 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
⊢ IsMultiplyPretransitive M α n.succ

Tactic:
exact IsMultiplyPreprimitive.isMultiplyPretransitive M α n.succ

Premises used: MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive, Nat.succ