[GOAL]
α : Type u
β : Type v
⊢ -1 ≠ 1
[PROOFSTEP]
decide
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ : Perm α
h✝ : σ = τ ∨ σ = swap i j * τ
h : σ = swap i j * τ
⊢ τ = swap i j * σ
[PROOFSTEP]
rw [h, swap_mul_self_mul]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = τ ∨ σ = swap i j * τ
hτυ : τ = υ ∨ τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
cases' hστ with hστ hστ
[GOAL]
case inl
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = τ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
cases' hτυ with hτυ hτυ
[GOAL]
case inr
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hτυ : τ = υ ∨ τ = swap i j * υ
hστ : σ = swap i j * τ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
cases' hτυ with hτυ hτυ
[GOAL]
case inl.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
try
  rw [hστ, hτυ, swap_mul_self_mul] <;>
    simp [hστ, hτυ]
      -- porting note: should close goals, but doesn't
[GOAL]
case inl.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
rw [hστ, hτυ, swap_mul_self_mul]
[GOAL]
case inl.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
try
  rw [hστ, hτυ, swap_mul_self_mul] <;>
    simp [hστ, hτυ]
      -- porting note: should close goals, but doesn't
[GOAL]
case inl.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
rw [hστ, hτυ, swap_mul_self_mul]
[GOAL]
case inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
try
  rw [hστ, hτυ, swap_mul_self_mul] <;>
    simp [hστ, hτυ]
      -- porting note: should close goals, but doesn't
[GOAL]
case inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
rw [hστ, hτυ, swap_mul_self_mul]
[GOAL]
case inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
try
  rw [hστ, hτυ, swap_mul_self_mul] <;>
    simp [hστ, hτυ]
      -- porting note: should close goals, but doesn't
[GOAL]
case inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
rw [hστ, hτυ, swap_mul_self_mul]
[GOAL]
case inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = swap i j * υ
⊢ υ = υ ∨ υ = swap i j * υ
[PROOFSTEP]
simp [hστ, hτυ]
  -- porting note: should close goals, but doesn't
[GOAL]
case inl.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
simp [hστ, hτυ]
[GOAL]
case inl.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = τ
hτυ : τ = swap i j * υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
simp [hστ, hτυ]
[GOAL]
case inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
i j : α
σ τ υ : Perm α
hστ : σ = swap i j * τ
hτυ : τ = υ
⊢ σ = υ ∨ σ = swap i j * υ
[PROOFSTEP]
simp [hστ, hτυ]
[GOAL]
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
⊢ ↑f⁻¹ y ∈ s
[PROOFSTEP]
have h0 : ∀ y ∈ s, ∃ (x : _) (hx : x ∈ s), y = (fun i (_ : i ∈ s) => f i) x hx :=
  Finset.surj_on_of_inj_on_of_card_le (fun x hx => (fun i _ => f i) x hx) (fun a ha => h a ha)
    (fun a₁ a₂ ha₁ ha₂ heq => (Equiv.apply_eq_iff_eq f).mp heq) rfl.ge
[GOAL]
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
⊢ ↑f⁻¹ y ∈ s
[PROOFSTEP]
obtain ⟨y2, hy2, heq⟩ := h0 y hy
[GOAL]
case intro.intro
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ y ∈ s
[PROOFSTEP]
convert hy2
[GOAL]
case h.e'_4
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ y = y2
[PROOFSTEP]
rw [heq]
[GOAL]
case h.e'_4
α : Type u
β : Type v
s : Finset α
f : Perm α
h : ∀ (x : α), x ∈ s → ↑f x ∈ s
y : α
hy : y ∈ s
h0 : ∀ (y : α), y ∈ s → ∃ x hx, y = (fun i x => ↑f i) x hx
y2 : α
hy2 : y2 ∈ s
heq : y = (fun i x => ↑f i) y2 hy2
⊢ ↑f⁻¹ ((fun i x => ↑f i) y2 hy2) = y2
[PROOFSTEP]
simp only [inv_apply_self]
[GOAL]
α : Type u
β : Type v
f : Perm α
s : Set α
inst✝ : Finite ↑s
h : Set.MapsTo (↑f) s s
⊢ Set.MapsTo (↑f⁻¹) s s
[PROOFSTEP]
cases nonempty_fintype s
[GOAL]
case intro
α : Type u
β : Type v
f : Perm α
s : Set α
inst✝ : Finite ↑s
h : Set.MapsTo (↑f) s s
val✝ : Fintype ↑s
⊢ Set.MapsTo (↑f⁻¹) s s
[PROOFSTEP]
exact fun x hx =>
  Set.mem_toFinset.mp <|
    perm_inv_on_of_perm_on_finset (fun a ha => Set.mem_toFinset.mpr (h (Set.mem_toFinset.mp ha)))
      (Set.mem_toFinset.mpr hx)
[GOAL]
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
[PROOFSTEP]
cases nonempty_fintype m
[GOAL]
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝ : Fintype m
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
[PROOFSTEP]
cases nonempty_fintype n
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) ↔ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
[PROOFSTEP]
constructor
[GOAL]
case intro.intro.mp
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl) → Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
[PROOFSTEP]
intro h
[GOAL]
case intro.intro.mp
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
[PROOFSTEP]
classical
rw [← perm_inv_mapsTo_iff_mapsTo] at h
intro x
cases' hx : σ x with l r
[GOAL]
case intro.intro.mp
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
[PROOFSTEP]
rw [← perm_inv_mapsTo_iff_mapsTo] at h
[GOAL]
case intro.intro.mp
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
[PROOFSTEP]
intro x
[GOAL]
case intro.intro.mp
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
⊢ x ∈ Set.range Sum.inr → ↑σ x ∈ Set.range Sum.inr
[PROOFSTEP]
cases' hx : σ x with l r
[GOAL]
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr) → Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
[PROOFSTEP]
intro h
[GOAL]
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
[PROOFSTEP]
classical
rw [← perm_inv_mapsTo_iff_mapsTo] at h
intro x
cases' hx : σ x with l r
[GOAL]
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
[PROOFSTEP]
rw [← perm_inv_mapsTo_iff_mapsTo] at h
[GOAL]
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
⊢ Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
[PROOFSTEP]
intro x
[GOAL]
case intro.intro.mpr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
⊢ x ∈ Set.range Sum.inl → ↑σ x ∈ Set.range Sum.inl
[PROOFSTEP]
cases' hx : σ x with l r
[GOAL]
case intro.intro.mp.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inr → Sum.inl l ∈ Set.range Sum.inr
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro.intro.mp.inl.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
⊢ Sum.inl l ∈ Set.range Sum.inr
[PROOFSTEP]
obtain ⟨y, hy⟩ := h ⟨l, rfl⟩
[GOAL]
case intro.intro.mp.inl.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
y : m
hy : Sum.inl y = ↑σ⁻¹ (Sum.inl l)
⊢ Sum.inl l ∈ Set.range Sum.inr
[PROOFSTEP]
rw [← hx, σ.inv_apply_self] at hy
[GOAL]
case intro.intro.mp.inl.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
l : m
a : n
hx : ↑σ (Sum.inr a) = Sum.inl l
y : m
hy : Sum.inl y = Sum.inr a
⊢ Sum.inl l ∈ Set.range Sum.inr
[PROOFSTEP]
exact absurd hy Sum.inl_ne_inr
[GOAL]
case intro.intro.mp.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inr → Sum.inr r ∈ Set.range Sum.inr
[PROOFSTEP]
rintro _
[GOAL]
case intro.intro.mp.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inl) (Set.range Sum.inl)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
a✝ : x ∈ Set.range Sum.inr
⊢ Sum.inr r ∈ Set.range Sum.inr
[PROOFSTEP]
exact ⟨r, rfl⟩
[GOAL]
case intro.intro.mpr.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
⊢ x ∈ Set.range Sum.inl → Sum.inl l ∈ Set.range Sum.inl
[PROOFSTEP]
rintro _
[GOAL]
case intro.intro.mpr.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
l : m
hx : ↑σ x = Sum.inl l
a✝ : x ∈ Set.range Sum.inl
⊢ Sum.inl l ∈ Set.range Sum.inl
[PROOFSTEP]
exact ⟨l, rfl⟩
[GOAL]
case intro.intro.mpr.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
x : m ⊕ n
r : n
hx : ↑σ x = Sum.inr r
⊢ x ∈ Set.range Sum.inl → Sum.inr r ∈ Set.range Sum.inl
[PROOFSTEP]
rintro ⟨a, rfl⟩
[GOAL]
case intro.intro.mpr.inr.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
⊢ Sum.inr r ∈ Set.range Sum.inl
[PROOFSTEP]
obtain ⟨y, hy⟩ := h ⟨r, rfl⟩
[GOAL]
case intro.intro.mpr.inr.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
y : n
hy : Sum.inr y = ↑σ⁻¹ (Sum.inr r)
⊢ Sum.inr r ∈ Set.range Sum.inl
[PROOFSTEP]
rw [← hx, σ.inv_apply_self] at hy
[GOAL]
case intro.intro.mpr.inr.intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
val✝¹ : Fintype m
val✝ : Fintype n
h : Set.MapsTo (↑σ⁻¹) (Set.range Sum.inr) (Set.range Sum.inr)
r : n
a : m
hx : ↑σ (Sum.inl a) = Sum.inr r
y : n
hy : Sum.inr y = Sum.inl a
⊢ Sum.inr r ∈ Set.range Sum.inl
[PROOFSTEP]
exact absurd hy Sum.inr_ne_inl
[GOAL]
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
cases nonempty_fintype m
[GOAL]
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝ : Fintype m
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
cases nonempty_fintype n
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
classical
have h1 : ∀ x : Sum m n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x :=
  by
  rintro x ⟨a, ha⟩
  apply h
  rw [← ha]
  exact ⟨a, rfl⟩
have h3 : ∀ x : Sum m n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x :=
  by
  rintro x ⟨b, hb⟩
  apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
  rw [← hb]
  exact ⟨b, rfl⟩
let σ₁' := subtypePermOfFintype σ h1
let σ₂' := subtypePermOfFintype σ h3
let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
rw [MonoidHom.mem_range, Prod.exists]
use σ₁, σ₂
rw [Perm.sumCongrHom_apply]
ext x
cases' x with a b
· rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inl_injective]
  rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk, subtypePerm_apply]
· rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inr_injective]
  erw [subtypePerm_apply]
  rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
have h1 : ∀ x : Sum m n, (∃ a : m, Sum.inl a = x) → ∃ a : m, Sum.inl a = σ x :=
  by
  rintro x ⟨a, ha⟩
  apply h
  rw [← ha]
  exact ⟨a, rfl⟩
