awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
this :
  ∀ (x : α),
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x →
      ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
y : α
hy :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) y
k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk : x = k • a
k' : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
hk' : y = k' • a
h : (k' * k⁻¹) • k • a = y
h₁ : (k' * k⁻¹) • k • a = k' • a
h₂ : (k' * k⁻¹ * k) • a = k' • a
h₃ h₄ : k' • a = k' • a
⊢ (k' * k⁻¹) • x = y

Tactic:
rw [hk, hk', smul_smul, inv_mul_cancel_right]

Premises used: smul_smul, inv_mul_cancel_right
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
suffices :
  ∀ (x : α),
    Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x →
      ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
⊢ IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)

Tactic:
suffices ∀ x ∈ SubMulAction.ofFixingSubgroup G ((↑g.support : Set α)ᶜ),
      ∃ k : fixingSubgroup G ((↑g.support : Set α)ᶜ), x = k • a by
    rw [isPretransitive_iff]
    rintro ⟨x, hx⟩ ⟨y, hy⟩
    obtain ⟨k, hk⟩ := this x hx
    obtain ⟨k', hk'⟩ := this y hy
    use k' * k⁻¹
    rw [← SetLike.coe_eq_coe]
    simp only [SetLike.mk_smul_mk]
    rw [hk, hk', smul_smul, inv_mul_cancel_right]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
simp_rw : ∀ y ∈ (↑g.support : Set α)ᶜ, Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg • y = y
⊢ Membership.mem (γ := Subgroup ↥G) (fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)

Tactic:
simp_rw [mem_fixingSubgroup_iff G]

Premises used: Membership.mem, Subtype, mem_fixingSubgroup_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
y : α
hy : y ∈ (↑g.support : Set α)ᶜ
⊢ Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg • y = y

Tactic:
simpa only [Set.mem_compl_iff, Finset.mem_coe, notMem_support] using hy

Premises used: Equiv.Perm.notMem_support, Finset.mem_coe, Set.mem_compl_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
⊢ Membership.mem (γ := Subgroup ↥G) (fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)

Tactic:
have hg' : (⟨g, hg⟩ : ↥G) ∈ fixingSubgroup G ((↑g.support : Set α)ᶜ) := by
    simp_rw [mem_fixingSubgroup_iff G]
    intro y hy
    simpa only [Set.mem_compl_iff, Finset.mem_coe, notMem_support] using hy
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
hg' :
  Membership.mem (γ := Subgroup ↥G) (fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
g' : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) :=
  Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Subgroup ↥G) (fixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg) hg'
obtain : ∀ (i : ℤ) (hi : (g ^ i : (a : α) → α) a = x), ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
⊢ ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a

Tactic:
obtain ⟨i, hi⟩ := hgc ((hs x).mpr hx)

Premises used: Iff.mpr
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
hg' :
  Membership.mem (γ := Subgroup ↥G) (fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
g' : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) :=
  Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Subgroup ↥G) (fixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg) hg'
i : ℤ
hi : (g ^ i : (a : α) → α) a = x
⊢ ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a

Tactic:
⟨g' ^ i, hi.symm⟩

Premises used: HPow.hPow, Exists.intro, Eq.symm
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : Fintype α
inst_1 : DecidableEq α
g : Perm α
hg : g ∈ G
a : α
left : (g : (a : α) → α) a ≠ a
hgc : ∀ ⦃y : α⦄, (g : (a : α) → α) y ≠ y → g.SameCycle a y
hs :
  ∀ (x : α),
    g • x ≠ x ↔
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
x : α
hx :
  Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
    (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x
hg' :
  Membership.mem (γ := Subgroup ↥G) (fixingSubgroup ↥G (↑g.support : Set α)ᶜ)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg)
g' : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) :=
  Subtype.mk (p := fun (x : ↥G) ↦ Membership.mem (γ := Subgroup ↥G) (fixingSubgroup ↥G (↑g.support : Set α)ᶜ) x)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg) hg'
i : ℤ
hi : (g ^ i : (a : α) → α) a = x
⊢ ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a

Tactic:
exact ⟨g' ^ i, hi.symm⟩
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
have : ∀ (this : Fintype α), G = ⊤
⊢ G = ⊤

Tactic:
have := Fintype.ofFinite α
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
inl : ∀ (hα3 : Nat.card α < 3), G = ⊤
inr : ∀ (hα3 : Nat.card α ≥ 3), G = ⊤
⊢ G = ⊤

Tactic:
rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3

Premises used: Nat.card, Nat.lt_or_ge, OfNat.ofNat
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α < 3
⊢ Nat.card α ≤ 2

Tactic:
rw [Nat.lt_succ_iff] at hα3

Premises used: Nat.lt_succ_iff
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
inl : Nat.card.{u_1} ↥G = Nat.card.{u_1} (Perm α)
⊢ G = ⊤

Tactic:
apply Subgroup.eq_top_of_card_eq

Premises used: Subgroup.eq_top_of_card_eq
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
inl : Fintype.card.{u_1} ↥G = Fintype.card.{u_1} (Perm α)
⊢ Nat.card.{u_1} ↥G = Nat.card.{u_1} (Perm α)

Tactic:
simp only [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 : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
inl : Fintype.card.{u_1} (Perm α) ≤ Fintype.card.{u_1} ↥G
⊢ Fintype.card.{u_1} ↥G = Fintype.card.{u_1} (Perm α)

Tactic:
apply le_antisymm (Fintype.card_subtype_le _)

Premises used: Fintype.card_subtype_le, le_antisymm
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
inl : (Nat.card α).factorial ≤ Fintype.card.{u_1} ↥G
⊢ Fintype.card.{u_1} (Perm α) ≤ Fintype.card.{u_1} ↥G

Tactic:
rw [← Nat.card_eq_fintype_card, Nat.card_perm]

Premises used: Nat.card_perm, Nat.card_eq_fintype_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
⊢ (Nat.card α).factorial ≤ Fintype.card.{u_1} ↥G

Tactic:
le_trans (Nat.factorial_le hα3) ?_

Premises used: Nat.factorial_le, le_trans
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
inl : Nat.factorial 2 ≤ Fintype.card.{u_1} ↥G
⊢ (Nat.card α).factorial ≤ Fintype.card.{u_1} ↥G

Tactic:
refine le_trans (Nat.factorial_le hα3) ?_

Premises used: Nat.factorial_le, le_trans
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≤ 2
⊢ Nonempty.{u_1 + 1} ↥G

Tactic:
have : Nonempty G := One.instNonempty
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≤ 2
this : Nonempty.{u_1 + 1} ↥G
inl : 2 ∣ Fintype.card.{u_1} ↥G
⊢ 2 ≤ Fintype.card.{u_1} ↥G

Tactic:
apply Nat.le_of_dvd Fintype.card_pos

Premises used: Nat.le_of_dvd, Fintype.card_pos
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≤ 2
this : Nonempty.{u_1 + 1} ↥G
inl : orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G.toSubmonoid) g hg) ∣ Fintype.card.{u_1} ↥G
⊢ 2 ∣ Fintype.card.{u_1} ↥G

Tactic:
rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]

Premises used: orderOf_submonoid, Equiv.Perm.IsSwap.orderOf, Subtype.mk
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≤ 2
this : Nonempty.{u_1 + 1} ↥G
⊢ orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G.toSubmonoid) g hg) ∣ Fintype.card.{u_1} ↥G

