awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hφD :
  Finset.image
      (fun (x : (_ : Fin n) × Fin n) ↦
        Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
          (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
          (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
      D =
    D
nth_rw :
  Eq.{u_1 + 1} (α := R)
    (∏ x ∈ D,
      f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
        ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
    (∏
      x ∈
        Finset.image
          (fun (x : (_ : Fin n) × Fin n) ↦
            Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
              (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
                ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
              (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
                ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
          D,
      (↑(↑(if
                    LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
⊢ Eq.{u_1 + 1} (α := R)
    (∏ x ∈ D,
      f ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))
        ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n))))
    (∏ x ∈ D,
      (↑(↑(if
                    LT.lt (α := Fin n) ((σ⁻¹ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)) : Fin n)
                      ((σ⁻¹ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)) : Fin n) then
                  1
                else -1) :
              ℤ) :
          R) *
        f (x.snd (β := fun (i : Fin n) ↦ Fin n)) (x.fst (β := fun (i : Fin n) ↦ Fin n)))

Tactic:
nth_rw 2 [← hφD]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hφD :
  Finset.image
      (fun (x : (_ : Fin n) × Fin n) ↦
        Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
          (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
          (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
      D =
    D
x : (_ : Fin n) × Fin n
hx : x ∈ (↑D : Set ((_ : Fin n) × Fin n))
y : (_ : Fin n) × Fin n
hy : y ∈ (↑D : Set ((_ : Fin n) × Fin n))
rw rw₁ : D.card = D.card
⊢ Finset.card (α := (_ : Fin n) × Fin n)
      (Finset.image
        (fun (x : (_ : Fin n) × Fin n) ↦
          Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
            (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
            (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
              ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
        D) =
    D.card

Tactic:
rw [hφD]
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hφD :
  Finset.image
      (fun (x : (_ : Fin n) × Fin n) ↦
        Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
          (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
          (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
      D =
    D
x : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂ ∈ D
⊢ x₂ < x₁

Tactic:
simpa [hD] using hx
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
D : Finset ((_ : Fin n) × Fin n) := Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hD : D = Finset.sigma (α := fun (i : Fin n) ↦ Fin n) Finset.univ Finset.Iio
hφD :
  Finset.image
      (fun (x : (_ : Fin n) × Fin n) ↦
        Sigma.mk (β := fun (i : Fin n) ↦ Fin n)
          (max ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n))))
          (min ((σ : (a : Fin n) → Fin n) (x.fst (β := fun (i : Fin n) ↦ Fin n)))
            ((σ : (a : Fin n) → Fin n) (x.snd (β := fun (i : Fin n) ↦ Fin n)))))
      D =
    D
x : (_ : Fin n) × Fin n
x₁ x₂ : Fin n
hx : Sigma.mk (β := fun (i : Fin n) ↦ Fin n) x₁ x₂ ∈ D
⊢ x₂ < x₁

Tactic:
replace hx : x₂ < x₁ := by simpa [hD] using hx
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∏ j : Fin n, ∏ i ∈ Finset.Iio j, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j)

Tactic:
σ.prod_Iio_comp_eq_sign_mul_prod hf

Premises used: Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
h :
  Eq.{u_1 + 1} (α := R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j))
    (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j))
h₁ :
  HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j)
⊢ ∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j)

Tactic:
convert! σ.prod_Iio_comp_eq_sign_mul_prod hf using 1

Premises used: Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∀ (x y : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ x ∧ y ∈ Finset.Ioi x ↔
      x ∈ Finset.Iio y ∧ Membership.mem (γ := Finset (Fin n)) Finset.univ y

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ Eq.{u_1 + 1} (α := R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j))
    (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f ((σ : (a : Fin n) → Fin n) i) ((σ : (a : Fin n) → Fin n) j))

Tactic:
apply Finset.prod_comm' (by simp)

Premises used: Finset.prod_comm'
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
h : Eq.{u_1 + 1} (α := R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j)
⊢ HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j) =
    HMul.hMul (α := R) (↑(↑((sign : (a : Perm (Fin n)) → ℤˣ) σ) : ℤ) : R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j)

Tactic:
convert! rfl using 2

Premises used: rfl
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ ∀ (x y : Fin n),
    Membership.mem (γ := Finset (Fin n)) Finset.univ x ∧ y ∈ Finset.Iio x ↔
      x ∈ Finset.Ioi y ∧ Membership.mem (γ := Finset (Fin n)) Finset.univ y

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Fin
Goal:
n : ℕ
R : Type u_1
inst : CommRing R
σ : Perm (Fin n)
f : Fin n → Fin n → R
hf : ∀ (i j : Fin n), f i j = -f j i
⊢ Eq.{u_1 + 1} (α := R) (∏ j : Fin n, ∏ i ∈ Finset.Iio j, f i j) (∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j)

Tactic:
apply Finset.prod_comm' (by simp)

Premises used: Finset.prod_comm'
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
⊢ IsConj σ τ

Tactic:
isConj_iff.2 ⟨Equiv.extendSubtype f, ?_⟩

Premises used: Iff.mpr, isConj_iff, Equiv.extendSubtype, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
refine :
  f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ *
      (f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)))⁻¹ =
    τ
⊢ IsConj σ τ

Tactic:
refine isConj_iff.2 ⟨Equiv.extendSubtype f, ?_⟩

Premises used: Iff.mpr, isConj_iff, Equiv.extendSubtype, Exists.intro
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
rw :
  f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ =
    τ * f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α))