[GOAL]
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
⊢ ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
[PROOFSTEP]
rintro x ⟨a, ha⟩
[GOAL]
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ ∃ a, Sum.inl a = ↑σ x
[PROOFSTEP]
apply h
[GOAL]
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ x ∈ Set.range Sum.inl
[PROOFSTEP]
rw [← ha]
[GOAL]
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
x : m ⊕ n
a : m
ha : Sum.inl a = x
⊢ Sum.inl a ∈ Set.range Sum.inl
[PROOFSTEP]
exact ⟨a, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
have h3 : ∀ x : Sum m n, (∃ b : n, Sum.inr b = x) → ∃ b : n, Sum.inr b = σ x :=
  by
  rintro x ⟨b, hb⟩
  apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
  rw [← hb]
  exact ⟨b, rfl⟩
[GOAL]
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
⊢ ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
[PROOFSTEP]
rintro x ⟨b, hb⟩
[GOAL]
case intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ ∃ b, Sum.inr b = ↑σ x
[PROOFSTEP]
apply (perm_mapsTo_inl_iff_mapsTo_inr σ).mp h
[GOAL]
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ x ∈ Set.range Sum.inr
[PROOFSTEP]
rw [← hb]
[GOAL]
case intro.a
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
x : m ⊕ n
b : n
hb : Sum.inr b = x
⊢ Sum.inr b ∈ Set.range Sum.inr
[PROOFSTEP]
exact ⟨b, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
let σ₁' := subtypePermOfFintype σ h1
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
let σ₂' := subtypePermOfFintype σ h3
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
let σ₁ := permCongr (Equiv.ofInjective _ Sum.inl_injective).symm σ₁'
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
let σ₂ := permCongr (Equiv.ofInjective _ Sum.inr_injective).symm σ₂'
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ σ ∈ MonoidHom.range (sumCongrHom m n)
[PROOFSTEP]
rw [MonoidHom.mem_range, Prod.exists]
[GOAL]
case intro.intro
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ ∃ a b, ↑(sumCongrHom m n) (a, b) = σ
[PROOFSTEP]
use σ₁, σ₂
[GOAL]
case h
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ ↑(sumCongrHom m n) (σ₁, σ₂) = σ
[PROOFSTEP]
rw [Perm.sumCongrHom_apply]
[GOAL]
case h
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
⊢ sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd = σ
[PROOFSTEP]
ext x
[GOAL]
case h.H
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
x : m ⊕ n
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) x = ↑σ x
[PROOFSTEP]
cases' x with a b
[GOAL]
case h.H.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
a : m
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) (Sum.inl a) = ↑σ (Sum.inl a)
[PROOFSTEP]
rw [Equiv.sumCongr_apply, Sum.map_inl, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inl_injective]
[GOAL]
case h.H.inl
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
a : m
⊢ ↑(↑σ₁' (↑(ofInjective Sum.inl (_ : Injective Sum.inl)) a)) = ↑σ (Sum.inl a)
[PROOFSTEP]
rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk, subtypePerm_apply]
[GOAL]
case h.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑(sumCongr (σ₁, σ₂).fst (σ₁, σ₂).snd) (Sum.inr b) = ↑σ (Sum.inr b)
[PROOFSTEP]
rw [Equiv.sumCongr_apply, Sum.map_inr, permCongr_apply, Equiv.symm_symm, apply_ofInjective_symm Sum.inr_injective]
[GOAL]
case h.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑(↑σ₂' (↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b)) = ↑σ (Sum.inr b)
[PROOFSTEP]
erw [subtypePerm_apply]
[GOAL]
case h.H.inr
α : Type u
β : Type v
m : Type u_1
n : Type u_2
inst✝¹ : Finite m
inst✝ : Finite n
σ : Perm (m ⊕ n)
h : Set.MapsTo (↑σ) (Set.range Sum.inl) (Set.range Sum.inl)
val✝¹ : Fintype m
val✝ : Fintype n
h1 : ∀ (x : m ⊕ n), (∃ a, Sum.inl a = x) → ∃ a, Sum.inl a = ↑σ x
h3 : ∀ (x : m ⊕ n), (∃ b, Sum.inr b = x) → ∃ b, Sum.inr b = ↑σ x
σ₁' : Perm { x // ∃ a, Sum.inl a = x } := subtypePermOfFintype σ h1
σ₂' : Perm { x // ∃ b, Sum.inr b = x } := subtypePermOfFintype σ h3
σ₁ : (fun x => Perm m) σ₁' := ↑(permCongr (ofInjective Sum.inl (_ : Injective Sum.inl)).symm) σ₁'
σ₂ : (fun x => Perm n) σ₂' := ↑(permCongr (ofInjective Sum.inr (_ : Injective Sum.inr)).symm) σ₂'
b : n
⊢ ↑{ val := ↑σ ↑(↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b),
        property := (_ : (fun x => ∃ b, Sum.inr b = x) (↑σ ↑(↑(ofInjective Sum.inr (_ : Injective Sum.inr)) b))) } =
    ↑σ (Sum.inr b)
[PROOFSTEP]
rw [ofInjective_apply, Subtype.coe_mk, Subtype.coe_mk]
[GOAL]
α : Type u
β : Type v
σ τ : Perm α
hστ : Disjoint σ τ
n : ℕ
⊢ (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1
[PROOFSTEP]
rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
⊢ Disjoint (Perm.extendDomain σ f) (Perm.extendDomain τ f)
[PROOFSTEP]
intro b
[GOAL]
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
⊢ ↑(Perm.extendDomain σ f) b = b ∨ ↑(Perm.extendDomain τ f) b = b
[PROOFSTEP]
by_cases pb : p b
[GOAL]
case pos
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : p b
⊢ ↑(Perm.extendDomain σ f) b = b ∨ ↑(Perm.extendDomain τ f) b = b
[PROOFSTEP]
refine' (h (f.symm ⟨b, pb⟩)).imp _ _
[GOAL]
case pos.refine'_1
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : p b
⊢ ↑σ (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb } → ↑(Perm.extendDomain σ f) b = b
[PROOFSTEP]
intro h
[GOAL]
case pos.refine'_1
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h✝ : Disjoint σ τ
b : β
pb : p b
h : ↑σ (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
⊢ ↑(Perm.extendDomain σ f) b = b
[PROOFSTEP]
rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
[GOAL]
case pos.refine'_2
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : p b
⊢ ↑τ (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb } → ↑(Perm.extendDomain τ f) b = b
[PROOFSTEP]
intro h
[GOAL]
case pos.refine'_2
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h✝ : Disjoint σ τ
b : β
pb : p b
h : ↑τ (↑f.symm { val := b, property := pb }) = ↑f.symm { val := b, property := pb }
⊢ ↑(Perm.extendDomain τ f) b = b
[PROOFSTEP]
rw [extendDomain_apply_subtype _ _ pb, h, apply_symm_apply, Subtype.coe_mk]
[GOAL]
case neg
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : ¬p b
⊢ ↑(Perm.extendDomain σ f) b = b ∨ ↑(Perm.extendDomain τ f) b = b
[PROOFSTEP]
left
[GOAL]
case neg.h
α✝ : Type u
β : Type v
α : Type u_1
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
σ τ : Perm α
h : Disjoint σ τ
b : β
pb : ¬p b
⊢ ↑(Perm.extendDomain σ f) b = b
[PROOFSTEP]
rw [extendDomain_apply_not_subtype _ _ pb]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : Nat.coprime n (orderOf σ)
⊢ support (σ ^ n) = support σ
[PROOFSTEP]
obtain ⟨m, hm⟩ := exists_pow_eq_self_of_coprime h
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
n : ℕ
h : Nat.coprime n (orderOf σ)
m : ℕ
hm : (σ ^ n) ^ m = σ
⊢ support (σ ^ n) = support σ
[PROOFSTEP]
exact le_antisymm (support_pow_le σ n) (le_trans (ge_of_eq (congr_arg support hm)) (support_pow_le (σ ^ n) m))
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
h : ∀ {x : α}, ↑f x ≠ x → x ∈ []
x : α
⊢ ↑(List.prod []) x = ↑f x
[PROOFSTEP]
rw [List.prod_nil]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
h : ∀ {x : α}, ↑f x ≠ x → x ∈ []
x : α
⊢ ↑1 x = ↑f x
[PROOFSTEP]
exact (Classical.not_not.1 (mt h (List.not_mem_nil _))).symm
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
f : Perm α
h : ∀ {x : α}, ↑f x ≠ x → x ∈ []
⊢ ∀ (g : Perm α), g ∈ [] → IsSwap g
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
x : α
l : List α
f : Perm α
h✝ : ∀ {x_1 : α}, ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
y : α
hy : ↑f y ≠ y
h : y = x
⊢ False
[PROOFSTEP]
simp [h, hfx.symm] at hy
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
x : α
l : List α
f : Perm α
h : ∀ {x_1 : α}, ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
m : { l // List.prod l = swap x (↑f x) * f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g } :=
  swapFactorsAux l (swap x (↑f x) * f) (_ : ∀ {y : α}, ↑(swap x (↑f x) * f) y ≠ y → y ∈ l)
⊢ List.prod (swap x (↑f x) :: ↑m) = f
[PROOFSTEP]
rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def, one_mul]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
val✝ : Fintype α
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
[PROOFSTEP]
cases' (truncSwapFactors f).out with l hl
[GOAL]
case intro.mk
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f : Perm α
val✝ : Fintype α
l : List (Perm α)
hl : List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
[PROOFSTEP]
induction' l with g l ih generalizing f
[GOAL]
case intro.mk.nil
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l : List (Perm α)
hl✝ : List.prod l = f✝ ∧ ∀ (g : Perm α), g ∈ l → IsSwap g
f : Perm α
hl : List.prod [] = f ∧ ∀ (g : Perm α), g ∈ [] → IsSwap g
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
[PROOFSTEP]
simp (config := { contextual := true }) only [hl.left.symm, List.prod_nil, forall_true_iff]
[GOAL]
case intro.mk.cons
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
⊢ P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
[PROOFSTEP]
intro h1 hmul_swap
[GOAL]
case intro.mk.cons
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
⊢ P f
[PROOFSTEP]
rcases hl.2 g (by simp) with ⟨x, y, hxy⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
⊢ g ∈ g :: l
[PROOFSTEP]
simp
[GOAL]
case intro.mk.cons.intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ P f
[PROOFSTEP]
rw [← hl.1, List.prod_cons, hxy.2]
[GOAL]
case intro.mk.cons.intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
P : Perm α → Prop
f✝ : Perm α
val✝ : Fintype α
l✝ : List (Perm α)
hl✝ : List.prod l✝ = f✝ ∧ ∀ (g : Perm α), g ∈ l✝ → IsSwap g
g : Perm α
l : List (Perm α)
ih :
  ∀ (f : Perm α),
    (List.prod l = f ∧ ∀ (g : Perm α), g ∈ l → IsSwap g) →
      P 1 → (∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)) → P f
f : Perm α
hl : List.prod (g :: l) = f ∧ ∀ (g_1 : Perm α), g_1 ∈ g :: l → IsSwap g_1
h1 : P 1
hmul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → P f → P (swap x y * f)
x y : α
hxy : x ≠ y ∧ g = swap x y
⊢ P (swap x y * List.prod l)
[PROOFSTEP]
exact hmul_swap _ _ _ hxy.1 (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩ h1 hmul_swap)
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
⊢ Subgroup.closure {σ | IsSwap σ} = ⊤
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
⊢ Subgroup.closure {σ | IsSwap σ} = ⊤
[PROOFSTEP]
refine' eq_top_iff.mpr fun x _ => _
[GOAL]
case intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
⊢ x ∈ Subgroup.closure {σ | IsSwap σ}
[PROOFSTEP]
obtain ⟨h1, h2⟩ := Subtype.mem (truncSwapFactors x).out
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : List.prod ↑(Trunc.out (truncSwapFactors x)) = x
h2 : ∀ (g : Perm α), g ∈ ↑(Trunc.out (truncSwapFactors x)) → IsSwap g
⊢ x ∈ Subgroup.closure {σ | IsSwap σ}
[PROOFSTEP]
rw [← h1]
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Finite α
val✝ : Fintype α
x : Perm α
x✝ : x ∈ ⊤
h1 : List.prod ↑(Trunc.out (truncSwapFactors x)) = x
h2 : ∀ (g : Perm α), g ∈ ↑(Trunc.out (truncSwapFactors x)) → IsSwap g
⊢ List.prod ↑(Trunc.out (truncSwapFactors x)) ∈ Subgroup.closure {σ | IsSwap σ}
[PROOFSTEP]
exact Subgroup.list_prod_mem _ fun y hy => Subgroup.subset_closure (h2 y hy)
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
w x y✝ z✝ : α
hwx : w ≠ x
hyz✝ : y✝ ≠ z✝
y z : α
hyz : y ≠ z
hwz : w ≠ z
⊢ swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
[PROOFSTEP]
rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ← mul_assoc _ (swap x z),
  swap_mul_swap_mul_swap hwx hwz, ← mul_assoc, swap_mul_swap_mul_swap hwz.symm hyz.symm]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ w ≠ y
[PROOFSTEP]
rw [hwz]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
⊢ z ≠ y
[PROOFSTEP]
exact hyz.symm
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
w x y z : α
hwx : w ≠ x
hyz : y ≠ z
h : ∀ {y z : α}, y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z
hwz : w = z
hwy : w ≠ y
⊢ swap w z * swap x y * swap w x * (swap w z * swap x y)⁻¹ = swap y z
[PROOFSTEP]
rw [swap_comm y z, h hyz.symm hwy]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a : (_ : Fin n) × Fin n
⊢ a ∈ finPairsLT n ↔ a.snd < a.fst
[PROOFSTEP]
simp only [finPairsLT, Fin.lt_iff_val_lt_val, true_and_iff, mem_attachFin, mem_range, mem_univ, mem_sigma]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ signAux 1 = 1
[PROOFSTEP]
unfold signAux
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = 1
[PROOFSTEP]
conv => rhs; rw [← @Finset.prod_const_one ℤˣ _ (finPairsLT n)]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
| (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = 1
[PROOFSTEP]
rhs; rw [← @Finset.prod_const_one ℤˣ _ (finPairsLT n)]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
| (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = 1
[PROOFSTEP]
rhs; rw [← @Finset.prod_const_one ℤˣ _ (finPairsLT n)]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
| (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = 1
[PROOFSTEP]
rhs
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
| 1
[PROOFSTEP]
rw [← @Finset.prod_const_one ℤˣ _ (finPairsLT n)]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ (∏ x in finPairsLT n, if ↑1 x.fst ≤ ↑1 x.snd then -1 else 1) = ∏ _x in finPairsLT n, 1
[PROOFSTEP]
exact Finset.prod_congr rfl fun a ha => if_neg (mem_finPairsLT.1 ha).not_le
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ } ∈ finPairsLT n
h : signBijAux f { fst := a₁, snd := a₂ } = signBijAux f { fst := b₁, snd := b₂ }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
[PROOFSTEP]
unfold signBijAux at h
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ } ∈ finPairsLT n
h :
  (if x : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst then
      { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd }
    else { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
[PROOFSTEP]
rw [mem_finPairsLT] at *
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
h :
  (if x : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst then
      { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd }
    else { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
[PROOFSTEP]
have : ¬b₁ < b₂ := hb.le.not_lt
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
h :
  (if x : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst then
      { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd }
    else { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst }) =
    if x : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst then
      { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
    else { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
this : ¬b₁ < b₂
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
[PROOFSTEP]
split_ifs at h
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
this : ¬b₁ < b₂
h✝¹ : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
h✝ : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst
h :
  { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd } =
    { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
[PROOFSTEP]
simp_all [(Equiv.injective f).eq_iff, eq_self_iff_true, and_self_iff, heq_iff_eq]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
this : ¬b₁ < b₂
h✝¹ : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
h✝ : ¬↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst
h :
  { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd } =
    { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
[PROOFSTEP]
simp_all [(Equiv.injective f).eq_iff, eq_self_iff_true, and_self_iff, heq_iff_eq]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
this : ¬b₁ < b₂
h✝¹ : ¬↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
h✝ : ↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst
h :
  { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst } =
    { fst := ↑f { fst := b₁, snd := b₂ }.fst, snd := ↑f { fst := b₁, snd := b₂ }.snd }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
[PROOFSTEP]
simp_all [(Equiv.injective f).eq_iff, eq_self_iff_true, and_self_iff, heq_iff_eq]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ }.snd < { fst := a₁, snd := a₂ }.fst
b₁ b₂ : Fin n
hb : { fst := b₁, snd := b₂ }.snd < { fst := b₁, snd := b₂ }.fst
this : ¬b₁ < b₂
h✝¹ : ¬↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
h✝ : ¬↑f { fst := b₁, snd := b₂ }.snd < ↑f { fst := b₁, snd := b₂ }.fst
h :
  { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst } =
    { fst := ↑f { fst := b₁, snd := b₂ }.snd, snd := ↑f { fst := b₁, snd := b₂ }.fst }
⊢ { fst := a₁, snd := a₂ } = { fst := b₁, snd := b₂ }
[PROOFSTEP]
simp_all [(Equiv.injective f).eq_iff, eq_self_iff_true, and_self_iff, heq_iff_eq]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₁ < ↑f b₂
h✝ : ↑f b₁ ≤ ↑f b₂
h : a₁ = b₂ ∧ a₂ = b₁
⊢ b₂ = b₁ ∧ b₁ = b₂
[PROOFSTEP]
exact absurd this (not_le.mpr ha)
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝¹ x✝ : (_ : Fin n) × Fin n
a₁ a₂ b₁ b₂ : Fin n
ha : b₁ < b₂
hb : b₂ < b₁
this : b₂ ≤ b₁
h✝¹ : ↑f b₂ ≤ ↑f b₁
h✝ : ↑f b₂ < ↑f b₁
h : a₂ = b₁ ∧ a₁ = b₂
⊢ b₂ = b₁ ∧ b₁ = b₂
[PROOFSTEP]
exact absurd this (not_le.mpr ha)
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
hxa : ↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } = signBijAux f { fst := ↑f⁻¹ a₁, snd := ↑f⁻¹ a₂ }
[PROOFSTEP]
dsimp [signBijAux]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
hxa : ↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } =
    if ↑f (↑f⁻¹ a₂) < ↑f (↑f⁻¹ a₁) then { fst := ↑f (↑f⁻¹ a₁), snd := ↑f (↑f⁻¹ a₂) }
    else { fst := ↑f (↑f⁻¹ a₂), snd := ↑f (↑f⁻¹ a₁) }
[PROOFSTEP]
rw [apply_inv_self, apply_inv_self, if_pos (mem_finPairsLT.1 ha)]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
hxa : ¬↑f⁻¹ a₂ < ↑f⁻¹ a₁
h : ↑f⁻¹ a₁ = ↑f⁻¹ a₂
⊢ False
[PROOFSTEP]
simp [mem_finPairsLT, f⁻¹.injective h, lt_irrefl] at ha
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
hxa : ¬↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } = signBijAux f { fst := ↑f⁻¹ a₂, snd := ↑f⁻¹ a₁ }
[PROOFSTEP]
dsimp [signBijAux]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
hxa : ¬↑f⁻¹ a₂ < ↑f⁻¹ a₁
⊢ { fst := a₁, snd := a₂ } =
    if ↑f (↑f⁻¹ a₁) < ↑f (↑f⁻¹ a₂) then { fst := ↑f (↑f⁻¹ a₂), snd := ↑f (↑f⁻¹ a₁) }
    else { fst := ↑f (↑f⁻¹ a₁), snd := ↑f (↑f⁻¹ a₂) }
[PROOFSTEP]
rw [apply_inv_self, apply_inv_self, if_neg (mem_finPairsLT.1 ha).le.not_lt]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
⊢ signBijAux f { fst := a₁, snd := a₂ } ∈ finPairsLT n
[PROOFSTEP]
unfold signBijAux
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
⊢ (if x : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst then
      { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd }
    else { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst }) ∈
    finPairsLT n
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
h : ↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
⊢ { fst := ↑f { fst := a₁, snd := a₂ }.fst, snd := ↑f { fst := a₁, snd := a₂ }.snd } ∈ finPairsLT n
[PROOFSTEP]
exact mem_finPairsLT.2 h
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a₁ a₂ : Fin n
ha : { fst := a₁, snd := a₂ } ∈ finPairsLT n
h : ¬↑f { fst := a₁, snd := a₂ }.snd < ↑f { fst := a₁, snd := a₂ }.fst
⊢ { fst := ↑f { fst := a₁, snd := a₂ }.snd, snd := ↑f { fst := a₁, snd := a₂ }.fst } ∈ finPairsLT n
[PROOFSTEP]
exact mem_finPairsLT.2 ((le_of_not_gt h).lt_of_ne fun h => (mem_finPairsLT.1 ha).ne (f.injective h.symm))
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ b < ↑f⁻¹ a
⊢ (if ↑f⁻¹ { fst := a, snd := b }.fst ≤ ↑f⁻¹ { fst := a, snd := b }.snd then -1 else 1) =
    if
        ↑f ((fun a x => signBijAux f⁻¹ a) { fst := a, snd := b } hab).fst ≤
          ↑f ((fun a x => signBijAux f⁻¹ a) { fst := a, snd := b } hab).snd then
      -1
    else 1
[PROOFSTEP]
simp_all [signBijAux, dif_pos h, if_neg h.not_le, apply_inv_self, apply_inv_self, if_neg (mem_finPairsLT.1 hab).not_le]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ b < ↑f⁻¹ a
⊢ 1 = if a ≤ b then -1 else 1
[PROOFSTEP]
split_ifs with h₁
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ b < ↑f⁻¹ a
h₁ : a ≤ b
⊢ 1 = -1
[PROOFSTEP]
dsimp [finPairsLT] at hab
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ Finset.sigma univ fun a => attachFin (range ↑a) (_ : ∀ (x : ℕ), x ∈ range ↑a → x < n)
h : ↑f⁻¹ b < ↑f⁻¹ a
h₁ : a ≤ b
⊢ 1 = -1
[PROOFSTEP]
simp at hab
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
h : ↑f⁻¹ b < ↑f⁻¹ a
h₁ : a ≤ b
hab : b < a
⊢ 1 = -1
[PROOFSTEP]
exact absurd h₁ (not_le_of_gt hab)
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ b < ↑f⁻¹ a
h₁ : ¬a ≤ b
⊢ 1 = 1
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ¬↑f⁻¹ b < ↑f⁻¹ a
⊢ (if ↑f⁻¹ { fst := a, snd := b }.fst ≤ ↑f⁻¹ { fst := a, snd := b }.snd then -1 else 1) =
    if
        ↑f ((fun a x => signBijAux f⁻¹ a) { fst := a, snd := b } hab).fst ≤
          ↑f ((fun a x => signBijAux f⁻¹ a) { fst := a, snd := b } hab).snd then
      -1
    else 1
[PROOFSTEP]
simp_all [signBijAux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self, apply_inv_self,
  if_pos (mem_finPairsLT.1 hab).le]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ a ≤ ↑f⁻¹ b
⊢ -1 =
    if
        ↑f (if ↑f⁻¹ b < ↑f⁻¹ a then { fst := ↑f⁻¹ a, snd := ↑f⁻¹ b } else { fst := ↑f⁻¹ b, snd := ↑f⁻¹ a }).fst ≤
          ↑f (if ↑f⁻¹ b < ↑f⁻¹ a then { fst := ↑f⁻¹ a, snd := ↑f⁻¹ b } else { fst := ↑f⁻¹ b, snd := ↑f⁻¹ a }).snd then
      -1
    else 1
[PROOFSTEP]
split_ifs with h₁ h₂ h₃
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ a ≤ ↑f⁻¹ b
h₁ : ↑f⁻¹ b < ↑f⁻¹ a
h₂ : ↑f { fst := ↑f⁻¹ a, snd := ↑f⁻¹ b }.fst ≤ ↑f { fst := ↑f⁻¹ a, snd := ↑f⁻¹ b }.snd
⊢ -1 = -1
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ a ≤ ↑f⁻¹ b
h₁ : ↑f⁻¹ b < ↑f⁻¹ a
h₂ : ¬↑f { fst := ↑f⁻¹ a, snd := ↑f⁻¹ b }.fst ≤ ↑f { fst := ↑f⁻¹ a, snd := ↑f⁻¹ b }.snd
⊢ -1 = 1
[PROOFSTEP]
exact absurd h (not_le_of_gt h₁)
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ a ≤ ↑f⁻¹ b
h₁ : ¬↑f⁻¹ b < ↑f⁻¹ a
h₃ : ↑f { fst := ↑f⁻¹ b, snd := ↑f⁻¹ a }.fst ≤ ↑f { fst := ↑f⁻¹ b, snd := ↑f⁻¹ a }.snd
⊢ -1 = -1
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ a ≤ ↑f⁻¹ b
h₁ : ¬↑f⁻¹ b < ↑f⁻¹ a
h₃ : ¬↑f { fst := ↑f⁻¹ b, snd := ↑f⁻¹ a }.fst ≤ ↑f { fst := ↑f⁻¹ b, snd := ↑f⁻¹ a }.snd
⊢ -1 = 1
[PROOFSTEP]
dsimp at *
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
h : ↑f⁻¹ a ≤ ↑f⁻¹ b
h₁ : ¬↑f⁻¹ b < ↑f⁻¹ a
h₃ : ¬↑f (↑f⁻¹ b) ≤ ↑f (↑f⁻¹ a)
⊢ -1 = 1
[PROOFSTEP]
dsimp [finPairsLT] at hab
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
hab : { fst := a, snd := b } ∈ Finset.sigma univ fun a => attachFin (range ↑a) (_ : ∀ (x : ℕ), x ∈ range ↑a → x < n)
h : ↑f⁻¹ a ≤ ↑f⁻¹ b
h₁ : ¬↑f⁻¹ b < ↑f⁻¹ a
h₃ : ¬↑f (↑f⁻¹ b) ≤ ↑f (↑f⁻¹ a)
⊢ -1 = 1
[PROOFSTEP]
simp at *
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm (Fin n)
x✝ : (_ : Fin n) × Fin n
a b : Fin n
h : ↑f⁻¹ a ≤ ↑f⁻¹ b
hab : b < a
h₁ : ↑f⁻¹ a ≤ ↑f⁻¹ b
h₃ : a < b
⊢ False
[PROOFSTEP]
exact absurd h₃ (asymm_of LT.lt hab)
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ signAux (f * g) = signAux f * signAux g
[PROOFSTEP]
rw [← signAux_inv g]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ signAux (f * g) = signAux f * signAux g⁻¹
[PROOFSTEP]
unfold signAux
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x in finPairsLT n, if ↑(f * g) x.fst ≤ ↑(f * g) x.snd then -1 else 1) =
    (∏ x in finPairsLT n, if ↑f x.fst ≤ ↑f x.snd then -1 else 1) *
      ∏ x in finPairsLT n, if ↑g⁻¹ x.fst ≤ ↑g⁻¹ x.snd then -1 else 1
[PROOFSTEP]
rw [← prod_mul_distrib]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ (∏ x in finPairsLT n, if ↑(f * g) x.fst ≤ ↑(f * g) x.snd then -1 else 1) =
    ∏ x in finPairsLT n, (if ↑f x.fst ≤ ↑f x.snd then -1 else 1) * if ↑g⁻¹ x.fst ≤ ↑g⁻¹ x.snd then -1 else 1
[PROOFSTEP]
refine' prod_bij (fun a _ => signBijAux g a) signBijAux_mem _ signBijAux_inj (by simpa using signBijAux_surj)
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ ∀ (b : (_ : Fin n) × Fin n), b ∈ finPairsLT n → ∃ a ha, b = (fun a x => signBijAux g a) a ha
[PROOFSTEP]
simpa using signBijAux_surj
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
⊢ ∀ (a : (_ : Fin n) × Fin n) (ha : a ∈ finPairsLT n),
    (if ↑(f * g) a.fst ≤ ↑(f * g) a.snd then -1 else 1) =
      (if ↑f ((fun a x => signBijAux g a) a ha).fst ≤ ↑f ((fun a x => signBijAux g a) a ha).snd then -1 else 1) *
        if ↑g⁻¹ ((fun a x => signBijAux g a) a ha).fst ≤ ↑g⁻¹ ((fun a x => signBijAux g a) a ha).snd then -1 else 1
[PROOFSTEP]
rintro ⟨a, b⟩ hab
[GOAL]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑(f * g) { fst := a, snd := b }.fst ≤ ↑(f * g) { fst := a, snd := b }.snd then -1 else 1) =
    (if
          ↑f ((fun a x => signBijAux g a) { fst := a, snd := b } hab).fst ≤
            ↑f ((fun a x => signBijAux g a) { fst := a, snd := b } hab).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ ((fun a x => signBijAux g a) { fst := a, snd := b } hab).fst ≤
            ↑g⁻¹ ((fun a x => signBijAux g a) { fst := a, snd := b } hab).snd then
        -1
      else 1
[PROOFSTEP]
dsimp only [signBijAux]
[GOAL]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑(f * g) a ≤ ↑(f * g) b then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
[PROOFSTEP]
rw [mul_apply, mul_apply]
[GOAL]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b } ∈ finPairsLT n
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
[PROOFSTEP]
rw [mem_finPairsLT] at hab
[GOAL]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
[PROOFSTEP]
by_cases h : g b < g a
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
[PROOFSTEP]
rw [dif_pos h]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g a, snd := ↑g b }.fst ≤ ↑f { fst := ↑g a, snd := ↑g b }.snd then -1 else 1) *
      if ↑g⁻¹ { fst := ↑g a, snd := ↑g b }.fst ≤ ↑g⁻¹ { fst := ↑g a, snd := ↑g b }.snd then -1 else 1
[PROOFSTEP]
simp only [not_le_of_gt hab, mul_one, mul_ite, mul_neg, Perm.inv_apply_self, if_false]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    if a ≤ b then -if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1 else if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1
[PROOFSTEP]
split_ifs with h₁ h₂ h₃
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
h₁ : ↑f (↑g a) ≤ ↑f (↑g b)
h₂ : a ≤ b
⊢ -1 = - -1
[PROOFSTEP]
dsimp at *
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
h₁ : ↑f (↑g a) ≤ ↑f (↑g b)
h₂ : ¬a ≤ b
⊢ -1 = -1
[PROOFSTEP]
dsimp at *
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
h₁ : ¬↑f (↑g a) ≤ ↑f (↑g b)
h₃ : a ≤ b
⊢ 1 = -1
[PROOFSTEP]
dsimp at *
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ↑g b < ↑g a
h₁ : ¬↑f (↑g a) ≤ ↑f (↑g b)
h₃ : ¬a ≤ b
⊢ 1 = 1
[PROOFSTEP]
dsimp at *
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ↑f (↑g a) ≤ ↑f (↑g b)
h₂ : a ≤ b
⊢ -1 = - -1
[PROOFSTEP]
exact absurd hab (not_lt_of_ge h₂)
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : b < a
h : ↑g b < ↑g a
h₁ : ¬↑f (↑g a) ≤ ↑f (↑g b)
h₃ : a ≤ b
⊢ 1 = -1
[PROOFSTEP]
exact absurd hab (not_lt_of_ge h₃)
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if
          ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑f (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1) *
      if
          ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).fst ≤
            ↑g⁻¹ (if x : ↑g b < ↑g a then { fst := ↑g a, snd := ↑g b } else { fst := ↑g b, snd := ↑g a }).snd then
        -1
      else 1
[PROOFSTEP]
rw [dif_neg h, inv_apply_self, inv_apply_self, if_pos hab.le]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
[PROOFSTEP]
by_cases h₁ : f (g b) ≤ f (g a)
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
[PROOFSTEP]
have : f (g b) ≠ f (g a) := by
  rw [Ne.def, f.injective.eq_iff, g.injective.eq_iff]
  exact ne_of_lt hab
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
⊢ ↑f (↑g b) ≠ ↑f (↑g a)
[PROOFSTEP]
rw [Ne.def, f.injective.eq_iff, g.injective.eq_iff]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
⊢ ¬b = a
[PROOFSTEP]
exact ne_of_lt hab
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
this : ↑f (↑g b) ≠ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
[PROOFSTEP]
rw [if_pos h₁, if_neg (h₁.lt_of_ne this).not_le]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ↑f (↑g b) ≤ ↑f (↑g a)
this : ↑f (↑g b) ≠ ↑f (↑g a)
⊢ 1 = -1 * -1
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ¬↑f (↑g b) ≤ ↑f (↑g a)
⊢ (if ↑f (↑g a) ≤ ↑f (↑g b) then -1 else 1) =
    (if ↑f { fst := ↑g b, snd := ↑g a }.fst ≤ ↑f { fst := ↑g b, snd := ↑g a }.snd then -1 else 1) * -1
[PROOFSTEP]
rw [if_neg h₁, if_pos (lt_of_not_ge h₁).le]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f g : Perm (Fin n)
a b : Fin n
hab : { fst := a, snd := b }.snd < { fst := a, snd := b }.fst
h : ¬↑g b < ↑g a
h₁ : ¬↑f (↑g b) ≤ ↑f (↑g a)
⊢ -1 = 1 * -1
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
⊢ signAux (swap 0 1) = ∏ x in {{ fst := 1, snd := 0 }}, if ↑(swap 0 1) x.fst ≤ ↑(swap 0 1) x.snd then -1 else 1
[PROOFSTEP]
refine'
  Eq.symm
    (prod_subset (fun ⟨x₁, x₂⟩ => by simp (config := { contextual := true }) [mem_finPairsLT, Fin.one_pos])
      fun a ha₁ ha₂ => _)
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x✝ : (_ : Fin (n + 2)) × Fin (n + 2)
x₁ x₂ : Fin (n + 2)
⊢ { fst := x₁, snd := x₂ } ∈ {{ fst := 1, snd := 0 }} → { fst := x₁, snd := x₂ } ∈ finPairsLT (n + 2)
[PROOFSTEP]
simp (config := { contextual := true }) [mem_finPairsLT, Fin.one_pos]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a : (_ : Fin (n + 2)) × Fin (n + 2)
ha₁ : a ∈ finPairsLT (n + 2)
ha₂ : ¬a ∈ {{ fst := 1, snd := 0 }}
⊢ (if ↑(swap 0 1) a.fst ≤ ↑(swap 0 1) a.snd then -1 else 1) = 1
[PROOFSTEP]
rcases a with ⟨a₁, a₂⟩
[GOAL]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₁ : { fst := a₁, snd := a₂ } ∈ finPairsLT (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
⊢ (if ↑(swap 0 1) { fst := a₁, snd := a₂ }.fst ≤ ↑(swap 0 1) { fst := a₁, snd := a₂ }.snd then -1 else 1) = 1
[PROOFSTEP]
replace ha₁ : a₂ < a₁ := mem_finPairsLT.1 ha₁
[GOAL]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
⊢ (if ↑(swap 0 1) { fst := a₁, snd := a₂ }.fst ≤ ↑(swap 0 1) { fst := a₁, snd := a₂ }.snd then -1 else 1) = 1
[PROOFSTEP]
dsimp only
[GOAL]
case mk
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
[PROOFSTEP]
rcases a₁.zero_le.eq_or_lt with (rfl | H)
[GOAL]
case mk.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₂ : Fin (n + 2)
ha₂ : ¬{ fst := 0, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < 0
⊢ (if ↑(swap 0 1) 0 ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
[PROOFSTEP]
exact absurd a₂.zero_le ha₁.not_le
[GOAL]
case mk.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
[PROOFSTEP]
rcases a₂.zero_le.eq_or_lt with (rfl | H')
[GOAL]
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₂ : ¬{ fst := a₁, snd := 0 } ∈ {{ fst := 1, snd := 0 }}
ha₁ : 0 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
[PROOFSTEP]
simp only [and_true_iff, eq_self_iff_true, heq_iff_eq, mem_singleton, Sigma.mk.inj_iff] at ha₂
[GOAL]
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
[PROOFSTEP]
have : 1 < a₁ := lt_of_le_of_ne (Nat.succ_le_of_lt ha₁) (Ne.symm (by intro h; apply ha₂; simp [h]))
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
⊢ a₁ ≠ 1
[PROOFSTEP]
intro h
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
h : a₁ = 1
⊢ False
[PROOFSTEP]
apply ha₂
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
h : a₁ = 1
⊢ a₁ = 1
[PROOFSTEP]
simp [h]
[GOAL]
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
[PROOFSTEP]
have h01 : Equiv.swap (0 : Fin (n + 2)) 1 0 = 1 := by
  simp
    -- Porting note: replaced `norm_num` by `rw`
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
⊢ ↑(swap 0 1) 0 = 1
[PROOFSTEP]
simp
  -- Porting note: replaced `norm_num` by `rw`
[GOAL]
case mk.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
ha₁ : 0 < a₁
ha₂ : ¬a₁ = 1
this : 1 < a₁
h01 : ↑(swap 0 1) 0 = 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 0 then -1 else 1) = 1
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne (ne_of_gt H) ha₂, h01, if_neg this.not_le]
[GOAL]
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
[PROOFSTEP]
have le : 1 ≤ a₂ := Nat.succ_le_of_lt H'
[GOAL]
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
[PROOFSTEP]
have lt : 1 < a₁ := le.trans_lt ha₁
[GOAL]
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
[PROOFSTEP]
have h01 : Equiv.swap (0 : Fin (n + 2)) 1 1 = 0 := by simp only [swap_apply_right]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
⊢ ↑(swap 0 1) 1 = 0
[PROOFSTEP]
simp only [swap_apply_right]
[GOAL]
case mk.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
[PROOFSTEP]
rcases le.eq_or_lt with (rfl | lt')
[GOAL]
case mk.inr.inr.inl
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ : Fin (n + 2)
H : 0 < a₁
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
ha₂ : ¬{ fst := a₁, snd := 1 } ∈ {{ fst := 1, snd := 0 }}
ha₁ : 1 < a₁
H' : 0 < 1
le : 1 ≤ 1
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) 1 then -1 else 1) = 1
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne H.ne' lt.ne', h01, if_neg H.not_le]
[GOAL]
case mk.inr.inr.inr
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
a₁ a₂ : Fin (n + 2)
ha₂ : ¬{ fst := a₁, snd := a₂ } ∈ {{ fst := 1, snd := 0 }}
ha₁ : a₂ < a₁
H : 0 < a₁
H' : 0 < a₂
le : 1 ≤ a₂
lt : 1 < a₁
h01 : ↑(swap 0 1) 1 = 0
lt' : 1 < a₂
⊢ (if ↑(swap 0 1) a₁ ≤ ↑(swap 0 1) a₂ then -1 else 1) = 1
[PROOFSTEP]
rw [swap_apply_of_ne_of_ne (ne_of_gt H) (ne_of_gt lt), swap_apply_of_ne_of_ne (ne_of_gt H') (ne_of_gt lt'),
  if_neg ha₁.not_le]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
⊢ 0 < 2
[PROOFSTEP]
decide
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
⊢ 1 < 2
[PROOFSTEP]
decide
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ n
⊢ signAux (swap { val := 0, isLt := (_ : 0 < n) } { val := 1, isLt := (_ : 1 < n) }) = -1
[PROOFSTEP]
rcases n with (_ | _ | n)
[GOAL]
case zero
α : Type u
β : Type v
inst✝ : DecidableEq α
hn : 2 ≤ Nat.zero
⊢ signAux (swap { val := 0, isLt := (_ : 0 < Nat.zero) } { val := 1, isLt := (_ : 1 < Nat.zero) }) = -1
[PROOFSTEP]
norm_num at hn
[GOAL]
case succ.zero
α : Type u
β : Type v
inst✝ : DecidableEq α
hn : 2 ≤ Nat.succ Nat.zero
⊢ signAux (swap { val := 0, isLt := (_ : 0 < Nat.succ Nat.zero) } { val := 1, isLt := (_ : 1 < Nat.succ Nat.zero) }) =
    -1
[PROOFSTEP]
norm_num at hn
[GOAL]
case succ.succ
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
hn : 2 ≤ Nat.succ (Nat.succ n)
⊢ signAux
      (swap { val := 0, isLt := (_ : 0 < Nat.succ (Nat.succ n)) }
        { val := 1, isLt := (_ : 1 < Nat.succ (Nat.succ n)) }) =
    -1
[PROOFSTEP]
exact signAux_swap_zero_one' n
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 0
⊢ x ≠ y → signAux (swap x y) = -1
[PROOFSTEP]
intro
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 0
_hxy✝ : x ≠ y
⊢ signAux (swap x y) = -1
[PROOFSTEP]
exact Fin.elim0 x
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 1
⊢ x ≠ y → signAux (swap x y) = -1
[PROOFSTEP]
dsimp [signAux, swap, swapCore]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
x y : Fin 1
⊢ ¬x = y →
    (∏ x_1 in finPairsLT 1,
        if
            (if x_1.fst = x then y else if x_1.fst = y then x else x_1.fst) ≤
              if x_1.snd = x then y else if x_1.snd = y then x else x_1.snd then
          -1
        else 1) =
      -1
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton, not_true, ite_true, le_refl, prod_const, IsEmpty.forall_iff]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ signAux (swap x y) = -1
[PROOFSTEP]
have h2n : 2 ≤ n + 2 := by exact le_add_self
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
⊢ 2 ≤ n + 2
[PROOFSTEP]
exact le_add_self
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ signAux (swap x y) = -1
[PROOFSTEP]
rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ IsConj (signAux (swap x y))
    (signAux (swap { val := 0, isLt := (_ : 0 < n + 2) } { val := 1, isLt := (_ : 1 < n + 2) }))
