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

State before:
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
⊢ Subgroup.closure adjSwaps = ⊤
Tactic:
ext f
State after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ f ∈ Subgroup.closure adjSwaps ↔ f ∈ ⊤

State before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ f ∈ Subgroup.closure adjSwaps ↔ f ∈ ⊤
Tactic:
simp only [Subgroup.mem_top, iff_true]
State after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ f ∈ Subgroup.closure adjSwaps

State before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ f ∈ Subgroup.closure adjSwaps
Tactic:
have hss : (f.support : Set ℕ) ⊆ Set.Iic f.ub
State after:
case hss
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ ↑f.support ⊆ Set.Iic (ub f)

case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
⊢ f ∈ Subgroup.closure adjSwaps

State before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
⊢ f ∈ Subgroup.closure adjSwaps
Tactic:
have hf := restrict_mono hss <| mem_restrict_support f
State after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ restrict (Set.Iic (ub f))
⊢ f ∈ Subgroup.closure adjSwaps

State before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ restrict (Set.Iic (ub f))
⊢ f ∈ Subgroup.closure adjSwaps
Tactic:
rw [← closure_adjSwapsBelow_eq] at hf
State after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
⊢ f ∈ Subgroup.closure adjSwaps

State before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
⊢ f ∈ Subgroup.closure adjSwaps
Tactic:
refine (Subgroup.closure_mono ?_) hf
State after:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
⊢ adjSwapsBelow (ub f) ⊆ adjSwaps

State before:
case h
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
⊢ adjSwapsBelow (ub f) ⊆ adjSwaps
Tactic:
rintro _ ⟨i, -, rfl⟩
State after:
case h.intro.intro
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
i : ℕ
⊢ (fun i => swap i (i + 1)) i ∈ adjSwaps

State before:
case h.intro.intro
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
hss : ↑f.support ⊆ Set.Iic (ub f)
hf : f ∈ Subgroup.closure (adjSwapsBelow (ub f))
i : ℕ
⊢ (fun i => swap i (i + 1)) i ∈ adjSwaps
Tactic:
exact ⟨i, rfl⟩
State after:
no goals

State before:
case hss
α : Type u_1
x y : α
f✝¹ g : Finperm α
f✝ f : Finperm ℕ
⊢ ↑f.support ⊆ Set.Iic (ub f)
Tactic:
exact fun x hx ↦ (f.lt_ub hx).le
State after:
no goals