internlm/Lean-Github huggingface dataset:
Theorem: Finperm.support_closure_aux
Proof state before:
α : Type u_1
x✝ y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
⊢ x ∈ f.support
Tactic:
simpa
Proof state after:
no goals
Theorem: Finperm.support_closure_aux
Proof state before:
α : Type u_1
x✝ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
⊢ card g.support < card f.support
Tactic:
exact card_lt_card <| (hsupp.trans_ssubset (erase_ssubset hx'))
Proof state after:
no goals
Theorem: Finperm.support_closure_aux
Proof state before:
case hg_supp
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
⊢ ↑g.support ⊆ t
Tactic:
refine (Finset.coe_subset.2 hsupp).trans (subset_trans (Finset.coe_subset.2 ?_) hf)
Proof state after:
case hg_supp
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
⊢ erase f.support x ⊆ f.support
Theorem: Finperm.support_closure_aux
Proof state before:
case hg_supp
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
⊢ erase f.support x ⊆ f.support
Tactic:
exact erase_subset x f.support
Proof state after:
no goals
Theorem: Finperm.support_closure_aux
Proof state before:
case hs
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
⊢ swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
Tactic:
refine Subgroup.subset_closure ⟨_, _, hf hx', hf ?_, ?_, rfl⟩
Proof state after:
case hs.refine_1
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
⊢ f⁻¹ x ∈ ↑f.support

case hs.refine_2
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
⊢ x ≠ f⁻¹ x
Theorem: Finperm.support_closure_aux
Proof state before:
case hs.refine_2
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
⊢ x ≠ f⁻¹ x
Tactic:
rwa [ne_eq, eq_inv_iff_eq]
Proof state after:
no goals
Theorem: Finperm.support_closure_aux
Proof state before:
case hs.refine_1
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
⊢ f⁻¹ x ∈ ↑f.support
Tactic:
rwa [mem_coe, mem_support_iff, apply_inv_apply, ne_eq, eq_inv_iff_eq]
Proof state after:
no goals
Theorem: Finperm.support_closure_aux
Proof state before:
case hf'
α : Type u_1
x✝¹ y : α
f✝ g✝ : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
hx' : x ∈ f.support
g : Finperm α := f * swap x (f⁻¹ x)
hg_def : g = f * swap x (f⁻¹ x)
hsupp : g.support ⊆ erase f.support x
x✝ : card g.support < card f.support
hg_supp : ↑g.support ⊆ t
hg : g ∈ Subgroup.closure (swapsOf t)
hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
⊢ f = g * swap x (f⁻¹ x)
Tactic:
rw [hg_def, mul_assoc, swap_mul_swap, mul_one]
Proof state after:
no goals
Theorem: Finperm.cl_swaps_eq_top
Proof state before:
α✝ : Type u_1
x y : α✝
f g : Finperm α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ Subgroup.closure (swaps α) = ⊤
Tactic:
rw [← swapsOf_univ_eq, ← restrict_univ]
Proof state after:
α✝ : Type u_1
x y : α✝
f g : Finperm α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ Subgroup.closure (swapsOf Set.univ) = restrict Set.univ
Theorem: Finperm.cl_swaps_eq_top
Proof state before:
α✝ : Type u_1
x y : α✝
f g : Finperm α✝
inst✝¹ : DecidableEq α✝
α : Type u_2
inst✝ : DecidableEq α
⊢ Subgroup.closure (swapsOf Set.univ) = restrict Set.univ
Tactic:
exact cl_swapsOf_eq _
Proof state after:
no goals
Theorem: Finperm.swapsAt_subset_swapsOf
Proof state before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
⊢ swapsAt x t ⊆ swapsOf (insert x t)
Tactic:
rintro s ⟨i, hi, rfl⟩
Proof state after:
case intro.intro
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
i : α
hi : i ∈ t \ {x}
⊢ (fun x_1 => swap x x_1) i ∈ swapsOf (insert x t)
Theorem: Finperm.swapsAt_subset_swapsOf
Proof state before:
case intro.intro
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
i : α
hi : i ∈ t \ {x}
⊢ (fun x_1 => swap x x_1) i ∈ swapsOf (insert x t)
Tactic:
exact ⟨x, _, Or.inl rfl, Or.inr hi.1, Ne.symm hi.2, rfl⟩
Proof state after:
no goals
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
⊢ Subgroup.closure (swapsAt x t) = restrict (insert x t)
Tactic:
have aux : ∀ {y}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
Proof state after:
case aux
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
⊢ ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)

α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
⊢ Subgroup.closure (swapsAt x t) = restrict (insert x t)
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
⊢ Subgroup.closure (swapsAt x t) = restrict (insert x t)
Tactic:
rw [← cl_swapsOf_eq, le_antisymm_iff]
Proof state after:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
⊢ Subgroup.closure (swapsAt x t) ≤ Subgroup.closure (swapsOf (insert x t)) ∧
    Subgroup.closure (swapsOf (insert x t)) ≤ Subgroup.closure (swapsAt x t)
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
⊢ Subgroup.closure (swapsAt x t) ≤ Subgroup.closure (swapsOf (insert x t)) ∧
    Subgroup.closure (swapsOf (insert x t)) ≤ Subgroup.closure (swapsAt x t)
Tactic:
refine ⟨Subgroup.closure_mono (swapsAt_subset_swapsOf _ _), (Subgroup.closure_le _).2 ?_⟩
Proof state after:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
⊢ swapsOf (insert x t) ⊆ ↑(Subgroup.closure (swapsAt x t))
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
⊢ swapsOf (insert x t) ⊆ ↑(Subgroup.closure (swapsAt x t))
Tactic:
rintro _ ⟨i, j, hi, hj, hne, rfl⟩
Proof state after:
case intro.intro.intro.intro.intro
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i j : α
hi : i ∈ insert x t
hj : j ∈ insert x t
hne : i ≠ j
⊢ swap i j ∈ ↑(Subgroup.closure (swapsAt x t))
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case intro.intro.intro.intro.intro
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i j : α
hi : i ∈ insert x t
hj : j ∈ insert x t
hne : i ≠ j
⊢ swap i j ∈ ↑(Subgroup.closure (swapsAt x t))
Tactic:
obtain (rfl | hjne) := eq_or_ne x j
Proof state after:
case intro.intro.intro.intro.intro.inl
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i : α
hi : i ∈ insert x t
hj : x ∈ insert x t
hne : i ≠ x
⊢ swap i x ∈ ↑(Subgroup.closure (swapsAt x t))

case intro.intro.intro.intro.intro.inr
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i j : α
hi : i ∈ insert x t
hj : j ∈ insert x t
hne : i ≠ j
hjne : x ≠ j
⊢ swap i j ∈ ↑(Subgroup.closure (swapsAt x t))
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case intro.intro.intro.intro.intro.inr
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i j : α
hi : i ∈ insert x t
hj : j ∈ insert x t
hne : i ≠ j
hjne : x ≠ j
⊢ swap i j ∈ ↑(Subgroup.closure (swapsAt x t))
Tactic:
rw [← swap_conj_eq hne hjne, swap_comm i]
Proof state after:
case intro.intro.intro.intro.intro.inr
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i j : α
hi : i ∈ insert x t
hj : j ∈ insert x t
hne : i ≠ j
hjne : x ≠ j
⊢ swap x i * swap x j * swap x i ∈ ↑(Subgroup.closure (swapsAt x t))
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case intro.intro.intro.intro.intro.inr
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i j : α
hi : i ∈ insert x t
hj : j ∈ insert x t
hne : i ≠ j
hjne : x ≠ j
⊢ swap x i * swap x j * swap x i ∈ ↑(Subgroup.closure (swapsAt x t))
Tactic:
exact mul_mem (mul_mem (aux hi) (aux hj)) (aux hi)
Proof state after:
no goals
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case aux
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
⊢ ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
Tactic:
intro y hy
Proof state after:
case aux
α : Type u_1
x✝ y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
y : α
hy : y ∈ insert x t
⊢ swap x y ∈ Subgroup.closure (swapsAt x t)
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case aux
α : Type u_1
x✝ y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
y : α
hy : y ∈ insert x t
⊢ swap x y ∈ Subgroup.closure (swapsAt x t)
Tactic:
rw [← Set.insert_diff_singleton] at hy
Proof state after:
case aux
α : Type u_1
x✝ y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
y : α
hy : y ∈ insert x (t \ {x})
⊢ swap x y ∈ Subgroup.closure (swapsAt x t)
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case aux
α : Type u_1
x✝ y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
y : α
hy : y ∈ insert x (t \ {x})
⊢ swap x y ∈ Subgroup.closure (swapsAt x t)
Tactic:
obtain (rfl | hy) := hy
Proof state after:
case aux.inl
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
t : Set α
y : α
⊢ swap y y ∈ Subgroup.closure (swapsAt y t)

case aux.inr
α : Type u_1
x✝ y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
y : α
hy : y ∈ t \ {x}
⊢ swap x y ∈ Subgroup.closure (swapsAt x t)
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case aux.inr
α : Type u_1
x✝ y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
y : α
hy : y ∈ t \ {x}
⊢ swap x y ∈ Subgroup.closure (swapsAt x t)
Tactic:
exact Subgroup.subset_closure ⟨y, hy, rfl⟩
Proof state after:
no goals
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case aux.inl
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
t : Set α
y : α
⊢ swap y y ∈ Subgroup.closure (swapsAt y t)
Tactic:
rw [swap_self, ← one_def]
Proof state after:
case aux.inl
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
t : Set α
y : α
⊢ 1 ∈ Subgroup.closure (swapsAt y t)
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case aux.inl
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
t : Set α
y : α
⊢ 1 ∈ Subgroup.closure (swapsAt y t)
Tactic:
exact Subgroup.one_mem _
Proof state after:
no goals
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case intro.intro.intro.intro.intro.inl
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i : α
hi : i ∈ insert x t
hj : x ∈ insert x t
hne : i ≠ x
⊢ swap i x ∈ ↑(Subgroup.closure (swapsAt x t))
Tactic:
rw [swap_comm]
Proof state after:
case intro.intro.intro.intro.intro.inl
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i : α
hi : i ∈ insert x t
hj : x ∈ insert x t
hne : i ≠ x
⊢ swap x i ∈ ↑(Subgroup.closure (swapsAt x t))
Theorem: Finperm.cl_swapsAt_eq
Proof state before:
case intro.intro.intro.intro.intro.inl
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
aux : ∀ {y : α}, y ∈ insert x t → swap x y ∈ Subgroup.closure (swapsAt x t)
i : α
hi : i ∈ insert x t
hj : x ∈ insert x t
hne : i ≠ x
⊢ swap x i ∈ ↑(Subgroup.closure (swapsAt x t))
Tactic:
exact aux hi
Proof state after:
no goals
Theorem: Finperm.cl_swapsAt_eq'
Proof state before:
α : Type u_1
x✝ y : α
f g : Finperm α
inst✝ : DecidableEq α
x : α
t : Set α
hxt : x ∈ t
⊢ Subgroup.closure (swapsAt x t) = restrict t
Tactic:
rw [cl_swapsAt_eq, Set.insert_eq_of_mem hxt]
Proof state after:
no goals
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
Tactic:
induction' n with n IH
Proof state after:
case zero
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
⊢ swap 0 Nat.zero ∈ Subgroup.closure (adjSwapsBelow Nat.zero)

case succ
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 (Nat.succ n) ∈ Subgroup.closure (adjSwapsBelow (Nat.succ n))
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case succ
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 (Nat.succ n) ∈ Subgroup.closure (adjSwapsBelow (Nat.succ n))
Tactic:
simp [Nat.succ_eq_add_one]
Proof state after:
case succ
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 (n + 1) ∈ Subgroup.closure (adjSwapsBelow (n + 1))
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case succ
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 (n + 1) ∈ Subgroup.closure (adjSwapsBelow (n + 1))
Tactic:
rw [← swap_conj_eq (x := 0) (y := n) (z := n+1)]
Proof state after:
case succ
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 n * swap n (n + 1) * swap 0 n ∈ Subgroup.closure (adjSwapsBelow (n + 1))

case succ.hxz
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ 0 ≠ n + 1

case succ.hyz
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ n ≠ n + 1
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case succ.hyz
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ n ≠ n + 1
Tactic:
exact Ne.symm (Nat.succ_ne_self n)
Proof state after:
no goals
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case zero
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
⊢ swap 0 Nat.zero ∈ Subgroup.closure (adjSwapsBelow Nat.zero)
Tactic:
simp only [Nat.zero_eq, swap_self, ← one_def]
Proof state after:
case zero
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
⊢ 1 ∈ Subgroup.closure (adjSwapsBelow 0)
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case zero
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
⊢ 1 ∈ Subgroup.closure (adjSwapsBelow 0)
Tactic:
exact Subgroup.one_mem (Subgroup.closure (adjSwapsBelow 0))
Proof state after:
no goals
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case succ
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 n * swap n (n + 1) * swap 0 n ∈ Subgroup.closure (adjSwapsBelow (n + 1))
Tactic:
refine Subgroup.mul_mem _ (Subgroup.mul_mem _ ?_ ?_) ?_
Proof state after:
case succ.refine_1
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 n ∈ Subgroup.closure (adjSwapsBelow (n + 1))

case succ.refine_2
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap n (n + 1) ∈ Subgroup.closure (adjSwapsBelow (n + 1))

case succ.refine_3
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 n ∈ Subgroup.closure (adjSwapsBelow (n + 1))
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case succ.refine_3
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 n ∈ Subgroup.closure (adjSwapsBelow (n + 1))
Tactic:
exact Subgroup.closure_mono (adjSwapsBelow_mono (le_self_add : n ≤ n +1)) IH
Proof state after:
no goals
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case succ.refine_1
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap 0 n ∈ Subgroup.closure (adjSwapsBelow (n + 1))
Tactic:
exact Subgroup.closure_mono (adjSwapsBelow_mono (le_self_add : n ≤ n +1)) IH
Proof state after:
no goals
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case succ.refine_2
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ swap n (n + 1) ∈ Subgroup.closure (adjSwapsBelow (n + 1))
Tactic:
exact Subgroup.subset_closure ⟨n, by simp, rfl⟩
Proof state after:
no goals
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ n ∈ Set.Iio (n + 1)
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.adjSwapsBelow_aux
Proof state before:
case succ.hxz
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
IH : swap 0 n ∈ Subgroup.closure (adjSwapsBelow n)
⊢ 0 ≠ n + 1
Tactic:
exact Nat.ne_of_beq_eq_false rfl
Proof state after:
no goals
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ Subgroup.closure (adjSwapsBelow n) = restrict (Set.Iic n)
Tactic:
refine le_antisymm ((Subgroup.closure_le _).2 ?_) ?_
Proof state after:
case refine_1
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ adjSwapsBelow n ⊆ ↑(restrict (Set.Iic n))

case refine_2
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ restrict (Set.Iic n) ≤ Subgroup.closure (adjSwapsBelow n)
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_2
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ restrict (Set.Iic n) ≤ Subgroup.closure (adjSwapsBelow n)
Tactic:
rw [← cl_swapsAt_eq' (x := 0) (by simp)]
Proof state after:
case refine_2
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ Subgroup.closure (swapsAt 0 (Set.Iic n)) ≤ Subgroup.closure (adjSwapsBelow n)
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_2
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ Subgroup.closure (swapsAt 0 (Set.Iic n)) ≤ Subgroup.closure (adjSwapsBelow n)
Tactic:
apply (Subgroup.closure_le _).2
Proof state after:
case refine_2
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ swapsAt 0 (Set.Iic n) ⊆ ↑(Subgroup.closure (adjSwapsBelow n))
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_2
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ swapsAt 0 (Set.Iic n) ⊆ ↑(Subgroup.closure (adjSwapsBelow n))
Tactic:
rintro _ ⟨i, ⟨hi : i ≤ n, -⟩, rfl⟩
Proof state after:
case refine_2.intro.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i ≤ n
⊢ (fun x => swap 0 x) i ∈ ↑(Subgroup.closure (adjSwapsBelow n))
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_2.intro.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i ≤ n
⊢ (fun x => swap 0 x) i ∈ ↑(Subgroup.closure (adjSwapsBelow n))
Tactic:
simp only [SetLike.mem_coe]
Proof state after:
case refine_2.intro.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i ≤ n
⊢ swap 0 i ∈ Subgroup.closure (adjSwapsBelow n)
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_2.intro.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i ≤ n
⊢ swap 0 i ∈ Subgroup.closure (adjSwapsBelow n)
Tactic:
exact Subgroup.closure_mono (adjSwapsBelow_mono hi) <| adjSwapsBelow_aux i
Proof state after:
no goals
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_1
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ adjSwapsBelow n ⊆ ↑(restrict (Set.Iic n))
Tactic:
rintro x ⟨i, hi, rfl⟩
Proof state after:
case refine_1.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i ∈ Set.Iio n
⊢ (fun i => swap i (i + 1)) i ∈ ↑(restrict (Set.Iic n))
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_1.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i ∈ Set.Iio n
⊢ (fun i => swap i (i + 1)) i ∈ ↑(restrict (Set.Iic n))
Tactic:
simp only [SetLike.mem_coe, mem_restrict_iff, swap_support, self_eq_add_right, ite_false,
  coe_insert, coe_singleton, Set.insert_subset_iff, Set.mem_Iic, Set.singleton_subset_iff]
Proof state after:
case refine_1.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i ∈ Set.Iio n
⊢ i ≤ n ∧ i + 1 ≤ n
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_1.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i ∈ Set.Iio n
⊢ i ≤ n ∧ i + 1 ≤ n
Tactic:
rw [Set.mem_Iio, ← Nat.add_one_le_iff] at hi
Proof state after:
case refine_1.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i + 1 ≤ n
⊢ i ≤ n ∧ i + 1 ≤ n
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
case refine_1.intro.intro
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n i : ℕ
hi : i + 1 ≤ n
⊢ i ≤ n ∧ i + 1 ≤ n
Tactic:
constructor <;> linarith
Proof state after:
no goals
Theorem: Finperm.closure_adjSwapsBelow_eq
Proof state before:
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ 0 ∈ Set.Iic n
Tactic:
simp
Proof state after:
no goals
Theorem: Finperm.closure_adjSwaps_eq
Proof state before:
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
⊢ Subgroup.closure adjSwaps = ⊤
Tactic:
ext f
Proof state after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ f ∈ Subgroup.closure adjSwaps ↔ f ∈ ⊤