[PROOFSTEP]
exact (MonoidHom.mk' signAux signAux_mul).map_isConj (isConj_swap hxy (by exact of_decide_eq_true rfl))
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x y : Fin (n + 2)
hxy : x ≠ y
h2n : 2 ≤ n + 2
⊢ { val := 0, isLt := (_ : 0 < n + 2) } ≠ { val := 1, isLt := (_ : 1 < n + 2) }
[PROOFSTEP]
exact of_decide_eq_true rfl
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
[PROOFSTEP]
have : f = 1 := Equiv.ext fun y => Classical.not_not.1 (mt (h y) (List.not_mem_nil _))
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
f : Perm α
e : α ≃ Fin n
h : ∀ (x : α), ↑f x ≠ x → x ∈ []
this : f = 1
⊢ signAux ((e.symm.trans f).trans e) = signAux2 [] f
[PROOFSTEP]
rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
⊢ signAux ((e.symm.trans f).trans e) = signAux2 (x :: l) f
[PROOFSTEP]
rw [signAux2]
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
[PROOFSTEP]
by_cases hfx : x = f x
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
[PROOFSTEP]
rw [if_pos hfx]
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = signAux2 l f
[PROOFSTEP]
exact
  signAux_eq_signAux2 l f _ fun y (hy : f y ≠ y) =>
    List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy ) (h y hy)
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h✝ : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : x = ↑f x
y : α
hy : ↑f y ≠ y
h : y = x
⊢ False
[PROOFSTEP]
simp [h, hfx.symm] at hy
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
[PROOFSTEP]
have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l := fun y hy =>
  have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
  List.mem_of_ne_of_mem this.2 (h _ this.1)
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
[PROOFSTEP]
have : (e.symm.trans (swap x (f x) * f)).trans e = swap (e x) (e (f x)) * (e.symm.trans f).trans e :=
  by
  ext
  rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
  repeat (rw [trans_apply])
  simp [swap, swapCore]
  split_ifs <;> rfl
