ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
⊢ extendSubtype f * σ * (extendSubtype f)⁻¹ = τ
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
⊢ IsConj σ τ
refine' isConj_iff.2 ⟨Equiv.extendSubtype f, _⟩
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
⊢ extendSubtype f * σ = τ * extendSubtype f
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
⊢ extendSubtype f * σ * (extendSubtype f)⁻¹ = τ
rw [mul_inv_eq_iff_eq_mul]
case H
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
⊢ ↑(extendSubtype f * σ) x = ↑(τ * extendSubtype f) x
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
⊢ extendSubtype f * σ = τ * extendSubtype f
ext x
case H
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
⊢ ↑(extendSubtype f) (↑σ x) = ↑τ (↑(extendSubtype f) x)
case H
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
⊢ ↑(extendSubtype f * σ) x = ↑(τ * extendSubtype f) x
simp only [Perm.mul_apply]
case pos
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : x ∈ support σ
⊢ ↑(extendSubtype f) (↑σ x) = ↑τ (↑(extendSubtype f) x)

case neg
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : ¬x ∈ support σ
⊢ ↑(extendSubtype f) (↑σ x) = ↑τ (↑(extendSubtype f) x)
case H
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
⊢ ↑(extendSubtype f) (↑σ x) = ↑τ (↑(extendSubtype f) x)
by_cases hx : x ∈ σ.support
case pos
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : x ∈ support σ
⊢ ↑(↑f { val := ↑σ x, property := ?pos.hx✝ }) = ↑τ ↑(↑f { val := x, property := ?pos.hx✝ })

case pos.hx
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : x ∈ support σ
⊢ x ∈ ↑(support σ)

case pos.hx
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : x ∈ support σ
⊢ ↑σ x ∈ ↑(support σ)

case pos.hx
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : x ∈ support σ
⊢ ↑σ x ∈ ↑(support σ)
case pos
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : x ∈ support σ
⊢ ↑(extendSubtype f) (↑σ x) = ↑τ (↑(extendSubtype f) x)
rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]
no goals
case pos
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : x ∈ support σ
⊢ ↑(↑f { val := ↑σ x, property := ?pos.hx✝ }) = ↑τ ↑(↑f { val := x, property := ?pos.hx✝ })
exact hf x (Finset.mem_coe.2 hx)
no goals
case neg
ι : Type ?u.3024744
α : Type u_1
β : Type ?u.3024750
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ τ : Perm α
f : { x // x ∈ ↑(support σ) } ≃ { x // x ∈ ↑(support τ) }
hf :
  ∀ (x : α) (hx : x ∈ ↑(support σ)),
    ↑(↑f { val := ↑σ x, property := (_ : ↑σ x ∈ support σ) }) = ↑τ ↑(↑f { val := x, property := hx })
x : α
hx : ¬x ∈ support σ
⊢ ↑(extendSubtype f) (↑σ x) = ↑τ (↑(extendSubtype f) x)
rwa [Classical.not_not.1 ((not_congr mem_support).1 (Equiv.extendSubtype_not_mem f _ _)),
  Classical.not_not.1 ((not_congr mem_support).mp hx)]