Theorem: Finperm.cl_swapsAt_eq (Bruhat/Finperm.lean)

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)
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)

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]
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)

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 ?_⟩
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))

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⟩
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))

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
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))

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]
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))

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)
State after:
no goals

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
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)

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
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)

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
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)

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⟩
State after:
no goals

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]
State after:
case aux.inl
α : Type u_1
x y✝ : α
f g : Finperm α
inst✝ : DecidableEq α
t : Set α
y : α
⊢ 1 ∈ Subgroup.closure (swapsAt y t)

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 _
State after:
no goals

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]
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))

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
State after:
no goals