[GOAL]
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
⊢ (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
[PROOFSTEP]
ext
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑((e.symm.trans (swap x (↑f x) * f)).trans e) x✝) = ↑(↑(swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e) x✝)
[PROOFSTEP]
rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑((e.symm.trans (f.trans (swap x (↑f x)))).trans e) x✝) =
    ↑(↑(((e.symm.trans f).trans e).trans (swap (↑e x) (↑e (↑f x)))) x✝)
[PROOFSTEP]
repeat (rw [trans_apply])
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑((e.symm.trans (f.trans (swap x (↑f x)))).trans e) x✝) =
    ↑(↑(((e.symm.trans f).trans e).trans (swap (↑e x) (↑e (↑f x)))) x✝)
[PROOFSTEP]
rw [trans_apply]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(e.symm.trans (f.trans (swap x (↑f x)))) x✝)) =
    ↑(↑(((e.symm.trans f).trans e).trans (swap (↑e x) (↑e (↑f x)))) x✝)
[PROOFSTEP]
rw [trans_apply]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(f.trans (swap x (↑f x))) (↑e.symm x✝))) = ↑(↑(((e.symm.trans f).trans e).trans (swap (↑e x) (↑e (↑f x)))) x✝)
[PROOFSTEP]
rw [trans_apply]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(((e.symm.trans f).trans e).trans (swap (↑e x) (↑e (↑f x)))) x✝)
[PROOFSTEP]
rw [trans_apply]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑((e.symm.trans f).trans e) x✝))
[PROOFSTEP]
rw [trans_apply]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑(e.symm.trans f) x✝)))
[PROOFSTEP]
rw [trans_apply]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑f (↑e.symm x✝))))
[PROOFSTEP]
rw [trans_apply]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (↑(swap x (↑f x)) (↑f (↑e.symm x✝)))) = ↑(↑(swap (↑e x) (↑e (↑f x))) (↑e (↑f (↑e.symm x✝))))
[PROOFSTEP]
simp [swap, swapCore]
[GOAL]
case H.h
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
⊢ ↑(↑e (if ↑f (↑e.symm x✝) = x then ↑f x else if ↑e.symm x✝ = x then x else ↑f (↑e.symm x✝))) =
    ↑(if ↑f (↑e.symm x✝) = x then ↑e (↑f x) else if ↑e.symm x✝ = x then ↑e x else ↑e (↑f (↑e.symm x✝)))
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝ : ↑f (↑e.symm x✝) = x
⊢ ↑(↑e (↑f x)) = ↑(↑e (↑f x))
[PROOFSTEP]
rfl
[GOAL]
case pos
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝¹ : ¬↑f (↑e.symm x✝) = x
h✝ : ↑e.symm x✝ = x
⊢ ↑(↑e x) = ↑(↑e x)
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
x✝ : Fin n
h✝¹ : ¬↑f (↑e.symm x✝) = x
h✝ : ¬↑e.symm x✝ = x
⊢ ↑(↑e (↑f (↑e.symm x✝))) = ↑(↑e (↑f (↑e.symm x✝)))
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
[PROOFSTEP]
have hefx : e x ≠ e (f x) := mt e.injective.eq_iff.1 hfx
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
hefx : ↑e x ≠ ↑e (↑f x)
⊢ signAux ((e.symm.trans f).trans e) = if x = ↑f x then signAux2 l f else -signAux2 l (swap x (↑f x) * f)
[PROOFSTEP]
rw [if_neg hfx, ← signAux_eq_signAux2 _ _ e hy, this, signAux_mul, signAux_swap hefx]
[GOAL]
case neg
α : Type u
β : Type v
inst✝ : DecidableEq α
n : ℕ
x : α
l : List α
f : Perm α
e : α ≃ Fin n
h : ∀ (x_1 : α), ↑f x_1 ≠ x_1 → x_1 ∈ x :: l
hfx : ¬x = ↑f x
hy : ∀ (y : α), ↑(swap x (↑f x) * f) y ≠ y → y ∈ l
this : (e.symm.trans (swap x (↑f x) * f)).trans e = swap (↑e x) (↑e (↑f x)) * (e.symm.trans f).trans e
hefx : ↑e x ≠ ↑e (↑f x)
⊢ signAux ((e.symm.trans f).trans e) = -(-1 * signAux ((e.symm.trans f).trans e))
[PROOFSTEP]
simp only [neg_neg, one_mul, neg_mul]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
s : Multiset α
e : α ≃ Fin (Fintype.card α)
l₁ l₂ : List α
h : l₁ ≈ l₂
⊢ (∀ (x : α), x ∈ l₁) = ∀ (x : α), x ∈ l₂
[PROOFSTEP]
simp only [h.mem_iff]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
s : Multiset α
e : α ≃ Fin (Fintype.card α)
l₁ l₂ : List α
h : l₁ ≈ l₂
h₁ : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l₁
h₂ : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l₂
x✝ : HEq h₁ h₂
⊢ HEq (signAux2 l₁ f) (signAux2 l₂ f)
[PROOFSTEP]
rw [← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _, ← signAux_eq_signAux2 _ _ e fun _ _ => h₂ _]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
[PROOFSTEP]
let ⟨l, hl⟩ := Quotient.exists_rep s
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
l : List α
hl : Quotient.mk (List.isSetoid α) l = s
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
[PROOFSTEP]
let e := equivFin α
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
s : Multiset α
hs : ∀ (x : α), x ∈ s
l : List α
hl : Quotient.mk (List.isSetoid α) l = s
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
[PROOFSTEP]
subst hl
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
⊢ signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ ∀ (x y : α), x ≠ y → signAux3 (swap x y) hs = -1
[PROOFSTEP]
show signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ ∀ x y, x ≠ y → signAux2 l (swap x y) = -1
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
[PROOFSTEP]
have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e :=
  Equiv.ext fun h => by simp [mul_apply]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
