Theorem: Equiv.Perm.is_prod_swap_list (Jordan/IndexNormal.lean)

State before:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
g : Perm α
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ g = List.prod l
Tactic:
induction' g using Equiv.Perm.swap_induction_on with f x y hxy hf
State after:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ 1 = List.prod l

case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
hf : ∃ l, (∀ s ∈ l, IsSwap s) ∧ f = List.prod l
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ swap x y * f = List.prod l

State before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ 1 = List.prod l
Tactic:
use List.nil
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (∀ s ∈ [], IsSwap s) ∧ 1 = List.prod []

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ (∀ s ∈ [], IsSwap s) ∧ 1 = List.prod []
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∀ s ∈ [], IsSwap s

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ 1 = List.prod []

State before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ ∀ s ∈ [], IsSwap s
Tactic:
intro s hs
State after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Perm α
hs : s ∈ []
⊢ IsSwap s

State before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Perm α
hs : s ∈ []
⊢ IsSwap s
Tactic:
exfalso
State after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Perm α
hs : s ∈ []
⊢ False

State before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Perm α
hs : s ∈ []
⊢ False
Tactic:
exact List.not_mem_nil s hs
State after:
no goals

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ 1 = List.prod []
Tactic:
simp only [List.prod_nil]
State after:
no goals

State before:
case a
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
hf : ∃ l, (∀ s ∈ l, IsSwap s) ∧ f = List.prod l
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ swap x y * f = List.prod l
Tactic:
obtain ⟨l, hl, hf⟩ := hf
State after:
case a.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ swap x y * f = List.prod l

State before:
case a.intro.intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ ∃ l, (∀ s ∈ l, IsSwap s) ∧ swap x y * f = List.prod l
Tactic:
use Equiv.swap x y::l
State after:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ (∀ s ∈ swap x y :: l, IsSwap s) ∧ swap x y * f = List.prod (swap x y :: l)

State before:
case h
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ (∀ s ∈ swap x y :: l, IsSwap s) ∧ swap x y * f = List.prod (swap x y :: l)
Tactic:
constructor
State after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ ∀ s ∈ swap x y :: l, IsSwap s

case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ swap x y * f = List.prod (swap x y :: l)

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ swap x y * f = List.prod (swap x y :: l)
Tactic:
rw [List.prod_cons]
State after:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ swap x y * f = swap x y * List.prod l

State before:
case h.right
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ swap x y * f = swap x y * List.prod l
Tactic:
rw [hf]
State after:
no goals

State before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
⊢ ∀ s ∈ swap x y :: l, IsSwap s
Tactic:
intro s hs
State after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ swap x y :: l
⊢ IsSwap s

State before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ swap x y :: l
⊢ IsSwap s
Tactic:
rw [List.mem_cons] at hs
State after:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y ∨ s ∈ l
⊢ IsSwap s

State before:
case h.left
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y ∨ s ∈ l
⊢ IsSwap s
Tactic:
cases' hs with hs hs
State after:
case h.left.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y
⊢ IsSwap s

case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s

State before:
case h.left.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y
⊢ IsSwap s

case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s
Tactic:
rw [hs]
State after:
case h.left.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y
⊢ IsSwap (swap x y)

case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s

State before:
case h.left.inl
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s = swap x y
⊢ IsSwap (swap x y)

case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s
Tactic:
exact ⟨x, y, hxy, rfl⟩
State after:
case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s

State before:
case h.left.inr
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
f : Perm α
x y : α
hxy : x ≠ y
l : List (Perm α)
hl : ∀ s ∈ l, IsSwap s
hf : f = List.prod l
s : Perm α
hs : s ∈ l
⊢ IsSwap s
Tactic:
exact hl s hs
State after:
no goals