-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem swap_mem_closure_isSwap {S : Set (Perm α)} (hS : ∀ f ∈ S, f.IsSwap) {x y : α} :
    swap x y ∈ closure S ↔ x ∈ orbit (closure S) y

Proof state:
case refine_4.intro.intro.intro.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x | swap x y ∈ closure S}
this : a = z ∨ a = w
⊢ False

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

Result:
case refine_4.intro.intro.intro.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x | swap x y ∈ closure S}
this : a = z ∨ a = w
⊢ swap (swap z w • a) a ∈ closure S

Proof state:
case refine_2
α : 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
z : α
hz : z ∈ {x | swap x y ∈ closure S}
⊢ z ∈ orbit (↥(closure S)) x

Tactic:
exact orbit_eq_iff.mpr hf ▸ ⟨⟨swap z y, hz⟩, swap_apply_right z y⟩

Result:
no goals

Proof state:
case refine_1.intro.intro.intro
α : 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
x y : α
hf : swap x y ∈ S
⊢ (swap x y)⁻¹ ∈ S

Tactic:
rwa [swap_inv]

Result:
no goals

Proof state:
case refine_4.intro.intro.intro.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x | swap x y ∈ closure S}
this : a = z ∨ a = w
⊢ swap (swap z w • a) a ∈ closure S

Tactic:
obtain rfl | rfl := this <;> simpa [swap_comm] using subset_closure hσ

Result:
no goals

Proof state:
α : 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
⊢ False

Tactic:
have := exists_smul_not_mem_of_subset_orbit_closure S {x | swap x y ∈ closure S}
  (fun f hf ↦ ?_) (fun z hz ↦ ?_) h ⟨y, ?_⟩

Result:
case refine_4
α : 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 ∈ {x | swap x y ∈ closure S}, σ • a ∉ {x | swap x y ∈ closure S}
⊢ False

case refine_1
α : 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
f : Equiv.Perm α
hf : f ∈ S
⊢ f⁻¹ ∈ S

case refine_2
α : 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
z : α
hz : z ∈ {x | swap x y ∈ closure S}
⊢ z ∈ orbit (↥(closure S)) x

case refine_3
α : 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
⊢ y ∈ {x | swap x y ∈ closure S}

Proof state:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
⊢ swap x y ∈ closure S ↔ x ∈ orbit (↥(closure S)) y

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

Result:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
⊢ swap x y ∈ closure S

Proof state:
α : Type u_2
inst✝ : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
x y : α
hf : x ∈ orbit (↥(closure S)) y
⊢ swap x y ∈ closure S

Tactic:
by_contra h

Result:
α : 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
⊢ False

Proof state:
case refine_4.intro.intro.intro.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x | swap x y ∈ closure S}
⊢ False

Tactic:
have := ne_of_mem_of_not_mem ha hσa

Result:
case refine_4.intro.intro.intro.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x | swap x y ∈ closure S}
this : a ≠ swap z w • a
⊢ False

Proof state:
case refine_3
α : 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.refl α ∈ closure S

Tactic:
apply one_mem

Result:
no goals

Proof state:
case refine_4
α : 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 ∈ {x | swap x y ∈ closure S}, σ • a ∉ {x | swap x y ∈ closure S}
⊢ False

Tactic:
obtain ⟨σ, hσ, a, ha, hσa⟩ := this

Result:
case refine_4.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
hσa : σ • a ∉ {x | swap x y ∈ closure S}
⊢ False

Proof state:
case refine_4.intro.intro.intro.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x | swap x y ∈ closure S}
this : a ≠ swap z w • a
⊢ False

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

Result:
case refine_4.intro.intro.intro.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x | swap x y ∈ closure S}
this : a = z ∨ a = w
⊢ False

Proof state:
case refine_4.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
hσa : σ • a ∉ {x | swap x y ∈ closure S}
⊢ False

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

Result:
case refine_4.intro.intro.intro.intro.intro.intro.intro
α : 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 : a ∈ {x | swap x y ∈ closure S}
z w : α
hzw : z ≠ w
hσ : swap z w ∈ S
hσa : swap z w • a ∉ {x | swap x y ∈ closure S}
⊢ False

Proof state:
case refine_1
α : 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
f : Equiv.Perm α
hf : f ∈ S
⊢ f⁻¹ ∈ S

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

Result:
case refine_1.intro.intro.intro
α : 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
x y : α
hf : swap x y ∈ S
⊢ (swap x y)⁻¹ ∈ S