h : Fin (Fintype.card α)
⊢ ↑((e.symm.trans (f * g)).trans e) h = ↑((e.symm.trans f).trans e * (e.symm.trans g).trans e) h
[PROOFSTEP]
simp [mul_apply]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g
[PROOFSTEP]
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
  signAux_eq_signAux2 _ _ e fun _ _ => hs _, hfg, signAux_mul]
[GOAL]
case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
⊢ ∀ (x y : α), x ≠ y → signAux2 l (swap x y) = -1
[PROOFSTEP]
intro x y hxy
[GOAL]
case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : x ≠ y
⊢ signAux2 l (swap x y) = -1
[PROOFSTEP]
have hexy : e x ≠ e y := mt e.injective.eq_iff.1 hxy
[GOAL]
case right
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
l : List α
e : α ≃ Fin (Fintype.card α) := Fintype.equivFin α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) l
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : x ≠ y
hexy : ↑e x ≠ ↑e y
⊢ signAux2 l (swap x y) = -1
[PROOFSTEP]
rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hexy]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ ↑sign (f.trans g) = ↑sign g * ↑sign f
[PROOFSTEP]
rw [← mul_def, sign_mul]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
⊢ ↑sign f⁻¹ = ↑sign f
[PROOFSTEP]
rw [MonoidHom.map_inv sign f, Int.units_inv_eq_self]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
H : x = y
⊢ ↑sign (swap x y) = if x = y then 1 else -1
[PROOFSTEP]
simp [H, swap_self]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
x y : α
H : ¬x = y
⊢ ↑sign (swap x y) = if x = y then 1 else -1
[PROOFSTEP]
simp [sign_swap H, H]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s : Multiset α
t : Multiset β
hs : ∀ (x : α), x ∈ s
ht : ∀ (x : β), x ∈ t
⊢ signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs
[PROOFSTEP]
induction' t, s using Quotient.inductionOn₂ with t s ht hs
[GOAL]
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
⊢ signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs
[PROOFSTEP]
show signAux2 _ _ = signAux2 _ _
[GOAL]
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f
[PROOFSTEP]
let n := equivFin β
[GOAL]
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
n : β ≃ Fin (Fintype.card β) := Fintype.equivFin β
⊢ signAux2 t ((e.symm.trans f).trans e) = signAux2 s f
[PROOFSTEP]
rw [← signAux_eq_signAux2 _ _ n fun _ _ => ht _, ← signAux_eq_signAux2 _ _ (e.trans n) fun _ _ => hs _]
[GOAL]
case h
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
n : β ≃ Fin (Fintype.card β) := Fintype.equivFin β
⊢ signAux ((n.symm.trans ((e.symm.trans f).trans e)).trans n) = signAux (((e.trans n).symm.trans f).trans (e.trans n))
[PROOFSTEP]
exact congr_arg signAux (Equiv.ext fun x => by simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply])
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
e : α ≃ β
s✝ : Multiset α
t✝ : Multiset β
hs✝ : ∀ (x : α), x ∈ s✝
ht✝ : ∀ (x : β), x ∈ t✝
t : List β
s : List α
hs : ∀ (x : α), x ∈ Quotient.mk (List.isSetoid α) s
ht : ∀ (x : β), x ∈ Quotient.mk (List.isSetoid β) t
n : β ≃ Fin (Fintype.card β) := Fintype.equivFin β
x : Fin (Fintype.card β)
⊢ ↑((n.symm.trans ((e.symm.trans f).trans e)).trans n) x = ↑(((e.trans n).symm.trans f).trans (e.trans n)) x
[PROOFSTEP]
simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply]
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ ↑sign (List.prod l) = (-1) ^ List.length l
[PROOFSTEP]
have h₁ : l.map sign = List.replicate l.length (-1) :=
  List.eq_replicate.2
    ⟨by simp, fun u hu =>
      let ⟨g, hg⟩ := List.mem_map.1 hu
      hg.2 ▸ (hl _ hg.1).sign_eq⟩
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
⊢ List.length (List.map (↑sign) l) = List.length l
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
hl : ∀ (g : Perm α), g ∈ l → IsSwap g
h₁ : List.map (↑sign) l = List.replicate (List.length l) (-1)
⊢ ↑sign (List.prod l) = (-1) ^ List.length l
[PROOFSTEP]
rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = 1
⊢ ↑sign 1 = a
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : Nontrivial α
a : ℤˣ
h : a = -1
x y : α
hxy : x ≠ y
⊢ ↑sign (swap x y) = a
[PROOFSTEP]
rw [sign_swap hxy, h]
[GOAL]
α : 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
[PROOFSTEP]
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)
[GOAL]
α : 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
[PROOFSTEP]
rw [← isConj_iff_eq, ← Or.resolve_right (Int.units_eq_one_or _) h, hab']
[GOAL]
α : 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))
[PROOFSTEP]
exact s.map_isConj (isConj_swap hab hxy)
[GOAL]
α : 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
[PROOFSTEP]
let ⟨g, hg⟩ := hs (-1)
[GOAL]
α : 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
[PROOFSTEP]
let ⟨l, hl⟩ := (truncSwapFactors g).out
[GOAL]
α : 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
[PROOFSTEP]
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)
[GOAL]
α : 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
[PROOFSTEP]
have : s l.prod = 1 := by rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
[GOAL]
α : 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
[PROOFSTEP]
rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
[GOAL]
α : 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
[PROOFSTEP]
rw [hl.1, hg] at this
[GOAL]
α : 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
[PROOFSTEP]
exact absurd this (by simp_all)
[GOAL]
α : 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
[PROOFSTEP]
simp_all
[GOAL]
α : 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
[PROOFSTEP]
let ⟨l, hl₁, hl₂⟩ := (truncSwapFactors f).out
[GOAL]
α : 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
[PROOFSTEP]
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)
[GOAL]
α : 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
[PROOFSTEP]
rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
  sign_prod_list_swap hl₂]
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
⊢ ↑sign (subtypePerm f h₁) = ↑sign f
[PROOFSTEP]
let l := (truncSwapFactors (subtypePerm f h₁)).out
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
⊢ ↑sign (subtypePerm f h₁) = ↑sign f
[PROOFSTEP]
have hl' : ∀ g' ∈ l.1.map ofSubtype, IsSwap g' := fun g' hg' =>
  let ⟨g, hg⟩ := List.mem_map.1 hg'
  hg.2 ▸ (l.2.2 _ hg.1).of_subtype_isSwap
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
⊢ ↑sign (subtypePerm f h₁) = ↑sign f
[PROOFSTEP]
have hl'₂ : (l.1.map ofSubtype).prod = f := by rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
⊢ List.prod (List.map ↑ofSubtype ↑l) = f
[PROOFSTEP]
rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
⊢ ↑sign (subtypePerm f h₁) = ↑sign f
[PROOFSTEP]
conv =>
  congr
  rw [← l.2.1]
  skip
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
| ↑sign (subtypePerm f h₁) = ↑sign f
[PROOFSTEP]
  congr
  rw [← l.2.1]
  skip
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
| ↑sign (subtypePerm f h₁) = ↑sign f
[PROOFSTEP]
  congr
  rw [← l.2.1]
  skip
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
| ↑sign (subtypePerm f h₁) = ↑sign f
[PROOFSTEP]
congr
[GOAL]
case a
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
| ↑sign (subtypePerm f h₁)
case a
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
| ↑sign f
[PROOFSTEP]
rw [← l.2.1]
[GOAL]
case a
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
| ↑sign (List.prod ↑l)
case a
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
| ↑sign f
[PROOFSTEP]
skip
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
⊢ ↑sign (List.prod ↑l) = ↑sign f
[PROOFSTEP]
simp_rw [← hl'₂]
[GOAL]
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Fintype α
f : Perm α
p : α → Prop
inst✝ : DecidablePred p
h₁ : ∀ (x : α), p x ↔ p (↑f x)
h₂ : ∀ (x : α), ↑f x ≠ x → p x
l : { l // List.prod l = subtypePerm f h₁ ∧ ∀ (g : Perm { x // p x }), g ∈ l → IsSwap g } :=
  Trunc.out (truncSwapFactors (subtypePerm f h₁))
hl' : ∀ (g' : Perm α), g' ∈ List.map ↑ofSubtype ↑l → IsSwap g'
hl'₂ : List.prod (List.map ↑ofSubtype ↑l) = f
⊢ ↑sign (List.prod ↑(Trunc.out (truncSwapFactors (subtypePerm f h₁)))) =
    ↑sign (List.prod (List.map ↑ofSubtype ↑(Trunc.out (truncSwapFactors (subtypePerm f h₁)))))
[PROOFSTEP]
rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), ↑e (↑f x) = ↑g (↑e x)
⊢ ↑sign f = ↑sign g
[PROOFSTEP]
have hg : g = (e.symm.trans f).trans e := Equiv.ext <| by simp [h]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), ↑e (↑f x) = ↑g (↑e x)
⊢ ∀ (x : β), ↑g x = ↑((e.symm.trans f).trans e) x
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
e : α ≃ β
h : ∀ (x : α), ↑e (↑f x) = ↑g (↑e x)
hg : g = (e.symm.trans f).trans e
⊢ ↑sign f = ↑sign g
[PROOFSTEP]
rw [hg, sign_symm_trans_trans]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
⊢ ∀ (x : α), ↑f x ≠ x ↔ ↑f (↑f x) ≠ ↑f x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
⊢ ∀ (x : β), ↑g x ≠ x ↔ ↑g (↑g x) ≠ ↑g x
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
x : { x // ↑f x ≠ x }
⊢ ↑g (i ↑x (_ : ↑f ↑x ≠ ↑x)) ≠ i ↑x (_ : ↑f ↑x ≠ ↑x)
[PROOFSTEP]
have : f (f x) ≠ f x := mt (fun h => f.injective h) x.2
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
x : { x // ↑f x ≠ x }
this : ↑f (↑f ↑x) ≠ ↑f ↑x
⊢ ↑g (i ↑x (_ : ↑f ↑x ≠ ↑x)) ≠ i ↑x (_ : ↑f ↑x ≠ ↑x)
[PROOFSTEP]
rw [← h _ x.2 this]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
f : Perm α
g : Perm β
i : (x : α) → ↑f x ≠ x → β
h : ∀ (x : α) (hx : ↑f x ≠ x) (hx' : ↑f (↑f x) ≠ ↑f x), i (↑f x) hx' = ↑g (i x hx)
hi : ∀ (x₁ x₂ : α) (hx₁ : ↑f x₁ ≠ x₁) (hx₂ : ↑f x₂ ≠ x₂), i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂
hg : ∀ (y : β), ↑g y ≠ y → ∃ x hx, i x hx = y
x : { x // ↑f x ≠ x }
this : ↑f (↑f ↑x) ≠ ↑f ↑x
⊢ i (↑f ↑x) this ≠ i ↑x (_ : ↑f ↑x ≠ ↑x)
[PROOFSTEP]
exact mt (hi _ _ this x.2) x.2
[GOAL]
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (a : α), a ∈ l
⊢ List.prod (List.map (fun a => prodExtendRight a (σ a)) l) = prodCongrRight σ
[PROOFSTEP]
ext ⟨a, b⟩ : 1
  -- We'll use induction on the list of elements,
    -- but we have to keep track of whether we already passed `a` in the list.
[GOAL]
case H.mk
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
⊢ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = ↑(prodCongrRight σ) (a, b)
[PROOFSTEP]
suffices
  a ∈ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, σ a b) ∨
    a ∉ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, b)
  by
  obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))
  rw [prod_eq, prodCongrRight_apply]
