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

State before:
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
obtain (h | h) := eq_or_ne f.support ∅
State after:
case inl
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support = ∅
⊢ f ∈ Subgroup.closure (swapsOf t)

case inr
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support ≠ ∅
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support ≠ ∅
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
simp only [ne_eq, eq_empty_iff_forall_not_mem, mem_support_iff, not_not, not_forall] at h
State after:
case inr
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : ∃ x, ¬f x = x
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : ∃ x, ¬f x = x
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
obtain ⟨x, hx⟩ := h
State after:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : Type u_1
x✝ y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
x : α
hx : ¬f x = x
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hx' : x ∈ f.support := by simpa
State after:
case inr.intro
α : 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
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
set g := f * swap x (f⁻¹ x) with hg_def
State after:
case inr.intro
α : 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)
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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)
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hsupp : g.support ⊆ _ := support_mul_pair_subset hx'
State after:
case inr.intro
α : 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
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have _ : g.support.card < f.support.card := by
  exact card_lt_card <| (hsupp.trans_ssubset (erase_ssubset hx'))
State after:
case inr.intro
α : 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
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hg_supp : (g.support : Set α) ⊆ t
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
⊢ ↑g.support ⊆ t

case inr.intro
α : 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
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
have hg := support_closure_aux hg_supp
State after:
case inr.intro
α : 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 ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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 ∈ Subgroup.closure (swapsOf t)
Tactic:
have hs : swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
State after:
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)

case inr.intro
α : 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 ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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 ∈ Subgroup.closure (swapsOf t)
Tactic:
have hf' : f = g * (swap x (f⁻¹ x))
State after:
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)

case inr.intro
α : 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)
hf' : f = g * swap x (f⁻¹ x)
⊢ f ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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)
hf' : f = g * swap x (f⁻¹ x)
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
rw [hf']
State after:
case inr.intro
α : 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)
hf' : f = g * swap x (f⁻¹ x)
⊢ g * swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)

State before:
case inr.intro
α : 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)
hf' : f = g * swap x (f⁻¹ x)
⊢ g * swap x (f⁻¹ x) ∈ Subgroup.closure (swapsOf t)
Tactic:
exact Subgroup.mul_mem _ hg hs
State after:
no goals

State before:
case inl
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support = ∅
⊢ f ∈ Subgroup.closure (swapsOf t)
Tactic:
rw [show f = 1 from (support_eq_empty_iff _).1 h]
State after:
case inl
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support = ∅
⊢ 1 ∈ Subgroup.closure (swapsOf t)

State before:
case inl
α : Type u_1
x y : α
f✝ g : Finperm α
inst✝ : DecidableEq α
t : Set α
f : Finperm α
hf : ↑f.support ⊆ t
h : f.support = ∅
⊢ 1 ∈ Subgroup.closure (swapsOf t)
Tactic:
exact Subgroup.one_mem _
State after:
no goals

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

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

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

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

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

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

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

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