Tactic:
orderOf_dvd_card

Premises used: Set.Mem, orderOf_dvd_card
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≤ 2
this : Nonempty.{u_1 + 1} ↥G
⊢ orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G.toSubmonoid) 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 : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
inr : ∀ (n : ℕ) (hn : Nat.card α = n + 3), G = ⊤
⊢ G = ⊤

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

Premises used: Nat.exists_eq_add_of_le'
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
a : (↑g.support : Set α).ncard + (↑g.support : Set α)ᶜ.ncard = (↑g.support : Set α).ncard + (n + 1)
n₁ : ℕ
⊢ (↑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 : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
⊢ (↑g.support : Set α)ᶜ.ncard = n + 1

Tactic:
have hsc : Set.ncard ((g.support)ᶜ : Set α) = n + 1 := by
    apply Nat.add_left_cancel
    rw [Set.ncard_add_ncard_compl, Set.ncard_coe_finset,
      card_support_eq_two.mpr h2g, add_comm, hn]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
inr : IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
⊢ G = ⊤

Tactic:
apply eq_top_of_isMultiplyPretransitive

Premises used: Equiv.Perm.eq_top_of_isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
this : IsMultiplyPreprimitive (↥G) α (Nat.card α - 1)
⊢ IsMultiplyPretransitive (↥G) α (Nat.card α - 1)

Tactic:
apply IsMultiplyPreprimitive.isMultiplyPretransitive

Premises used: MulAction.IsMultiplyPreprimitive.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
inr : IsMultiplyPreprimitive (↥G) α (Nat.card α - 1)
⊢ IsMultiplyPretransitive (↥G) α (Nat.card α - 1)

Tactic:
suffices IsMultiplyPreprimitive G α (Nat.card α - 1) by
    apply IsMultiplyPreprimitive.isMultiplyPretransitive
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
⊢ Nat.card α - 1 = n + 2

Tactic:
grind
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
inr : IsMultiplyPreprimitive (↥G) α (n + 2)
⊢ IsMultiplyPreprimitive (↥G) α (Nat.card α - 1)

Tactic:
rw [show Nat.card α - 1 = n + 2 by grind]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑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 hsc

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

Tactic:
rw [hn]
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
⊢ n + 2 < n + 3

Tactic:
apply Nat.lt_add_one

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

Tactic:
have := isPretransitive_of_isCycle_mem h2g.isCycle hg
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
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 : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
this :
  IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
⊢ Nat.Prime 2

Tactic:
Nat.prime_two

Premises used: Nat.prime_two
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
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 α)ᶜ) = 2
⊢ Nat.Prime (Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ))

Tactic:
convert! Nat.prime_two

Premises used: Nat.prime_two
-- Module: Mathlib.GroupTheory.GroupAction.Jordan
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
this_1 : Fintype α
hα3 : Nat.card α ≥ 3
n : ℕ
hn : Nat.card α = n + 3
hsc : (↑g.support : Set α)ᶜ.ncard = n + 1
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 α)ᶜ) = 2

Tactic:
rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← card_support_eq_two.mpr h2g]

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

Tactic:
simp [SubMulAction.mem_ofFixingSubgroup_iff, support]

Premises used: Equiv.Perm.support, SubMulAction.mem_ofFixingSubgroup_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
inl : ∀ (hα4 : Nat.card α < 4), alternatingGroup α ≤ G
inr : ∀ (hα4 : Nat.card α ≥ 4), alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G

Tactic:
rcases Nat.lt_or_ge (Nat.card α) 4 with hα4 | hα4

Premises used: Nat.card, Nat.lt_or_ge, OfNat.ofNat
-- 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
⊢ Nat.card α ≤ 3

Tactic:
rw [Nat.lt_succ_iff] at hα4

Premises used: Nat.lt_succ_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 : G.index ≤ 2
⊢ alternatingGroup α ≤ G

Tactic:
apply alternatingGroup_le_of_index_le_two

Premises used: Equiv.Perm.alternatingGroup_le_of_index_le_two