awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq :
  Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
H :
  Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) = (a, b)

Tactic:
refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq :
  Eq (α := α × β)
    ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)
H H₁ : Eq (α := α × β) ((a, (σ a : (a : β) → β) b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)
⊢ Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, (σ a : (a : β) → β) b) : α × β)
    ((a, (σ a : (a : β) → β) b) : α × β)

Tactic:
rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]

Premises used: Equiv.Perm.prodExtendRight_apply_ne, Eq.rec, List.nodup_cons, And.left, Iff.mp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
pos :
  ∀ (ha' : a = a'),
    a ∈ a' :: l ∧
        Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
neg :
  ∀ (ha' : ¬a = a'),
    a ∈ a' :: l ∧
        Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
by_cases ha' : a = a'
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : a = a'
pos :
  ∀
    (ih :
      ∀ (hl : l.Nodup),
        a ∈ l ∧
            Eq (α := α × β)
              ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
              ((a, (σ a : (a : β) → β) b) : α × β) ∨
          a ∉ l ∧
            (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b))
    (hl : (a' :: l).Nodup) (notMem_l : a ∉ l)
    (prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b))
    (ha' : a = a),
    a ∈ a :: l ∧
        Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ a :: l ∧ (prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) = (a, b)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
rw [← ha'] at *
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : a = a
⊢ a ∈ a :: l ∧
      Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a :: l ∧ (prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
Or.inl ⟨l.mem_cons_self, ?_⟩

Premises used: And.intro, Or.inl, List.mem_cons_self
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : a = a
pos :
  Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)
⊢ a ∈ a :: l ∧
      Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a :: l ∧ (prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
refine Or.inl ⟨l.mem_cons_self, ?_⟩

Premises used: Or.inl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : a = a
pos pos₁ : Eq (α := α × β) ((a, (σ a : (a : β) → β) b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)
⊢ Eq (α := α × β) ((prodExtendRight a (σ a) : (a : α × β) → α × β) (a, b) : α × β) ((a, (σ a : (a : β) → β) b) : α × β)

Tactic:
rw [prodExtendRight_apply_eq]

Premises used: Equiv.Perm.prodExtendRight_apply_eq
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : ¬a = a'
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
Or.inr ⟨fun h => not_or_intro ha' notMem_l ((List.mem_cons).mp h), ?_⟩

Premises used: not_or_intro, And.intro, Iff.mp, List.mem_cons, Or.inr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : ¬a = a'
neg : (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)
⊢ a ∈ a' :: l ∧
      Eq (α := α × β) ((prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
refine Or.inr ⟨fun h => not_or_intro ha' notMem_l ((List.mem_cons).mp h), ?_⟩

Premises used: Or.inr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  ∀ (hl : l.Nodup),
    a ∈ l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
hl : (a' :: l).Nodup
notMem_l : a ∉ l
prod_eq : (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)
ha' : ¬a = a'
neg neg₁ : (a, b) = (a, b)
⊢ (prodExtendRight a' (σ a') : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
rw [prodExtendRight_apply_ne _ ha']

Premises used: Equiv.Perm.prodExtendRight_apply_ne
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
β : Type v
α : Type u_1
inst : DecidableEq α
σ : α → Perm β
l : List α
hl : l.Nodup
a : α
b : β
H :
  ∀ (hl : List.Nodup.{u_1} (α := α) []),
    Membership.mem (γ := List α) [] a ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) : α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ [] ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) []) : (a : α × β) → α × β) (a, b) = (a, b)
H₁ :
  ∀ (a' : α) (l : List α)
    (ih :
      ∀ (hl : l.Nodup),
        a ∈ l ∧
            Eq (α := α × β)
              ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
              ((a, (σ a : (a : β) → β) b) : α × β) ∨
          a ∉ l ∧
            (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b))
    (hl : (a' :: l).Nodup),
    a ∈ a' :: l ∧
        Eq (α := α × β)
          ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) (a' :: l)) : (a : α × β) → α × β) (a, b) :
            α × β)
          ((a, (σ a : (a : β) → β) b) : α × β) ∨
      a ∉ a' :: l ∧
        (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) (a' :: l)) : (a : α × β) → α × β) (a, b) = (a, b)
⊢ a ∈ l ∧
      Eq (α := α × β)
        ((List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) : α × β)
        ((a, (σ a : (a : β) → β) b) : α × β) ∨
    a ∉ l ∧ (List.prod (List.map (fun (a : α) ↦ prodExtendRight a (σ a)) l) : (a : α × β) → α × β) (a, b) = (a, b)

Tactic:
induction l with
  | nil =>
    refine Or.inr ⟨List.not_mem_nil, ?_⟩
    rw [List.map_nil, List.prod_nil, one_apply]
  | cons a' l ih =>
    rw [List.map_cons, List.prod_cons, mul_apply]
    rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨notMem_l, prod_eq⟩) <;>
      rw [prod_eq]
    · refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩
      rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]
    by_cases ha' : a = a'
    · rw [← ha'] at *
      refine Or.inl ⟨l.mem_cons_self, ?_⟩
      rw [prodExtendRight_apply_eq]
    · refine Or.inr ⟨fun h => not_or_intro ha' notMem_l ((List.mem_cons).mp h), ?_⟩
      rw [prodExtendRight_apply_ne _ ha']

Premises used: List.map_cons, Finset.cons, Equiv.Perm.prodExtendRight_apply_eq, List.prod_nil, Equiv.Perm.one_apply, Equiv.Perm.mul_apply, Or.inl, List.prod_cons, Or.inr, List.map_nil
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
a : α
σ : Perm β
x : α × β
a' : α
b : β
hab : (prodExtendRight a σ : (a : α × β) → α × β) (a', b) ≠ (a', b)
h :
  Ne (α := α × β)
    ((prodExtendRight a σ : (a : α × β) → α × β) ((prodExtendRight a σ : (a : α × β) → α × β) (a', b)) : α × β)
    ((prodExtendRight a σ : (a : α × β) → α × β) (a', b) : α × β)
⊢ Eq (α := β)
    ((fun (ab : α × β) (x : (prodExtendRight a σ : (a : α × β) → α × β) ab ≠ ab) ↦ ab.2)
        ((prodExtendRight a σ : (a : α × β) → α × β) (a', b)) h :
      β)
    ((σ : (a : β) → β)
        ((fun (ab : α × β) (x : (prodExtendRight a σ : (a : α × β) → α × β) ab ≠ ab) ↦ ab.2) (a', b) hab) :
      β)

Tactic:
simp [eq_of_prodExtendRight_ne hab]

Premises used: Equiv.Perm.eq_of_prodExtendRight_ne
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
a : α
σ : Perm β
x x_1 : α × β
a₁ : α
b₁ : β
hab₁ : (prodExtendRight a σ : (a : α × β) → α × β) (a₁, b₁) ≠ (a₁, b₁)
a₂ : α
b₂ : β
hab₂ : (prodExtendRight a σ : (a : α × β) → α × β) (a₂, b₂) ≠ (a₂, b₂)
h :
  Eq.{v + 1} (α := β)
    ((fun (ab : α × β) (x : (prodExtendRight a σ : (a : α × β) → α × β) ab ≠ ab) ↦ ab.2) (a₁, b₁) hab₁)
    ((fun (ab : α × β) (x : (prodExtendRight a σ : (a : α × β) → α × β) ab ≠ ab) ↦ ab.2) (a₂, b₂) hab₂)
⊢ (a₁, b₁) = (a₂, b₂)

Tactic:
simpa [eq_of_prodExtendRight_ne hab₁, eq_of_prodExtendRight_ne hab₂] using h

Premises used: Equiv.Perm.eq_of_prodExtendRight_ne
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
a : α
σ : Perm β
y : β
hy : (σ : (a : β) → β) y ≠ y
⊢ (prodExtendRight a σ : (a : α × β) → α × β) (a, y) ≠ (a, y)

Tactic:
simpa
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
a : α
σ : Perm β
y : β
hy : (σ : (a : β) → β) y ≠ y
⊢ (fun (ab : α × β) (x : (prodExtendRight a σ : (a : α × β) → α × β) ab ≠ ab) ↦ ab.2) (a, y) ⋯ = y

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
obtain :
  ∀ (l : List α) (hl : l.Nodup) (mem_l : ∀ (x : α), x ∈ l),
    Eq (α := ℤˣ) (((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodCongrRight σ) : ℤˣ)
      (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodCongrRight σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)

Tactic:
obtain ⟨l, hl, mem_l⟩ := Finite.exists_univ_list α

Premises used: Finite.exists_univ_list
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
apply : ⊤ ≤ l.toFinset
⊢ l.toFinset = univ

Tactic:
apply eq_top_iff.mpr

Premises used: Iff.mpr, eq_top_iff
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
b : α
_ : Membership.mem (γ := Finset α) ⊤ b → b ∈ l.toFinset
⊢ Membership.mem (γ := Finset α) ⊤ b → b ∈ l.toFinset

Tactic:
_
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
b : α
h : Membership.mem (γ := Finset α) ⊤ b
⊢ b ∈ l.toFinset

Tactic:
List.mem_toFinset.mpr (mem_l b)

Premises used: List.mem_toFinset, Iff.mpr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
b : α
h : Membership.mem (γ := Finset α) ⊤ b
⊢ b ∈ l.toFinset

Tactic:
exact List.mem_toFinset.mpr (mem_l b)

Premises used: List.mem_toFinset, Iff.mpr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
⊢ l.toFinset = univ

Tactic:
have l_to_finset : l.toFinset = Finset.univ := by
    apply eq_top_iff.mpr
    intro b _
    exact List.mem_toFinset.mpr (mem_l b)
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
l_to_finset : l.toFinset = univ
rw :
  Eq (α := ℤˣ)
    (List.prod
      (List.map (comp (β := Perm (α × β)) (⇑sign : (a : Perm (α × β)) → ℤˣ) fun (a : α) ↦ prodExtendRight a (σ a)) l))
    (List.prod (List.map (fun (k : α) ↦ ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k)) l))
⊢ Eq (α := ℤˣ) (((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodCongrRight σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)

Tactic:
rw [← prod_prodExtendRight σ hl mem_l, map_list_prod sign, List.map_map, ← l_to_finset,
    List.prod_toFinset _ hl]

Premises used: Equiv.Perm.sign, List.map_map, map_list_prod, Equiv.Perm.prod_prodExtendRight, List.prod_toFinset
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
l : List α
hl : l.Nodup
mem_l : ∀ (x : α), x ∈ l
l_to_finset : l.toFinset = univ
simp_rw :
  Eq (α := ℤˣ)
    (List.prod
      (List.map (comp (β := Perm (α × β)) (⇑sign : (a : Perm (α × β)) → ℤˣ) fun (a : α) ↦ prodExtendRight a (σ a)) l))
    (List.prod
      (List.map (fun (k : α) ↦ ((sign : Perm (α × β) →* ℤˣ) : (a : Perm (α × β)) → ℤˣ) (prodExtendRight k (σ k))) l))
⊢ Eq (α := ℤˣ)
    (List.prod
      (List.map (comp (β := Perm (α × β)) (⇑sign : (a : Perm (α × β)) → ℤˣ) fun (a : α) ↦ prodExtendRight a (σ a)) l))
    (List.prod (List.map (fun (k : α) ↦ ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k)) l))

Tactic:
simp_rw [← fun a => sign_prodExtendRight a (σ a), Function.comp_def]

Premises used: Equiv.Perm.sign_prodExtendRight, Function.comp_def
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
⊢ Eq (α := ℤˣ) (((sign : Perm (β × α) →* ℤˣ) : (a : Perm (β × α)) → ℤˣ) (prodCongrLeft σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)

Tactic:
(sign_eq_sign_of_equiv _ _ (prodComm β α) ?_).trans (sign_prodCongrRight σ)

Premises used: Equiv.prodComm, Equiv.Perm.sign_prodCongrRight, Equiv.Perm.sign_eq_sign_of_equiv, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α → Perm β
refine :
  ∀ (x : β × α),
    Eq (α := α × β) ((prodComm β α : (a : β × α) → α × β) ((prodCongrLeft σ : (a : β × α) → β × α) x) : α × β)
      ((prodCongrRight σ : (a : α × β) → α × β) ((prodComm β α : (a : β × α) → α × β) x) : α × β)
⊢ Eq (α := ℤˣ) (((sign : Perm (β × α) →* ℤˣ) : (a : Perm (β × α)) → ℤˣ) (prodCongrLeft σ) : ℤˣ)
    (∏ k : α, ((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) (σ k) : ℤˣ)

Tactic:
refine (sign_eq_sign_of_equiv _ _ (prodComm β α) ?_).trans (sign_prodCongrRight σ)

Premises used: Equiv.prodComm, Equiv.Perm.sign_prodCongrRight, Equiv.Perm.sign_eq_sign_of_equiv, Eq.trans
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α_1 : Type u
inst : DecidableEq α_1
β : Type v
inst_1 : Fintype α_1
inst_2 : DecidableEq β
inst_3 : Fintype β
σ : α_1 → Perm β
b : β
α : α_1
⊢ Eq (α := α_1 × β)
    ((prodComm β α_1 : (a : β × α_1) → α_1 × β) ((prodCongrLeft σ : (a : β × α_1) → β × α_1) (b, α)) : α_1 × β)
    ((prodCongrRight σ : (a : α_1 × β) → α_1 × β) ((prodComm β α_1 : (a : β × α_1) → α_1 × β) (b, α)) : α_1 × β)

Tactic:
rfl
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
e : α ≃ β
p : Perm α
⊢ ∀ (x : β),
    Eq.{u + 1} (α := α)
      ((e.symm : (a : β) → α) ((((e.permCongr : (a : Perm α) → Perm β) p : Perm β) : (a : β) → β) x : β) : α)
      ((p : (a : α) → α) ((e.symm : (a : β) → α) x : α) : α)

Tactic:
simp