awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
refine : ∀ (h : Fintype.card α ∣ i), x = y
⊢ Eq (α := Subgroup (Perm α)) (closure {σ, swap x ((σ ^ i : (a : α) → α) x)}) ⊤

Tactic:
refine closure_cycle_coprime_swap
    (Nat.Coprime.symm (h0.coprime_iff_not_dvd.mpr fun h => h4 ?_)) h1 h2 x

Premises used: Iff.mpr, Nat.Coprime.symm, Equiv.Perm.closure_cycle_coprime_swap, Nat.Prime.coprime_iff_not_dvd
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
h : Fintype.card α ∣ i
obtain : ∀ (m : ℕ) (hm : i = Fintype.card α * m), x = y
⊢ x = y

Tactic:
obtain ⟨m, hm⟩ := h
-- Module: Mathlib.GroupTheory.Perm.Closure
Goal:
α : Type u_2
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
h0 : Nat.Prime (Fintype.card α)
h1 : σ.IsCycle
h2 : σ.support = univ
x y : α
h4 : x ≠ y
h5 : τ = swap x y
i : ℕ
hi : (σ ^ i : (a : α) → α) x = y
m : ℕ
hm : i = Fintype.card α * m
rwa : ∀ (hi : (σ ^ (Fintype.card α * m) : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₁ : ∀ (hi : ((σ ^ Fintype.card α) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₂ : ∀ (hi : ((σ ^ card.{u_2} (α := α) univ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₃ : ∀ (hi : ((σ ^ #σ.support) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₄ : ∀ (hi : ((σ ^ orderOf σ) ^ m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₅ : ∀ (hi : (HPow.hPow (α := Perm α) 1 m : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₆ : ∀ (hi : (1 : (a : α) → α) x = y) (hm : i = Fintype.card α * m), x = y
rwa₇ rwa₈ rwa₉ rwa₁₀ : ∀ (hi : x = y) (hm : i = Fintype.card α * m), x = y
⊢ x = y

Tactic:
rwa [hm, pow_mul, ← Finset.card_univ, ← h2, ← h1.orderOf, pow_orderOf_eq_one, one_pow,
    one_apply] at hi

Premises used: one_pow, Finset.card_univ, Equiv.Perm.IsCycle.orderOf, pow_mul, pow_orderOf_eq_one, Equiv.Perm.one_apply
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : Membership.mem (γ := Subgroup G) (closure S) g
⊢ (fixedBy.{u_1, u_2} (M := G) α 1)ᶜ.Finite

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : Membership.mem (γ := Subgroup G) (closure S) g
⊢ ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure S) x), (fixedBy α x)ᶜ.Finite → (fixedBy α x⁻¹)ᶜ.Finite

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : Membership.mem (γ := Subgroup G) (closure S) g
refine :
  ∀ (g g' : G),
    Membership.mem (γ := Subgroup G) (closure S) g →
      Membership.mem (γ := Subgroup G) (closure S) g' →
        ∀ (hg : (fixedBy α g)ᶜ.Finite) (hg' : (fixedBy α g')ᶜ.Finite),
          (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ
⊢ (fixedBy α g)ᶜ.Finite

Tactic:
refine closure_induction h (by simp) (fun g g' _ _ hg hg' ↦ (hg.union hg').subset ?_)
      (by simp) hg
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g_1 : G
hg_1 : Membership.mem (γ := Subgroup G) (closure S) g_1
g g' : G
h_1 : Membership.mem (γ := Subgroup G) (closure S) g
h_2 : Membership.mem (γ := Subgroup G) (closure S) g'
hg : (fixedBy α g)ᶜ.Finite
hg' : (fixedBy α g')ᶜ.Finite
simp_rw : (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g ∩ fixedBy α g')ᶜ
simp_rw₁ : fixedBy α g ∩ fixedBy α g' ⊆ fixedBy α (g * g')
⊢ (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ

Tactic:
simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]

Premises used: Set.compl_inter, MulAction.fixedBy_mul, Set.compl_subset_compl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
have : ∀ (b : α) (hb : b ∈ T), ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
⊢ ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)

Tactic:
have ⟨b, hb⟩ := nonempty
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
b : α
hb : b ∈ T
obtain :
  ∀ (σ : ↥(closure S)) (hb : (fun (m : ↥(closure S)) ↦ m • a) σ ∈ T),
    ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
⊢ ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)

Tactic:
obtain ⟨σ, rfl⟩ := subset hb

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun (m : ↥(closure S)) ↦ m • a) σ ∈ T
contrapose : ∀ (h : LE.le (α := Subgroup G) (closure S) (stabilizer G T)), a ∈ T
⊢ ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)

Tactic:
contrapose notMem with h
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun (m : ↥(closure S)) ↦ m • a) σ ∈ T
h : LE.le (α := Subgroup G) (closure S) (stabilizer G T)
⊢ a ∈ T

Tactic:
smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)

Premises used: Iff.mp, Set.smul_mem_smul_set_iff
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
nonempty : T.Nonempty
σ : ↥(closure S)
hb : (fun (m : ↥(closure S)) ↦ m • a) σ ∈ T
h : LE.le (α := Subgroup G) (closure S) (stabilizer G T)
⊢ a ∈ T

Tactic:
exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)

Premises used: Iff.mp, Set.smul_mem_smul_set_iff
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
⊢ ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)

Tactic:
have key0 : ¬ closure S ≤ stabilizer G T := by
    have ⟨b, hb⟩ := nonempty
    obtain ⟨σ, rfl⟩ := subset hb
    contrapose notMem with h
    exact smul_mem_smul_set_iff.mp ((h σ.2).symm ▸ hb)
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ¬LE.le (α := Subgroup G) (closure S) (stabilizer G T)
contrapose! :
  ∀ (key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T), LE.le (α := Subgroup G) (closure S) (stabilizer G T)
⊢ ∃ σ ∈ S, ∃ a ∈ T, σ • a ∉ T

Tactic:
contrapose! key0
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T
⊢ LE.le (α := Subgroup G) (closure S) (stabilizer G T)

Tactic:
(closure_le _).mpr fun σ hσ ↦ ?_

Premises used: Iff.mpr, Subgroup.closure_le
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T
refine : ∀ (σ : G) (hσ : σ ∈ S), σ ∈ (↑(stabilizer G T) : Set G)
⊢ LE.le (α := Subgroup G) (closure S) (stabilizer G T)

Tactic:
refine (closure_le _).mpr fun σ hσ ↦ ?_

Premises used: Iff.mpr, Subgroup.closure_le
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T
σ : G
hσ : σ ∈ S
simp_rw : ∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T
⊢ σ ∈ (↑(stabilizer G T) : Set G)

Tactic:
simp_rw [SetLike.mem_coe, mem_stabilizer_iff, Set.ext_iff, mem_smul_set_iff_inv_smul_mem]

Premises used: SetLike.mem_coe, MulAction.mem_stabilizer_iff, Set.ext_iff, Set.mem_smul_set_iff_inv_smul_mem
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ ∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T

Tactic:
fun a ↦ ⟨fun h ↦ smul_inv_smul σ a ▸ key0 σ hσ (σ⁻¹ • a) h, key0 σ⁻¹ (hS σ hσ) a⟩

Premises used: Eq.rec, smul_inv_smul, Inv.inv, Iff.intro, HSMul.hSMul
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
G : Type u_1
α : Type u_2
inst : Group G
inst_1 : MulAction G α
S : Set G
T : Set α
a : α
hS : ∀ g ∈ S, g⁻¹ ∈ S
subset : T ⊆ orbit.{u_1, u_2} (↥(closure S)) a
notMem : a ∉ T
nonempty : T.Nonempty
key0 : ∀ (σ : G) (_ : σ ∈ S) (a : α) (_ : a ∈ T), σ • a ∈ T
σ : G
hσ : σ ∈ S
⊢ ∀ (x : α), σ⁻¹ • x ∈ T ↔ x ∈ T

Tactic:
exact fun a ↦ ⟨fun h ↦ smul_inv_smul σ a ▸ key0 σ hσ (σ⁻¹ • a) h, key0 σ⁻¹ (hS σ hσ) a⟩
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
⊢ Set.Finite (α := α) {x, y}

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
x y z : α
h : Membership.mem (γ := Set α) {x, y}ᶜ z
a : z ≠ x
a₁ : z ≠ y
⊢ z ∈ fixedBy α (swap x y)

Tactic:
apply swap_apply_of_ne_of_ne

Premises used: Equiv.swap_apply_of_ne_of_ne
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
y z : α
h : Membership.mem (γ := Set α) {z, y}ᶜ z
⊢ False

Tactic:
simp at h
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
x z : α
h : Membership.mem (γ := Set α) {x, z}ᶜ z
⊢ False

Tactic:
simp at h
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
σ : Perm α
h : σ.IsSwap
obtain : ∀ (x y : α), (fixedBy α (swap x y))ᶜ.Finite
⊢ (fixedBy α σ)ᶜ.Finite

Tactic:
obtain ⟨x, y, -, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
⊢ (fixedBy α (swap x y))ᶜ.Finite

Tactic:
finite_compl_fixedBy_swap

Premises used: finite_compl_fixedBy_swap
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
x y : α
⊢ (fixedBy α (swap x y))ᶜ.Finite

Tactic:
exact finite_compl_fixedBy_swap

Premises used: finite_compl_fixedBy_swap
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
inl : ∀ (hab : swap a a ∈ M) (hbc : swap a c ∈ M), swap a c ∈ M
inr : ∀ (hab' : a ≠ b), swap a c ∈ M
⊢ swap a c ∈ M

Tactic:
obtain rfl | hab' := eq_or_ne a b

Premises used: eq_or_ne, rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a a ∈ M
hbc : swap a c ∈ M
⊢ swap a c ∈ M

Tactic:
hbc
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a a ∈ M
hbc : swap a c ∈ M
⊢ swap a c ∈ M

Tactic:
exact hbc
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
inr : ∀ (hbc : swap b a ∈ M), swap a a ∈ M
inr₁ : ∀ (hac : a ≠ c), swap a c ∈ M
⊢ swap a c ∈ M

Tactic:
obtain rfl | hac := eq_or_ne a c

Premises used: eq_or_ne, rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hab' : a ≠ b
hbc : swap b a ∈ M
⊢ swap a a ∈ M

Tactic:
swap_self a ▸ one_mem M

Premises used: Eq.rec, Equiv.swap_self, OneMemClass.one_mem, Eq.symm
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a b : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hab' : a ≠ b
hbc : swap b a ∈ M
⊢ swap a a ∈ M

Tactic:
exact swap_self a ▸ one_mem M
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
inr : swap b c * swap a b * swap b c ∈ M
⊢ swap a c ∈ M

Tactic:
rw [swap_comm, ← swap_mul_swap_mul_swap hab' hac]

Premises used: Equiv.swap_comm, Equiv.swap_mul_swap_mul_swap
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ swap b c * swap a b * swap b c ∈ M

Tactic:
mul_mem (mul_mem hbc hab) hbc

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
a b c : α
C : Type u_3
inst_1 : SetLike.{u_3, u_2} C (Equiv.Perm α)
inst_2 : SubmonoidClass C (Equiv.Perm α)
M : C
hab : swap a b ∈ M
hbc : swap b c ∈ M
hab' : a ≠ b
hac : a ≠ c
⊢ swap b c * swap a b * swap b c ∈ M

Tactic:
exact mul_mem (mul_mem hbc hab) hbc

Premises used: MulMemClass.mul_mem
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y) ↔ x ∈ orbit (↥(closure S)) y

Tactic:
⟨fun h ↦ ⟨⟨swap x y, h⟩, swap_apply_right x y⟩, fun hf ↦ ?_⟩

Premises used: Equiv.swap, Subtype.mk, Iff.intro, Exists.intro, Equiv.swap_apply_right
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
refine : ∀ (hf : x ∈ orbit (↥(closure S)) y), Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y) ↔ x ∈ orbit (↥(closure S)) y

Tactic:
refine ⟨fun h ↦ ⟨⟨swap x y, h⟩, swap_apply_right x y⟩, fun hf ↦ ?_⟩
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
by_contra : ∀ (h : swap x y ∉ closure S), False
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
refine_4 :
  ∀
    (this :
      ∃ σ ∈ S,
        ∃ (a : α),
          Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a ∧
            σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
    False
refine_1 : ∀ (f : Equiv.Perm α) (hf : f ∈ S), f⁻¹ ∈ S
refine_2 :
  ∀ (z : α)
    (hz : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} z),
    z ∈ orbit (↥(closure S)) x
refine_3 : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} y
⊢ False

Tactic:
have := exists_smul_notMem_of_subset_orbit_closure S {x | swap x y ∈ closure S}
    (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
this :
  ∃ σ ∈ S,
    ∃ (a : α),
      Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a ∧
        σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
refine_4 :
  ∀ (σ : Equiv.Perm α) (hσ : σ ∈ S) (a : α)
    (ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a)
    (hσa : σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}), False
⊢ False

Tactic:
obtain ⟨σ, hσ, a, ha, hσa⟩ := this
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
σ : Equiv.Perm α
hσ : σ ∈ S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
hσa : σ • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
refine_4 :
  ∀ (z w : α) (hzw : z ≠ w) (hσ : swap z w ∈ S)
    (hσa : swap z w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}), False
