Theorem: repbleByWord_aux (Bruhat/Word.lean)

State before:
s : Set ℕ
hs : Set.Finite s
⊢ RepbleByWord_aux s
Tactic:
apply @Set.Finite.induction_on _ RepbleByWord_aux _ hs
State after:
case H0
s : Set ℕ
hs : Set.Finite s
⊢ RepbleByWord_aux ∅

case H1
s : Set ℕ
hs : Set.Finite s
⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)

State before:
case H0
s : Set ℕ
hs : Set.Finite s
⊢ RepbleByWord_aux ∅

case H1
s : Set ℕ
hs : Set.Finite s
⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
all_goals clear s hs
State after:
case H0

⊢ RepbleByWord_aux ∅

case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)

State before:
case H0

⊢ RepbleByWord_aux ∅

case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
. intros f hf
  rw [Set.subset_empty_iff, support_empty_iff_id] at hf
  subst hf
  exact ⟨_, idHasWord⟩
State after:
case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)

State before:
case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
. intros a s _ _ hs_repble f hf
  set g := (Equiv.swap a (f a)) * f with hg
  suffices hgs : support g ⊆ s
  obtain ⟨w, hw⟩ := hs_repble g hgs
  obtain ⟨w_swap, hw_swap⟩ := swapHasWord a (f a)
  use (w_swap ++ w)
  simp [Word_mul, hw_swap, hw, hg]
  . intro b hb
    by_cases h : b = a
    . subst b
      absurd (unswap_support f a)
      exact hb
    exact Set.mem_of_mem_insert_of_ne (hf (unswap_support' _ _ hb)) h
State after:
no goals

State before:
case H1
s : Set ℕ
hs : Set.Finite s
⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
clear s hs
State after:
case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)

State before:
case H0

⊢ RepbleByWord_aux ∅
Tactic:
intros f hf
State after:
case H0
f : Equiv.Perm ℕ
hf : support f ⊆ ∅
⊢ RepbleByWord f

State before:
case H0
f : Equiv.Perm ℕ
hf : support f ⊆ ∅
⊢ RepbleByWord f
Tactic:
rw [Set.subset_empty_iff, support_empty_iff_id] at hf
State after:
case H0
f : Equiv.Perm ℕ
hf : f = 1
⊢ RepbleByWord f

State before:
case H0
f : Equiv.Perm ℕ
hf : f = 1
⊢ RepbleByWord f
Tactic:
subst hf
State after:
case H0

⊢ RepbleByWord 1

State before:
case H0

⊢ RepbleByWord 1
Tactic:
exact ⟨_, idHasWord⟩
State after:
no goals

State before:
case H1

⊢ ∀ {a : ℕ} {s : Set ℕ}, a ∉ s → Set.Finite s → RepbleByWord_aux s → RepbleByWord_aux (insert a s)
Tactic:
intros a s _ _ hs_repble f hf
State after:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
⊢ RepbleByWord f

State before:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
⊢ RepbleByWord f
Tactic:
set g := (Equiv.swap a (f a)) * f with hg
State after:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ RepbleByWord f

State before:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ RepbleByWord f
Tactic:
suffices hgs : support g ⊆ s
State after:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s

State before:
case H1
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
obtain ⟨w, hw⟩ := hs_repble g hgs
State after:
case H1.intro
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s

State before:
case H1.intro
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
obtain ⟨w_swap, hw_swap⟩ := swapHasWord a (f a)
State after:
case H1.intro.intro
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
w_swap : Word
hw_swap : Word.toPerm w_swap = Equiv.swap a (f a)
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s

State before:
case H1.intro.intro
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
w_swap : Word
hw_swap : Word.toPerm w_swap = Equiv.swap a (f a)
⊢ RepbleByWord f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
use (w_swap ++ w)
State after:
case h
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
w_swap : Word
hw_swap : Word.toPerm w_swap = Equiv.swap a (f a)
⊢ Word.toPerm (w_swap ++ w) = f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s

State before:
case h
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hgs : support g ⊆ s
w : Word
hw : Word.toPerm w = g
w_swap : Word
hw_swap : Word.toPerm w_swap = Equiv.swap a (f a)
⊢ Word.toPerm (w_swap ++ w) = f

case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
simp [Word_mul, hw_swap, hw, hg]
State after:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s

State before:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
. intro b hb
  by_cases h : b = a
  . subst b
    absurd (unswap_support f a)
    exact hb
  exact Set.mem_of_mem_insert_of_ne (hf (unswap_support' _ _ hb)) h
State after:
no goals

State before:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
⊢ support g ⊆ s
Tactic:
intro b hb
State after:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
⊢ b ∈ s

State before:
case hgs
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
⊢ b ∈ s
Tactic:
by_cases h : b = a
State after:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : b = a
⊢ b ∈ s

case neg
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : ¬b = a
⊢ b ∈ s

State before:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : b = a
⊢ b ∈ s

case neg
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : ¬b = a
⊢ b ∈ s
Tactic:
. subst b
  absurd (unswap_support f a)
  exact hb
State after:
case neg
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : ¬b = a
⊢ b ∈ s

State before:
case neg
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : ¬b = a
⊢ b ∈ s
Tactic:
exact Set.mem_of_mem_insert_of_ne (hf (unswap_support' _ _ hb)) h
State after:
no goals

State before:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
b : ℕ
hb : b ∈ support g
h : b = a
⊢ b ∈ s
Tactic:
subst b
State after:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hb : a ∈ support g
⊢ a ∈ s

State before:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hb : a ∈ support g
⊢ a ∈ s
Tactic:
absurd (unswap_support f a)
State after:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hb : a ∈ support g
⊢ a ∈ support (Equiv.swap a (f a) * f)

State before:
case pos
a : ℕ
s : Set ℕ
a✝¹ : a ∉ s
a✝ : Set.Finite s
hs_repble : RepbleByWord_aux s
f : Equiv.Perm ℕ
hf : support f ⊆ insert a s
g : Equiv.Perm ℕ := Equiv.swap a (f a) * f
hg : g = Equiv.swap a (f a) * f
hb : a ∈ support g
⊢ a ∈ support (Equiv.swap a (f a) * f)
Tactic:
exact hb
State after:
no goals