awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ (k' * k⁻¹) • x = y
have h : (k' * k⁻¹) • k • a = y
Tactic: rw [hk, hk', smul_smul, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ (k' * k⁻¹) • x = y
have h₁ : (k' * k⁻¹) • k • a = k' • a
Tactic: rw [hk, hk', smul_smul, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ (k' * k⁻¹) • x = y
have h₂ : (k' * k⁻¹ * k) • a = k' • a
Tactic: rw [hk, hk', smul_smul, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ (k' * k⁻¹) • x = y
have h₃ : k' • a = k' • a
Tactic: rw [hk, hk', smul_smul, inv_mul_cancel_right]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
have 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
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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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)
have simp_rw : ∀ y ∈ (↑g.support : Set α)ᶜ, Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G) g hg • y = y
Tactic: simp_rw [mem_fixingSubgroup_iff G]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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
⊢ ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
have hg' : 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
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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'
⊢ ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
have obtain : ∀ (i : ℤ) (hi : (g ^ i : (a : α) → α) a = x), ∃ (k : ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)), x = k • a
Tactic: obtain ⟨i, hi⟩ := hgc ((hs x).mpr hx)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
⊢ G = ⊤
have have : ∀ (this : Fintype α), G = ⊤
Tactic: have := Fintype.ofFinite α
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α
⊢ G = ⊤
have inl : ∀ (hα3 : Nat.card α < 3), G = ⊤
Tactic: rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 = ⊤
⊢ G = ⊤
have inr : ∀ (hα3 : Nat.card α ≥ 3), G = ⊤
Tactic: rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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
⊢ G = ⊤
have hα3₁ : Nat.card α ≤ 2
Tactic: rw [Nat.lt_succ_iff] at hα3
Cleared hypotheses: hα3
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ G = ⊤
have inl : Nat.card.{u_1} ↥G = Nat.card.{u_1} (Perm α)
Tactic: apply Subgroup.eq_top_of_card_eq
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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.{u_1} ↥G = Nat.card.{u_1} (Perm α)
have inl : Fintype.card.{u_1} ↥G = Fintype.card.{u_1} (Perm α)
Tactic: simp only [Nat.card_eq_fintype_card]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ Fintype.card.{u_1} ↥G = Fintype.card.{u_1} (Perm α)
have inl : Fintype.card.{u_1} (Perm α) ≤ Fintype.card.{u_1} ↥G
Tactic: apply le_antisymm (Fintype.card_subtype_le _)
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ Fintype.card.{u_1} (Perm α) ≤ Fintype.card.{u_1} ↥G
have inl : (Nat.card α).factorial ≤ Fintype.card.{u_1} ↥G
Tactic: rw [← Nat.card_eq_fintype_card, Nat.card_perm]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
have inl : Nat.factorial 2 ≤ Fintype.card.{u_1} ↥G
Tactic: refine le_trans (Nat.factorial_le hα3) ?_
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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
⊢ 2 ≤ Fintype.card.{u_1} ↥G
have this₁ : Nonempty.{u_1 + 1} ↥G
Tactic: have : Nonempty G := One.instNonempty
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ 2 ≤ Fintype.card.{u_1} ↥G
have inl : 2 ∣ Fintype.card.{u_1} ↥G
Tactic: apply Nat.le_of_dvd Fintype.card_pos
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ 2 ∣ Fintype.card.{u_1} ↥G
have inl : orderOf (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ G.toSubmonoid) g hg) ∣ Fintype.card.{u_1} ↥G
Tactic: rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ G = ⊤
have inr : ∀ (n : ℕ) (hn : Nat.card α = n + 3), G = ⊤
Tactic: obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα3
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
have a : (↑g.support : Set α).ncard + (↑g.support : Set α)ᶜ.ncard = (↑g.support : Set α).ncard + (n + 1)
Tactic: apply Nat.add_left_cancel
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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 = ⊤
have hsc : (↑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]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ G = ⊤
have inr : IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
Tactic: apply eq_top_of_isMultiplyPretransitive
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ IsMultiplyPretransitive (↥G) α (Nat.card α - 1)
have inr : IsMultiplyPreprimitive (↥G) α (Nat.card α - 1)
Tactic: suffices IsMultiplyPreprimitive G α (Nat.card α - 1) by
    apply IsMultiplyPreprimitive.isMultiplyPretransitive
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ IsMultiplyPreprimitive (↥G) α (Nat.card α - 1)
have inr : IsMultiplyPreprimitive (↥G) α (n + 2)
Tactic: rw [show Nat.card α - 1 = n + 2 by grind]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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
⊢ IsMultiplyPreprimitive (↥G) α (n + 2)
have inr : n + 2 < Nat.card α
Tactic: apply hG.isMultiplyPreprimitive hsc
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α
⊢ IsMultiplyPreprimitive (↥G) α (n + 2)
have inr₁ : IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
Tactic: apply hG.isMultiplyPreprimitive hsc
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 < Nat.card α
have inr : n + 2 < n + 3
Tactic: rw [hn]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (hypothesis)
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
⊢ IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
have this₁ : IsPretransitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
Tactic: have := isPretransitive_of_isCycle_mem h2g.isCycle hg
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 α)ᶜ)
⊢ IsPreprimitive.{u_1, u_1} ↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ) ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ)
have inr : Nat.Prime (Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ))
Tactic: apply IsPreprimitive.of_prime_card
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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 (Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ))
have h : Nat.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) = 2
Tactic: convert! Nat.prime_two
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
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.card.{u_1} ↥(ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) = 2
have h : Finset.card.{u_1} (α := α)
    {x : α |
      Membership.mem (γ := SubMulAction (↥(fixingSubgroup ↥G (↑g.support : Set α)ᶜ)) α)
        (ofFixingSubgroup ↥G (↑g.support : Set α)ᶜ) x} =
  g.support.card