⊢ f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ *
      (f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)))⁻¹ =
    τ

Tactic:
rw [mul_inv_eq_iff_eq_mul]

Premises used: mul_inv_eq_iff_eq_mul
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
H :
  ∀ (x : α),
    Eq (α := α)
      ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ :
            (a : α) → α)
          x :
        α)
      ((τ * f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
            (a : α) → α)
          x :
        α)
⊢ f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ =
    τ * f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α))

Tactic:
ext x
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
H :
  Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) * σ :
          (a : α) → α)
        x :
      α)
    ((τ * f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        x :
      α)

Tactic:
simp only [Perm.mul_apply]

Premises used: Equiv.Perm.mul_apply
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
pos :
  ∀ (hx : x ∈ σ.support),
    Eq (α := α)
      ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
            (a : α) → α)
          ((σ : (a : α) → α) x : α) :
        α)
      ((τ : (a : α) → α)
          ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
                (a : α) → α)
              x :
            α) :
        α)
neg :
  ∀ (hx : x ∉ σ.support),
    Eq (α := α)
      ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
            (a : α) → α)
          ((σ : (a : α) → α) x : α) :
        α)
      ((τ : (a : α) → α)
          ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
                (a : α) → α)
              x :
            α) :
        α)
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)

Tactic:
by_cases hx : x ∈ σ.support

Premises used: Equiv.Perm.support
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
hx : x ∈ σ.support
pos :
  Eq (α := α)
    ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x ⋯)) :
          α) :
      α)
pos₁ : x ∈ (↑σ.support : Set α)
pos₂ : Membership.mem (α := α) (↑σ.support : Set α) ((σ : (a : α) → α) x : α)
⊢ Eq (α := α)
    ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
          (a : α) → α)
        ((σ : (a : α) → α) x : α) :
      α)
    ((τ : (a : α) → α)
        ((f.extendSubtype (p := Membership.mem (↑σ.support : Set α)) (q := Membership.mem (↑τ.support : Set α)) :
              (a : α) → α)
            x :
          α) :
      α)

Tactic:
rw [Equiv.extendSubtype_apply_of_mem, Equiv.extendSubtype_apply_of_mem]

Premises used: Equiv.extendSubtype_apply_of_mem
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
hx : x ∈ σ.support
⊢ Eq (α := α)
    ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x ⋯)) :
          α) :
      α)

Tactic:
hf x (Finset.mem_coe.2 hx)

Premises used: Iff.mpr, Finset.mem_coe
-- Module: Mathlib.GroupTheory.Perm.Finite
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
σ τ : Perm α
f : { x : α // x ∈ (↑σ.support : Set α) } ≃ { x : α // x ∈ (↑τ.support : Set α) }
hf :
  ∀ (x : α) (hx : x ∈ (↑σ.support : Set α)),
    Eq (α := α)
      ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
          α) :
        α)
      ((τ : (a : α) → α)
          (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
                (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x hx)) :
            α) :
        α)
x : α
hx : x ∈ σ.support
⊢ Eq (α := α)
    ((↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
            (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) ((σ : (a : α) → α) x) ⋯)) :
        α) :
      α)
    ((τ : (a : α) → α)
        (↑((f : (a : { x : α // x ∈ (↑σ.support : Set α) }) → { x : α // x ∈ (↑τ.support : Set α) })
              (Subtype.mk (p := fun (x : α) ↦ x ∈ (↑σ.support : Set α)) x ⋯)) :
          α) :
      α)

Tactic:
exact hf x (Finset.mem_coe.2 hx)

Premises used: Iff.mpr, Finset.mem_coe