⊢ False

Tactic:
obtain ⟨z, w, hzw, rfl⟩ := hS σ hσ

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
⊢ a ≠ swap z w • a

Tactic:
have := ne_of_mem_of_not_mem ha hσa
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
this : a ≠ swap z w • a
⊢ a = z ∨ a = w

Tactic:
rw [Perm.smul_def, ne_comm, swap_apply_ne_self_iff, and_iff_right hzw] at this

Premises used: Equiv.Perm.smul_def, Equiv.swap_apply_ne_self_iff, and_iff_right, ne_comm
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
this : a = z ∨ a = w
⊢ False

Tactic:
hσa (SubmonoidClass.swap_mem_trans (closure S) ?_ ha)

Premises used: Subgroup.closure, SubmonoidClass.swap_mem_trans
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
this : a = z ∨ a = w
refine_4 : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap z w • a) a)
⊢ False

Tactic:
refine hσa (SubmonoidClass.swap_mem_trans (closure S) ?_ ha)

Premises used: Subgroup.closure, SubmonoidClass.swap_mem_trans
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
this : a = z ∨ a = w
refine_4 :
  ∀ (hzw : a ≠ w) (hσ : swap a w ∈ S)
    (hσa : swap a w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
    Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap a w • a) a)
refine_4₁ :
  ∀ (hzw : z ≠ a) (hσ : swap z a ∈ S)
    (hσa : swap z a • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}),
    Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap z a • a) a)
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap z w • a) a)