Tactic: rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← card_support_eq_two.mpr h2g]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
⊢ G = ⊤
have have : ∀ (this : Fintype α), G = ⊤
Tactic: classical
  have := Fintype.ofFinite α
  rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3
  · -- trivial case : Nat.card α ≤ 2
    rw [Nat.lt_succ_iff] at hα3
    apply Subgroup.eq_top_of_card_eq
    simp only [Nat.card_eq_fintype_card]
    apply le_antisymm (Fintype.card_subtype_le _)
    rw [← Nat.card_eq_fintype_card, Nat.card_perm]
    refine le_trans (Nat.factorial_le hα3) ?_
    rw [Nat.factorial_two]
    have : Nonempty G := One.instNonempty
    apply Nat.le_of_dvd Fintype.card_pos
    rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
    exact orderOf_dvd_card
  -- important case : Nat.card α ≥ 3
  obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα3
  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]
  apply eq_top_of_isMultiplyPretransitive
  suffices IsMultiplyPreprimitive G α (Nat.card α - 1) by
    apply IsMultiplyPreprimitive.isMultiplyPretransitive
  rw [show Nat.card α - 1 = n + 2 by grind]
  apply hG.isMultiplyPreprimitive hsc
  · rw [hn]; apply Nat.lt_add_one
  have := isPretransitive_of_isCycle_mem h2g.isCycle hg
  apply IsPreprimitive.of_prime_card
  convert! Nat.prime_two
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← card_support_eq_two.mpr h2g]
  simp [SubMulAction.mem_ofFixingSubgroup_iff, support]
-- Lean 4 proof step from Mathlib.GroupTheory.GroupAction.Jordan (goal)
Goal:
α : Type u_1
G : Subgroup (Perm α)
inst : DecidableEq α
inst_1 : Finite α
hG : IsPreprimitive (↥G) α
g : Perm α
h2g : g.IsSwap
hg : g ∈ G
have have₁ have₂ : ∀ (this : Fintype α), G = ⊤
⊢ G = ⊤
have inl : ∀ (this : Fintype α) (hα3 : Nat.card α < 3), G = ⊤
Tactic: classical
  have := Fintype.ofFinite α
  rcases Nat.lt_or_ge (Nat.card α) 3 with hα3 | hα3
  · -- trivial case : Nat.card α ≤ 2
    rw [Nat.lt_succ_iff] at hα3
    apply Subgroup.eq_top_of_card_eq
    simp only [Nat.card_eq_fintype_card]
    apply le_antisymm (Fintype.card_subtype_le _)
    rw [← Nat.card_eq_fintype_card, Nat.card_perm]
    refine le_trans (Nat.factorial_le hα3) ?_
    rw [Nat.factorial_two]
    have : Nonempty G := One.instNonempty
    apply Nat.le_of_dvd Fintype.card_pos
    rw [← h2g.orderOf, orderOf_submonoid ⟨g, hg⟩]
    exact orderOf_dvd_card
  -- important case : Nat.card α ≥ 3
  obtain ⟨n, hn⟩ := Nat.exists_eq_add_of_le' hα3
  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]
  apply eq_top_of_isMultiplyPretransitive
  suffices IsMultiplyPreprimitive G α (Nat.card α - 1) by
    apply IsMultiplyPreprimitive.isMultiplyPretransitive
  rw [show Nat.card α - 1 = n + 2 by grind]
  apply hG.isMultiplyPreprimitive hsc
  · rw [hn]; apply Nat.lt_add_one
  have := isPretransitive_of_isCycle_mem h2g.isCycle hg
  apply IsPreprimitive.of_prime_card
  convert! Nat.prime_two
  rw [Nat.card_eq_fintype_card, Fintype.card_subtype, ← card_support_eq_two.mpr h2g]
  simp [SubMulAction.mem_ofFixingSubgroup_iff, support]