[GOAL]
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
⊢ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = ↑(prodCongrRight σ) (a, b)
[PROOFSTEP]
obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))
[GOAL]
case intro
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
this :
  a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
left✝ : a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b)
⊢ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = ↑(prodCongrRight σ) (a, b)
[PROOFSTEP]
rw [prod_eq, prodCongrRight_apply]
[GOAL]
case H.mk
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (a : α), a ∈ l
a : α
b : β
⊢ a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
[PROOFSTEP]
clear mem_l
[GOAL]
case H.mk
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl : List.Nodup l
a : α
b : β
⊢ a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
[PROOFSTEP]
induction' l with a' l ih
[GOAL]
case H.mk.nil
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl✝ : List.Nodup l
a : α
b : β
hl : List.Nodup []
⊢ a ∈ [] ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) [])) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ [] ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) [])) (a, b) = (a, b)
[PROOFSTEP]
refine' Or.inr ⟨List.not_mem_nil _, _⟩
[GOAL]
case H.mk.nil
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l : List α
hl✝ : List.Nodup l
a : α
b : β
hl : List.Nodup []
⊢ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) [])) (a, b) = (a, b)
[PROOFSTEP]
rw [List.map_nil, List.prod_nil, one_apply]
[GOAL]
case H.mk.cons
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
⊢ a ∈ a' :: l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) (a' :: l))) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ a' :: l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) (a' :: l))) (a, b) = (a, b)
[PROOFSTEP]
rw [List.map_cons, List.prod_cons, mul_apply]
[GOAL]
case H.mk.cons
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
⊢ a ∈ a' :: l ∧
      ↑(prodExtendRight a' (σ a')) (↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b)) =
        (a, ↑(σ a) b) ∨
    ¬a ∈ a' :: l ∧
      ↑(prodExtendRight a' (σ a')) (↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b)) = (a, b)
