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

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

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

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

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

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]
State after:
case zero
α : Type u_1
x y : α
f✝ g : Finperm α
f : Finperm ℕ
⊢ 1 ∈ Subgroup.closure (adjSwapsBelow 0)

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

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

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

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

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

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

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