awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.KleinFour (hypothesis)
Goal:
α : Type u_1
inst : DecidableEq α
inst_1 : Fintype α
hα4 : Nat.card α = 4
h : Subgroup.Normal (G := ↥(alternatingGroup α)) (kleinFour α)
this :
  Nat.card.{u_1} (HasQuotient.Quotient ↥(alternatingGroup α) (B := Subgroup ↥(alternatingGroup α)) (kleinFour α)) = 3
comm_le : LE.le (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) (kleinFour α)
comm_ne_bot : Ne.{u_1 + 1} (α := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) ⊥
k : ↥(alternatingGroup α)
hk : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (commutator ↥(alternatingGroup α)) k
hk' : k ≠ 1
hk2 : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (kleinFour α) k
⊢ (↑k : Perm α).cycleType = {2, 2}
have hk2₁ : k = 1 ∨ (↑k : Perm α).cycleType = {2, 2}
Tactic: rw [← SetLike.mem_coe, coe_kleinFour_of_card_eq_four hα4,
    Set.mem_union, Set.mem_singleton_iff, Set.mem_setOf_eq] at hk2
Cleared hypotheses: hk2
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : 2 < s.ncard
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
have hs₁ : ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
Tactic: rw [two_lt_ncard_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : ∃ (a : α) (b : α) (c : α), a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
have obtain : ∀ (a b c : α) (ha : a ∈ s) (hb : b ∈ s) (hc : c ∈ s) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c),
  ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
Tactic: obtain ⟨a, b, c, ha, hb, hc, hab, hac, hbc⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
have refine : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b * swap a c)
Tactic: refine ⟨swap a b * swap a c, ?_, isThreeCycle_swap_mul_swap_same hab hac hbc⟩
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a b c : α
ha : a ∈ s
hb : b ∈ s
hc : c ∈ s
hab : a ≠ b
hac : a ≠ c
hbc : b ≠ c
⊢ Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) (swap a b * swap a c)
have rw : (swap a b * swap a c)⁻¹ • s ⊆ s
Tactic: rw [mem_stabilizer_set_iff_subset_smul_set s.toFinite, subset_smul_set_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
have inl : ∀ (hs : 2 < s.ncard), ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
Tactic: rcases Nat.lt_or_ge 2 (ncard s) with hs | hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
inl :
  ∀ (hs : 2 < s.ncard),
    ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
have inr : ∀ (hs : 2 ≥ s.ncard), ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
Tactic: rcases Nat.lt_or_ge 2 (ncard s) with hs | hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
have this : s.ncard + sᶜ.ncard = Nat.card α
Tactic: have := ncard_add_ncard_compl s
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hα : 4 < Nat.card α
hs : 2 ≥ s.ncard
this : s.ncard + sᶜ.ncard = Nat.card α
⊢ ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g ∧ g.IsThreeCycle
have inr : ∃ (g : Perm α), Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) sᶜ) g ∧ g.IsThreeCycle
Tactic: rw [← stabilizer_compl]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup (Perm α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (Perm α) s ⊓ alternatingGroup α ≤ G
⊢ alternatingGroup α ≤ G
have obtain : ∀ (g : Perm α) (hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g) (hg3 : g.IsThreeCycle),
  alternatingGroup α ≤ G
Tactic: obtain ⟨g, hg, hg3⟩ := exists_mem_stabilizer_isThreeCycle s h4
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
h4 : 4 < Nat.card α
G : Subgroup (Perm α)
hG' : IsPreprimitive (↥G) α
s : Set α
hG : stabilizer (Perm α) s ⊓ alternatingGroup α ≤ G
g : Perm α
hg : Membership.mem (γ := Subgroup (Perm α)) (stabilizer (Perm α) s) g
hg3 : g.IsThreeCycle
⊢ alternatingGroup α ≤ G
have apply : g ∈ G
Tactic: apply alternatingGroup_le_of_isPreprimitive_of_isThreeCycle_mem hG' hg3
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
⊢ ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have obtain : ∀ (a : α) (ha : a ∈ sᶜ) (b : α) (hb : b ∈ sᶜ) (hab : a ≠ b),
  ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
Tactic: obtain ⟨a, ha, b, hb, hab⟩ := hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
have h : (swap a b).IsSwap ∧ _root_.Disjoint s (↑(swap a b).support : Set α)
Tactic: use Equiv.swap a b
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
a : α
ha : a ∈ sᶜ
b : α
hb : b ∈ sᶜ
hab : a ≠ b
⊢ (swap a b).IsSwap ∧ _root_.Disjoint s (↑(swap a b).support : Set α)
have h : a ≠ b ∧ _root_.Disjoint s (↑(swap a b).support : Set α)
Tactic: rw [swap_isSwap_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
Tactic: have : ∃ k : Perm α, IsSwap k ∧ _root_.Disjoint s k.support := by
    obtain ⟨a, ha, b, hb, hab⟩ := hs
    use Equiv.swap a b
    rw [swap_isSwap_iff]; aesop
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
this : ∃ (k : Perm α), k.IsSwap ∧ _root_.Disjoint s (↑k.support : Set α)
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have obtain : ∀ (k : Perm α) (hk_swap : k.IsSwap) (hk_support : _root_.Disjoint s (↑k.support : Set α)),
  Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
Tactic: obtain ⟨k, hk_swap, hk_support⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
⊢ k • s = s
have rw : k • s ⊆ s
Tactic: rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
x : α
hx : x ∈ s
⊢ k • x ∈ s
have h : k • x = x
Tactic: convert! hx
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
x : α
hx : x ∈ s
⊢ k • x = x
have h : x ∉ k.support
Tactic: rw [Perm.smul_def, ← Perm.notMem_support]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (hypothesis)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
⊢ Function.Surjective.{u_1 + 1, u_1 + 1} (α := ↥(stabilizer (↥(alternatingGroup α)) s)) (β := Perm (↑s : Type u_1))
    toPerm
have hks : k • s = s
Tactic: have hks : k • s = s := by
    rw [← mem_stabilizer_iff, mem_stabilizer_set_iff_smul_set_subset s.toFinite]
    intro _
    simp only [mem_smul_set]
    rintro ⟨x, hx, rfl⟩
    convert! hx
    rw [Perm.smul_def, ← Perm.notMem_support]
    exact (Set.disjoint_left.mp hk_support) hx
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
have inl : ∀ (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)),
  ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
Tactic: rcases Int.units_eq_one_or (sign g) with hsg | hsg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
inl :
  ∀ (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)),
    ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