Tactic:
obtain rfl | rfl := this

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
w : α
hzw : a ≠ w
hσ : swap a w ∈ S
hσa : swap a w • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap a w • a) a)

Tactic:
simpa [swap_comm] using subset_closure hσ

Premises used: Equiv.swap_comm, Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
a : α
ha : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} a
z : α
hzw : z ≠ a
hσ : swap z a ∈ S
hσa : swap z a • a ∉ {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)}
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap (swap z a • a) a)

Tactic:
simpa [swap_comm] using subset_closure hσ

Premises used: Equiv.swap_comm, Subgroup.subset_closure
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf_1 : x ∈ orbit (↥(closure S)) y
h : swap x y ∉ closure S
f : Equiv.Perm α
hf : f ∈ S
refine_1 : ∀ (x y : α) (hf : swap x y ∈ S), (swap x y)⁻¹ ∈ S
⊢ f⁻¹ ∈ S

Tactic:
obtain ⟨x, y, -, rfl⟩ := hS f hf

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x_1 y_1 : α
hf_1 : x_1 ∈ orbit (↥(closure S)) y_1
h : swap x_1 y_1 ∉ closure S
x y : α
hf refine_1 refine_1₁ refine_1₂ refine_1₃ : swap x y ∈ S
⊢ (swap x y)⁻¹ ∈ S

Tactic:
rwa [swap_inv]

Premises used: Equiv.swap_inv