α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this : ∀ (f : Perm α), IsSwap f → ↑s f = 1
⊢ False
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
⊢ False
have : ∀ f, IsSwap f → s f = 1 := fun f ⟨a, b, hab, hab'⟩ => by
  rw [← isConj_iff_eq, ← Or.resolve_right (Int.units_eq_one_or _) h, hab']
  exact s.map_isConj (isConj_swap hab hxy)
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
⊢ False
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this : ∀ (f : Perm α), IsSwap f → ↑s f = 1
⊢ False
let ⟨g, hg⟩ := hs (-1)
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ False
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
⊢ False
let ⟨l, hl⟩ := (truncSwapFactors g).out
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this✝ : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
this : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = 1
⊢ False
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ False
have : ∀ a ∈ l.map s, a = (1 : ℤˣ) := fun a ha =>
  let ⟨g, hg⟩ := List.mem_map.1 ha
  hg.2 ▸ this _ (hl.2 _ hg.1)
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
this✝ : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = 1
this : ↑s (List.prod l) = 1
⊢ False
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this✝ : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
this : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = 1
⊢ False
have : s l.prod = 1 := by
  rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
this✝ : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = 1
this : -1 = 1
⊢ False
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
this✝ : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = 1
this : ↑s (List.prod l) = 1
⊢ False
rw [hl.1, hg] at this
no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
this✝ : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = 1
this : -1 = 1
⊢ False
exact absurd this (by simp_all)
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f✝ : Perm α
x✝¹ : IsSwap f✝
x y : α
hxy : x ≠ y
hxy' : f✝ = swap x y
h : ¬↑s (swap x y) = -1
f : Perm α
x✝ : IsSwap f
a b : α
hab : a ≠ b
hab' : f = swap a b
⊢ IsConj (↑s (swap a b)) (↑s (swap x y))
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f✝ : Perm α
x✝¹ : IsSwap f✝
x y : α
hxy : x ≠ y
hxy' : f✝ = swap x y
h : ¬↑s (swap x y) = -1
f : Perm α
x✝ : IsSwap f
a b : α
hab : a ≠ b
hab' : f = swap a b
⊢ ↑s f = 1
rw [← isConj_iff_eq, ← Or.resolve_right (Int.units_eq_one_or _) h, hab']
no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f✝ : Perm α
x✝¹ : IsSwap f✝
x y : α
hxy : x ≠ y
hxy' : f✝ = swap x y
h : ¬↑s (swap x y) = -1
f : Perm α
x✝ : IsSwap f
a b : α
hab : a ≠ b
hab' : f = swap a b
⊢ IsConj (↑s (swap a b)) (↑s (swap x y))
exact s.map_isConj (isConj_swap hab hxy)
no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this✝ : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
this : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = 1
⊢ ↑s (List.prod l) = 1
rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
f : Perm α
x✝ : IsSwap f
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬↑s (swap x y) = -1
this✝¹ : ∀ (f : Perm α), IsSwap f → ↑s f = 1
g : Perm α
hg : ↑s g = -1
l : List (Perm α)
hl : List.prod l = g ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
this✝ : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = 1
this : -1 = 1
⊢ ¬-1 = 1
simp_all
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
this : ∀ {f : Perm α}, IsSwap f → ↑s f = -1
f : Perm α
l : List (Perm α)
hl₁ : List.prod l = f
hl₂ : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ ↑s f = ↑sign f
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
this : ∀ {f : Perm α}, IsSwap f → ↑s f = -1
f : Perm α
⊢ ↑s f = ↑sign f
let ⟨l, hl₁, hl₂⟩ := (truncSwapFactors f).out
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
this : ∀ {f : Perm α}, IsSwap f → ↑s f = -1
f : Perm α
l : List (Perm α)
hl₁ : List.prod l = f
hl₂ : ∀ (g : Perm α), g ∈ l → IsSwap g
hsl : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = -1
⊢ ↑s f = ↑sign f
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
this : ∀ {f : Perm α}, IsSwap f → ↑s f = -1
f : Perm α
l : List (Perm α)
hl₁ : List.prod l = f
hl₂ : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ ↑s f = ↑sign f
have hsl : ∀ a ∈ l.map s, a = (-1 : ℤˣ) := fun a ha =>
  let ⟨g, hg⟩ := List.mem_map.1 ha
  hg.2 ▸ this (hl₂ _ hg.1)
no goals
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ↑s
this : ∀ {f : Perm α}, IsSwap f → ↑s f = -1
f : Perm α
l : List (Perm α)
hl₁ : List.prod l = f
hl₂ : ∀ (g : Perm α), g ∈ l → IsSwap g
hsl : ∀ (a : ℤˣ), a ∈ List.map (↑s) l → a = -1
⊢ ↑s f = ↑sign f
rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
  sign_prod_list_swap hl₂]