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

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

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

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

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

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

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

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

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

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

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

State before:
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
n : ℕ
⊢ 0 ∈ Set.Iic n
Tactic:
simp
State after:
no goals