awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
z : α
hz : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} z
⊢ z ∈ orbit (↥(closure S)) x

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

Premises used: Iff.mpr, Equiv.swap, Eq.rec, Subtype.mk, Exists.intro, MulAction.orbit_eq_iff, Equiv.swap_apply_right, Eq.symm
-- 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
z : α
hz : Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} z
⊢ z ∈ orbit (↥(closure S)) x

Tactic:
exact orbit_eq_iff.mpr hf ▸ ⟨⟨swap z y, hz⟩, swap_apply_right z 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
refine_3 : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (Equiv.refl α)
⊢ Membership.mem (γ := Set α) {x : α | Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (swap x y)} y

Tactic:
rw [mem_setOf, swap_self]

Premises used: Set.mem_setOf, Equiv.swap_self
-- 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
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) (Equiv.refl α)

Tactic:
apply one_mem

Premises used: OneMemClass.one_mem
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f ↔
    (fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)

Tactic:
⟨fun hf ↦ ⟨?_, fun x ↦ mem_orbit_iff.mpr ⟨⟨f, hf⟩, rfl⟩⟩, ?_⟩

Premises used: Iff.mpr, MulAction.mem_orbit_iff, Subtype.mk, And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
refine_1 : ∀ (hf : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f), (fixedBy α f)ᶜ.Finite
refine_2 :
  ((fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)) →
    Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f ↔
    (fixedBy α f)ᶜ.Finite ∧ ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)

Tactic:
refine ⟨fun hf ↦ ⟨?_, fun x ↦ mem_orbit_iff.mpr ⟨⟨f, hf⟩, rfl⟩⟩, ?_⟩
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
⊢ (fixedBy α f)ᶜ.Finite

Tactic:
finite_compl_fixedBy_closure_iff.mpr (fun f hf ↦ (hS f hf).finite_compl_fixedBy) _ hf

Premises used: Iff.mpr, Equiv.Perm.IsSwap.finite_compl_fixedBy, finite_compl_fixedBy_closure_iff
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
⊢ (fixedBy α f)ᶜ.Finite

Tactic:
exact finite_compl_fixedBy_closure_iff.mpr (fun f hf ↦ (hS f hf).finite_compl_fixedBy) _ hf

Premises used: Iff.mpr, Equiv.Perm.IsSwap.finite_compl_fixedBy, finite_compl_fixedBy_closure_iff
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
fin : (fixedBy α f)ᶜ.Finite
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
⊢ let supp := (fixedBy α f)ᶜ;
  supp.Finite

Tactic:
set supp := (fixedBy α f)ᶜ with supp_eq

Premises used: MulAction.fixedBy
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
fin : (fixedBy α f)ᶜ.Finite
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
fin₁ :
  let supp := (fixedBy α f)ᶜ;
  supp.Finite
⊢ let supp := (fixedBy α f)ᶜ;
  supp = (fixedBy α f)ᶜ

Tactic:
set supp := (fixedBy α f)ᶜ with supp_eq

Premises used: MulAction.fixedBy
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp : Set α := (fixedBy α f)ᶜ
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
refine_2 : (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f

Tactic:
suffices h : (fixedBy α f)ᶜ ⊆ supp → f ∈ closure S from h supp_eq.symm.subset
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp : Set α := (fixedBy α f)ᶜ
fin : supp.Finite
supp_eq : supp = (fixedBy α f)ᶜ
refine_2 :
  ∀ (supp : Set α) (fin : supp.Finite) (supp_eq : supp = (fixedBy α f)ᶜ),
    (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
⊢ (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f

Tactic:
clear_value supp
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp : Set α
fin : supp.Finite
refine_2 :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
⊢ (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f

Tactic:
revert f
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
apply :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ ∅ → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
apply₁ :
  ∀ {a : α} {s : Set α},
    a ∉ s →
      ∀ (hs : s.Finite),
        (∀ {f : Equiv.Perm α}
            (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
            (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f) →
          ∀ {f : Equiv.Perm α}
            (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
            (fixedBy α f)ᶜ ⊆ insert a s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
⊢ ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ supp → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f

Tactic:
apply fin.induction_on ..

Premises used: Set.Finite.induction_on
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) 1

Tactic:
(closure S).one_mem

Premises used: Subgroup.closure, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
h : f = 1
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f

Tactic:
convert! (closure S).one_mem

Premises used: Subgroup.closure, Subgroup.one_mem
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
h : ∀ (x : α), Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ f = 1

Tactic:
ext
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x : α
h : ∀ (h : ¬Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)), False
⊢ Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)

Tactic:
by_contra h
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x : α
h : ¬Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ False

Tactic:
emp h

Premises used: Set.Mem
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
f : Equiv.Perm α
emp : (fixedBy α f)ᶜ ⊆ ∅
x : α
h : ¬Eq (α := α) ((f : (a : α) → α) x : α) ((1 : (a : α) → α) x : α)
⊢ False

Tactic:
exact emp h
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f

Tactic:
(mul_mem_cancel_left ((swap_mem_closure_isSwap hS).2 (hf a))).1
    (ih (fun b ↦ ?_) fun b hb ↦ ?_)

Premises used: Iff.mpr, swap_mem_closure_isSwap, Iff.mp, mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
refine_1 :
  ∀ (b : α),
    Membership.mem (α := α) (orbit (↥(closure S)) b)
      ((HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f : (a : α) → α) b : α)
refine_2 :
  ∀ (b : α) (hb : b ∈ (fixedBy α (HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f))ᶜ),
    b ∈ s
⊢ Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f

Tactic:
refine (mul_mem_cancel_left ((swap_mem_closure_isSwap hS).2 (hf a))).1
    (ih (fun b ↦ ?_) fun b hb ↦ ?_)

Premises used: Iff.mpr, swap_mem_closure_isSwap, Iff.mp, mul_mem_cancel_left
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
refine_1 :
  (if Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α) then a
    else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) ∈
    orbit (↥(closure S)) b
⊢ Membership.mem (α := α) (orbit (↥(closure S)) b)
    ((HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f : (a : α) → α) b : α)

Tactic:
rw [Perm.mul_apply, swap_apply_def]

Premises used: Equiv.swap_apply_def, Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
pos : ∀ (h1 : Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)), a ∈ orbit (↥(closure S)) b
pos₁ :
  ∀ (h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)) (h2 : (f : (a : α) → α) b = a),
    Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) a : α)