have inr : ∀ (hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)),
  ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
Tactic: rcases Int.units_eq_one_or (sign g) with hsg | hsg
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
have property : Membership.mem (α := Perm α) (alternatingGroup α)
  ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
Tactic: use! Equiv.Perm.ofSubtype g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
property :
  Membership.mem (α := Perm α) (alternatingGroup α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
have property₁ : Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
  (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) sorry :
    ↥(alternatingGroup α))
Tactic: use! Equiv.Perm.ofSubtype g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
property :
  Membership.mem (α := Perm α) (alternatingGroup α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α)
property₁ :
  Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
    (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) ⋯ :
      ↥(alternatingGroup α))
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
have h : toPerm (α := ↥(stabilizer (↥(alternatingGroup α)) s))
    (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦
        Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) x)
        (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
          ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) sorry)
        sorry :
      ↥(stabilizer (↥(alternatingGroup α)) s)) =
  g
Tactic: use! Equiv.Perm.ofSubtype g
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (1 : ℤˣ)
⊢ Membership.mem (α := ↥(alternatingGroup α)) (γ := Subgroup ↥(alternatingGroup α))
    (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g) ⋯ :
      ↥(alternatingGroup α))
have property : HSMul.hSMul (α := Perm α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) s =
  s
Tactic: rw [mem_stabilizer_iff, Submonoid.mk_smul]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
have property : HMul.hMul (α := Perm α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k ∈
  alternatingGroup α
Tactic: use! Equiv.Perm.ofSubtype g * k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
property :
  HMul.hMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k ∈
    alternatingGroup α
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
have property₁ : Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
  (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
    (HMul.hMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
    sorry)
Tactic: use! Equiv.Perm.ofSubtype g * k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
property :
  HMul.hMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k ∈
    alternatingGroup α
property₁ :
  Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      (HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
      ⋯)
⊢ ∃ (a : ↥(stabilizer (↥(alternatingGroup α)) s)), toPerm a = g
have h : toPerm (α := ↥(stabilizer (↥(alternatingGroup α)) s))
    (Subtype.mk (p := fun (x : ↥(alternatingGroup α)) ↦
      Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s) x)
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        (HMul.hMul (α := Perm α)
          ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
        sorry)
      sorry) =
  g
Tactic: use! Equiv.Perm.ofSubtype g * k
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      (HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
      ⋯)
have property : HSMul.hSMul (α := ↥(alternatingGroup α))
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      (HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
      sorry)
    s =
  s
Tactic: rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
property :
  HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        (HMul.hMul (α := Perm α)
          ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
        ⋯)
      s =
    s
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      (HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
      ⋯)
have property₁ : HMul.hMul (α := Perm α)
      ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k •
    s =
  s
Tactic: rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]
-- Lean 4 proof step from Mathlib.GroupTheory.SpecificGroups.Alternating.MaximalSubgroups (goal)
Goal:
α : Type u_1
inst : Fintype α
inst_1 : DecidableEq α
s : Set α
hs : sᶜ.Nontrivial
k : Perm α
hk_swap : k.IsSwap
hk_support : _root_.Disjoint s (↑k.support : Set α)
hks : k • s = s
g : Perm (↑s : Type u_1)
hsg : Eq (α := ℤˣ) (((sign : Perm (↑s : Type u_1) →* ℤˣ) : (a : Perm (↑s : Type u_1)) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
property :
  HSMul.hSMul (α := ↥(alternatingGroup α))
      (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
        (HMul.hMul (α := Perm α)
          ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
        ⋯)
      s =
    s
property₁ :
  HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k •
      s =
    s
⊢ Membership.mem (γ := Subgroup ↥(alternatingGroup α)) (stabilizer (↥(alternatingGroup α)) s)
    (Subtype.mk (p := fun (x : Perm α) ↦ x ∈ alternatingGroup α)
      (HMul.hMul (α := Perm α)
        ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) k)
      ⋯)
have property₂ : HSMul.hSMul (α := Perm α)
    ((Perm.ofSubtype (p := fun (x : α) ↦ x ∈ s) : (a : Perm { x : α // x ∈ s }) → Perm α) g : Perm α) (k • s) =
  s
Tactic: rw [mem_stabilizer_iff, Submonoid.mk_smul, mul_smul, hks, ofSubtype_mem_stabilizer]