[PROOFSTEP]
rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨not_mem_l, prod_eq⟩)
[GOAL]
case H.mk.cons.inl.intro
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
mem_l : a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b)
⊢ a ∈ a' :: l ∧
      ↑(prodExtendRight a' (σ a')) (↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b)) =
        (a, ↑(σ a) b) ∨
    ¬a ∈ a' :: l ∧
      ↑(prodExtendRight a' (σ a')) (↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b)) = (a, b)
[PROOFSTEP]
rw [prod_eq]
[GOAL]
case H.mk.cons.inr.intro
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
not_mem_l : ¬a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
⊢ a ∈ a' :: l ∧
      ↑(prodExtendRight a' (σ a')) (↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b)) =
        (a, ↑(σ a) b) ∨
    ¬a ∈ a' :: l ∧
      ↑(prodExtendRight a' (σ a')) (↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b)) = (a, b)
[PROOFSTEP]
rw [prod_eq]
[GOAL]
case H.mk.cons.inl.intro
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
mem_l : a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b)
⊢ a ∈ a' :: l ∧ ↑(prodExtendRight a' (σ a')) (a, ↑(σ a) b) = (a, ↑(σ a) b) ∨
    ¬a ∈ a' :: l ∧ ↑(prodExtendRight a' (σ a')) (a, ↑(σ a) b) = (a, b)
[PROOFSTEP]
refine' Or.inl ⟨List.mem_cons_of_mem _ mem_l, _⟩
[GOAL]
case H.mk.cons.inl.intro
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
mem_l : a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b)
⊢ ↑(prodExtendRight a' (σ a')) (a, ↑(σ a) b) = (a, ↑(σ a) b)
[PROOFSTEP]
rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]
[GOAL]
case H.mk.cons.inr.intro
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
not_mem_l : ¬a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
⊢ a ∈ a' :: l ∧ ↑(prodExtendRight a' (σ a')) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ a' :: l ∧ ↑(prodExtendRight a' (σ a')) (a, b) = (a, b)
[PROOFSTEP]
by_cases ha' : a = a'
[GOAL]
case pos
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
not_mem_l : ¬a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
ha' : a = a'
⊢ a ∈ a' :: l ∧ ↑(prodExtendRight a' (σ a')) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ a' :: l ∧ ↑(prodExtendRight a' (σ a')) (a, b) = (a, b)
[PROOFSTEP]
rw [← ha'] at *
[GOAL]
case pos
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
not_mem_l : ¬a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
ha' : a = a
⊢ a ∈ a :: l ∧ ↑(prodExtendRight a (σ a)) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ a :: l ∧ ↑(prodExtendRight a (σ a)) (a, b) = (a, b)
[PROOFSTEP]
refine' Or.inl ⟨l.mem_cons_self a, _⟩
[GOAL]
case pos
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
not_mem_l : ¬a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
ha' : a = a
⊢ ↑(prodExtendRight a (σ a)) (a, b) = (a, ↑(σ a) b)
[PROOFSTEP]
rw [prodExtendRight_apply_eq]
[GOAL]
case neg
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
not_mem_l : ¬a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
ha' : ¬a = a'
⊢ a ∈ a' :: l ∧ ↑(prodExtendRight a' (σ a')) (a, b) = (a, ↑(σ a) b) ∨
    ¬a ∈ a' :: l ∧ ↑(prodExtendRight a' (σ a')) (a, b) = (a, b)
[PROOFSTEP]
refine' Or.inr ⟨fun h => not_or_of_not ha' not_mem_l ((List.mem_cons).mp h), _⟩
[GOAL]
case neg
α✝ : Type u
β : Type v
inst✝² : DecidableEq α✝
inst✝¹ : Fintype α✝
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
l✝ : List α
hl✝ : List.Nodup l✝
a : α
b : β
a' : α
l : List α
ih :
  List.Nodup l →
    a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, ↑(σ a) b) ∨
      ¬a ∈ l ∧ ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
hl : List.Nodup (a' :: l)
not_mem_l : ¬a ∈ l
prod_eq : ↑(List.prod (List.map (fun a => prodExtendRight a (σ a)) l)) (a, b) = (a, b)
ha' : ¬a = a'
⊢ ↑(prodExtendRight a' (σ a')) (a, b) = (a, b)
[PROOFSTEP]
rw [prodExtendRight_apply_ne _ ha']
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ : α × β
a' : α
b : β
hab : ↑(prodExtendRight a σ) (a', b) ≠ (a', b)
x✝ : ↑(prodExtendRight a σ) (↑(prodExtendRight a σ) (a', b)) ≠ ↑(prodExtendRight a σ) (a', b)
⊢ (fun ab x => ab.snd) (↑(prodExtendRight a σ) (a', b)) x✝ = ↑σ ((fun ab x => ab.snd) (a', b) hab)
[PROOFSTEP]
simp [eq_of_prodExtendRight_ne hab]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
x✝¹ x✝ : α × β
a₁ : α
b₁ : β
hab₁ : ↑(prodExtendRight a σ) (a₁, b₁) ≠ (a₁, b₁)
a₂ : α
b₂ : β
hab₂ : ↑(prodExtendRight a σ) (a₂, b₂) ≠ (a₂, b₂)
h : (fun ab x => ab.snd) (a₁, b₁) hab₁ = (fun ab x => ab.snd) (a₂, b₂) hab₂
⊢ (a₁, b₁) = (a₂, b₂)
[PROOFSTEP]
simpa [eq_of_prodExtendRight_ne hab₁, eq_of_prodExtendRight_ne hab₂] using h
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
y : β
hy : ↑σ y ≠ y
⊢ ↑(prodExtendRight a σ) (a, y) ≠ (a, y)
[PROOFSTEP]
simpa
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
a : α
σ : Perm β
y : β
hy : ↑σ y ≠ y
⊢ (fun ab x => ab.snd) (a, y) (_ : ↑(prodExtendRight a σ) (a, y) ≠ (a, y)) = y
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ↑sign (prodCongrRight σ) = ∏ k : α, ↑sign (σ k)
[PROOFSTEP]
obtain ⟨l, hl, mem_l⟩ := Finite.exists_univ_list α
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
⊢ ↑sign (prodCongrRight σ) = ∏ k : α, ↑sign (σ k)
[PROOFSTEP]
have l_to_finset : l.toFinset = Finset.univ := by
  apply eq_top_iff.mpr
  intro b _
  exact List.mem_toFinset.mpr (mem_l b)
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
⊢ List.toFinset l = univ
[PROOFSTEP]
apply eq_top_iff.mpr
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
⊢ ⊤ ≤ List.toFinset l
[PROOFSTEP]
intro b _
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
b : α
a✝ : b ∈ ⊤
⊢ b ∈ List.toFinset l
[PROOFSTEP]
exact List.mem_toFinset.mpr (mem_l b)
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
l_to_finset : List.toFinset l = univ
⊢ ↑sign (prodCongrRight σ) = ∏ k : α, ↑sign (σ k)
[PROOFSTEP]
rw [← prod_prodExtendRight σ hl mem_l, sign.map_list_prod, List.map_map, ← l_to_finset, List.prod_toFinset _ hl]
[GOAL]
case intro.intro
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
l : List α
hl : List.Nodup l
mem_l : ∀ (x : α), x ∈ l
l_to_finset : List.toFinset l = univ
⊢ List.prod (List.map (↑sign ∘ fun a => prodExtendRight a (σ a)) l) = List.prod (List.map (fun k => ↑sign (σ k)) l)
[PROOFSTEP]
simp_rw [← fun a => sign_prodExtendRight a (σ a), Function.comp]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ↑sign (prodCongrLeft σ) = ∏ k : α, ↑sign (σ k)
[PROOFSTEP]
refine' (sign_eq_sign_of_equiv _ _ (prodComm β α) _).trans (sign_prodCongrRight σ)
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α → Perm β
⊢ ∀ (x : β × α), ↑(prodComm β α) (↑(prodCongrLeft σ) x) = ↑(prodCongrRight σ) (↑(prodComm β α) x)
[PROOFSTEP]
rintro ⟨b, α⟩
[GOAL]
case mk
α✝ : Type u
β : Type v
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σ : α✝ → Perm β
b : β
α : α✝
⊢ ↑(prodComm β α✝) (↑(prodCongrLeft σ) (b, α)) = ↑(prodCongrRight σ) (↑(prodComm β α✝) (b, α))
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
e : α ≃ β
p : Perm α
⊢ ∀ (x : β), ↑e.symm (↑(↑(permCongr e) p) x) = ↑p (↑e.symm x)
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr σa σb) = ↑sign σa * ↑sign σb
[PROOFSTEP]
suffices sign (sumCongr σa (1 : Perm β)) = sign σa ∧ sign (sumCongr (1 : Perm α) σb) = sign σb by
  rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
this : ↑sign (sumCongr σa 1) = ↑sign σa ∧ ↑sign (sumCongr 1 σb) = ↑sign σb
⊢ ↑sign (sumCongr σa σb) = ↑sign σa * ↑sign σb
[PROOFSTEP]
rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
[GOAL]
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr σa 1) = ↑sign σa ∧ ↑sign (sumCongr 1 σb) = ↑sign σb
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr σa 1) = ↑sign σa
[PROOFSTEP]
refine' σa.swap_induction_on ?_ fun σa' a₁ a₂ ha ih => ?_
[GOAL]
case left.refine'_1
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 1) = ↑sign 1
[PROOFSTEP]
simp
[GOAL]
case left.refine'_2
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
σa' : Perm α
a₁ a₂ : α
ha : a₁ ≠ a₂
ih : ↑sign (sumCongr σa' 1) = ↑sign σa'
⊢ ↑sign (sumCongr (swap a₁ a₂ * σa') 1) = ↑sign (swap a₁ a₂ * σa')
[PROOFSTEP]
rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one, sign_swap ha,
  sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
[GOAL]
case right
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 σb) = ↑sign σb
[PROOFSTEP]
refine' σb.swap_induction_on ?_ fun σb' b₁ b₂ hb ih => ?_
[GOAL]
case right.refine'_1
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb : Perm β
⊢ ↑sign (sumCongr 1 1) = ↑sign 1
[PROOFSTEP]
simp
[GOAL]
case right.refine'_2
α : Type u
β : Type v
inst✝³ : DecidableEq α
inst✝² : Fintype α
inst✝¹ : DecidableEq β
inst✝ : Fintype β
σa : Perm α
σb σb' : Perm β
b₁ b₂ : β
hb : b₁ ≠ b₂
ih : ↑sign (sumCongr 1 σb') = ↑sign σb'
⊢ ↑sign (sumCongr 1 (swap b₁ b₂ * σb')) = ↑sign (swap b₁ b₂ * σb')
[PROOFSTEP]
rw [← one_mul (1 : Perm α), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_one_swap, sign_swap hb,
  sign_swap (Sum.inr_injective.ne_iff.mpr hb)]
[GOAL]
α : Type u
β : Type v
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
p : α → Prop
inst✝ : DecidablePred p
ep : Perm { a // p a }
en : Perm { a // ¬p a }
⊢ ↑sign (subtypeCongr ep en) = ↑sign ep * ↑sign en
[PROOFSTEP]
simp [subtypeCongr]
[GOAL]
α : Type u
β : Type v
inst✝⁴ : DecidableEq α
inst✝³ : Fintype α
inst✝² : DecidableEq β
inst✝¹ : Fintype β
e : Perm α
p : β → Prop
inst✝ : DecidablePred p
f : α ≃ Subtype p
⊢ ↑sign (extendDomain e f) = ↑sign e
[PROOFSTEP]
simp only [Equiv.Perm.extendDomain, sign_subtypeCongr, sign_permCongr, sign_refl, mul_one]