neg :
  ∀ (h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)) (h2 : ¬(f : (a : α) → α) b = a),
    Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) b : α)
⊢ (if Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α) then a
    else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) ∈
    orbit (↥(closure S)) b

Tactic:
split_ifs with h1 h2
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)
pos : a ∈ orbit (↥(closure S)) a
⊢ a ∈ orbit (↥(closure S)) b

Tactic:
rw [← orbit_eq_iff.mpr (hf b), h1, orbit_eq_iff.mpr (hf a)]

Premises used: Iff.mpr, MulAction.orbit_eq_iff
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)
⊢ a ∈ orbit (↥(closure S)) a

Tactic:
apply mem_orbit_self

Premises used: MulAction.mem_orbit_self
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)
h2 : (f : (a : α) → α) b = a
pos : Membership.mem (α := α) (orbit (↥(closure S)) a) ((f : (a : α) → α) a : α)
⊢ Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) a : α)

Tactic:
rw [← orbit_eq_iff.mpr (hf b), h2]

Premises used: Iff.mpr, MulAction.orbit_eq_iff
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)
h2 : (f : (a : α) → α) b = a
⊢ Membership.mem (α := α) (orbit (↥(closure S)) a) ((f : (a : α) → α) a : α)

Tactic:
apply hf
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)
h2 : ¬(f : (a : α) → α) b = a
⊢ Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) b : α)

Tactic:
hf b
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
h1 : ¬Eq (α := α) ((f : (a : α) → α) b : α) ((f : (a : α) → α) a : α)
h2 : ¬(f : (a : α) → α) b = a
⊢ Membership.mem (α := α) (orbit (↥(closure S)) b) ((f : (a : α) → α) b : α)

Tactic:
exact hf b
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∈ (fixedBy α (HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f))ᶜ
refine_2 :
  ∀ (hb : b ∉ s), b ∉ (fixedBy α (HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f))ᶜ
⊢ b ∈ s

Tactic:
contrapose hb
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
refine_2 : (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
⊢ b ∉ (fixedBy α (HMul.hMul (α := Equiv.Perm α) (swap ((f : (a : α) → α) a) a : Equiv.Perm α) f))ᶜ

Tactic:
simp_rw [notMem_compl_iff, mem_fixedBy, Perm.smul_def, Perm.mul_apply, swap_apply_def,
      apply_eq_iff_eq]

Premises used: Equiv.Perm.smul_def, Equiv.swap_apply_def, Set.notMem_compl_iff, Equiv.Perm.mul_apply, Equiv.apply_eq_iff_eq, MulAction.mem_fixedBy
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
pos :
  ∀ (hb' : (f : (a : α) → α) b = b),
    (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
neg :
  ∀ (hb' : ¬(f : (a : α) → α) b = b),
    (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b
⊢ (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b

Tactic:
by_cases hb' : f b = b

Premises used: DFunLike.coe
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : (f : (a : α) → α) b = b
pos : (if b = a then a else if b = a then (f : (a : α) → α) a else b) = b
⊢ (if b = a then a else if (f : (a : α) → α) b = a then (f : (a : α) → α) a else (f : (a : α) → α) b) = b

Tactic:
rw [hb']
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : (f : (a : α) → α) b = b
pos : ∀ (h : b = a), a = b
neg : ∀ (h : ¬b = a), b = b
⊢ (if b = a then a else if b = a then (f : (a : α) → α) a else b) = b

Tactic:
split_ifs with h
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : (f : (a : α) → α) b = b
h : b = a
⊢ a = b

Tactic:
simp only [h]
-- Module: Mathlib.GroupTheory.Perm.ClosureSwap
Goal:
α : Type u_2
inst : DecidableEq α
S : Set (Equiv.Perm α)
hS : ∀ f ∈ S, f.IsSwap
supp : Set α
fin : supp.Finite
a : α
s : Set α
ih :
  ∀ {f : Equiv.Perm α} (hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)),
    (fixedBy α f)ᶜ ⊆ s → Membership.mem (γ := Subgroup (Equiv.Perm α)) (closure S) f
f : Equiv.Perm α
hf : ∀ (x : α), Membership.mem (α := α) (orbit (↥(closure S)) x) ((f : (a : α) → α) x : α)
supp_subset : (fixedBy α f)ᶜ ⊆ insert a s
b : α
hb : b ∉ s
hb' : (f : (a : α) → α) b = b
h : ¬b = a
⊢ b = b

Tactic:
simp only [h]