awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
x y : α
H : x = y
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (if x = y then 1 else -1 : ℤˣ)

Tactic:
simp [H, swap_self]

Premises used: Equiv.swap_self
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
x y : α
H : ¬x = y
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (if x = y then 1 else -1 : ℤˣ)

Tactic:
simp [sign_swap H, H]

Premises used: Equiv.Perm.sign_swap
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
h : f.IsSwap
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (-1 : ℤˣ)

Tactic:
let ⟨_, _, hxy⟩ := h
  hxy.2.symm ▸ sign_swap hxy.1

Premises used: Equiv.Perm.sign, Eq.rec, _private.0.Equiv.Perm.IsSwap.sign_eq.match_1, And.right, And.left, OfNat.ofNat, Eq.symm, Eq, DFunLike.coe, Neg.neg, Equiv.Perm.sign_swap
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
f : Perm α
e : α ≃ β
⊢ Eq (α := ℤˣ) (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) ((e.symm.trans f).trans e) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
signAux3_symm_trans_trans f e mem_univ mem_univ

Premises used: Finset.mem_univ, Equiv.Perm.signAux3_symm_trans_trans, Equiv.Perm.signAux3
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Fintype α
inst_2 : DecidableEq β
inst_3 : Fintype β
f : Perm β
e : α ≃ β
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) ((e.trans f).trans e.symm) : ℤˣ)
    (((sign : Perm β →* ℤˣ) : (a : Perm β) → ℤˣ) f : ℤˣ)

Tactic:
sign_symm_trans_trans f e.symm

Premises used: Equiv.Perm.sign_symm_trans_trans, Equiv.symm
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ List.length (α := ℤˣ) (List.map (⇑sign : (a : Perm α) → ℤˣ) l) = l.length

Tactic:
simp
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ Eq (α := List ℤˣ) (List.map (⇑sign : (a : Perm α) → ℤˣ) l) (List.replicate l.length (-1))

Tactic:
have h₁ : l.map sign = List.replicate l.length (-1) :=
    List.eq_replicate_iff.2
      ⟨by simp, fun u hu =>
        let ⟨g, hg⟩ := List.mem_map.1 hu
        hg.2 ▸ (hl _ hg.1).sign_eq⟩
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
h₁ : Eq (α := List ℤˣ) (List.map (⇑sign : (a : Perm α) → ℤˣ) l) (List.replicate l.length (-1))
rw :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (List.prod (List.replicate l.length (-1)) : ℤˣ)
rw₁ :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
    (List.prod (List.map (⇑sign : (a : Perm α) → ℤˣ) l) : ℤˣ)
rw₂ rw₃ :
  Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod = HPow.hPow (α := ℤˣ) (-1) l.length

Tactic:
rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]

Premises used: Equiv.Perm.sign, List.prod_hom, List.prod_replicate
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : Eq (α := ℤ) (↑(Int.natAbs (↑(((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f) : ℤ)) : ℤ) 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
rw₂ rw₃ : Eq (α := ℤ) 1 1
⊢ Eq (α := ℤ) |(↑(((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f) : ℤ)| 1

Tactic:
rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]

Premises used: Int.units_natAbs, Nat.cast_one, Int.abs_eq_natAbs
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : Nontrivial α
a : ℤˣ
h : a = 1
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) 1 = a

Tactic:
simp [h]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : Nontrivial α
a : ℤˣ
h : a = -1
x y : α
hxy : x ≠ y
rw : -1 = a
rw₁ rw₂ : Eq (α := ℤˣ) (-1) (-1)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x y) = a

Tactic:
rw [sign_swap hxy, h]

Premises used: Equiv.Perm.sign_swap
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f_1 : Perm α
h_1 : f_1.IsSwap
x y : α
hxy : x ≠ y
hxy' : f_1 = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
f : Perm α
h_2 : f.IsSwap
a b : α
hab : a ≠ b
hab' : f = swap a b
rw : IsConj (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ)
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)

Tactic:
rw [← isConj_iff_eq, ← Or.resolve_right (Int.units_eq_one_or _) h, hab']

Premises used: Int.units_eq_one_or, isConj_iff_eq, Or.resolve_right
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f_1 : Perm α
h_1 : f_1.IsSwap
x y : α
hxy : x ≠ y
hxy' : f_1 = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
f : Perm α
h_2 : f.IsSwap
a b : α
hab : a ≠ b
hab' : f = swap a b
⊢ IsConj (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ)

Tactic:
s.map_isConj (isConj_swap hab hxy)

Premises used: Equiv.Perm.isConj_swap, MonoidHom.map_isConj
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f_1 : Perm α
h_1 : f_1.IsSwap
x y : α
hxy : x ≠ y
hxy' : f_1 = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
f : Perm α
h_2 : f.IsSwap
a b : α
hab : a ≠ b
hab' : f = swap a b
⊢ IsConj (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ)

Tactic:
exact s.map_isConj (isConj_swap hab hxy)

Premises used: Equiv.Perm.isConj_swap, MonoidHom.map_isConj
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
⊢ ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)

Tactic:
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)
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
this : ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
let : ∀ (g : Perm α) (hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)), False
⊢ False

Tactic:
let ⟨g, hg⟩ := hs (-1)
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
this : ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
g : Perm α
hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
let : ∀ (l : List (Perm α)) (hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap), False
⊢ False

Tactic:
let ⟨l, hl⟩ := (truncSwapFactors g).out
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
this : ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
g : Perm α
hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
⊢ ∀ (a : ℤˣ), Membership.mem (γ := List ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l) a → a = 1

Tactic:
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)
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
this_1 : ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
g : Perm α
hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this : ∀ (a : ℤˣ), Membership.mem (γ := List ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l) a → a = 1
rw : Eq (α := ℤˣ) (List.prod (List.map (⇑s : (a : Perm α) → ℤˣ) l)) 1
rw₁ : Eq (α := ℤˣ) (List.prod (List.replicate (List.length (α := ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l)) 1)) 1
rw₂ : HPow.hPow (α := ℤˣ) 1 (List.length (α := ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l)) = 1
rw₃ rw₄ : Eq (α := ℤˣ) 1 1
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (1 : ℤˣ)

Tactic:
rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]

Premises used: Iff.mpr, one_pow, List.eq_replicate_length, List.prod_hom, List.prod_replicate
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
this_1 : ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
g : Perm α
hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this : ∀ (a : ℤˣ), Membership.mem (γ := List ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l) a → a = 1
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (1 : ℤˣ)

Tactic:
have : s l.prod = 1 := by
          rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
this_1 : ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
g : Perm α
hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this_2 : ∀ (a : ℤˣ), Membership.mem (γ := List ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l) a → a = 1
this : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (1 : ℤˣ)
⊢ Eq (α := ℤˣ) (-1) 1

Tactic:
rw [hl.1, hg] at this

Premises used: And.left
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
this_1 : ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
g : Perm α
hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this_2 : ∀ (a : ℤˣ), Membership.mem (γ := List ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l) a → a = 1
this : Eq (α := ℤˣ) (-1) 1
⊢ ¬Eq (α := ℤˣ) (-1) 1

Tactic:
simp_all
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
f : Perm α
h_1 : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ) (-1 : ℤˣ)
this_1 : ∀ (f : Perm α), f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
g : Perm α
hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this_2 : ∀ (a : ℤˣ), Membership.mem (γ := List ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l) a → a = 1
this : Eq (α := ℤˣ) (-1) 1
⊢ False

Tactic:
exact absurd this (by simp_all)

Premises used: absurd
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
this : ∀ {f : Perm α}, f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (-1 : ℤˣ)
f : Perm α
let :
  ∀ (l : List (Perm α)) (hl₁ : l.prod = f) (hl₂ : ∀ g ∈ l, g.IsSwap),
    Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
let ⟨l, hl₁, hl₂⟩ := (truncSwapFactors f).out
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
this : ∀ {f : Perm α}, f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (-1 : ℤˣ)
f : Perm α
l : List (Perm α)
hl₁ : l.prod = f
hl₂ : ∀ g ∈ l, g.IsSwap
⊢ ∀ (a : ℤˣ), Membership.mem (γ := List ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l) a → a = -1

Tactic:
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)
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
s : Perm α →* ℤˣ
hs : Surjective (α := Perm α) (β := ℤˣ) (⇑s : (a : Perm α) → ℤˣ)
this : ∀ {f : Perm α}, f.IsSwap → Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (-1 : ℤˣ)
f : Perm α
l : List (Perm α)
hl₁ : l.prod = f
hl₂ : ∀ g ∈ l, g.IsSwap
hsl : ∀ (a : ℤˣ), Membership.mem (γ := List ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l) a → a = -1
rw : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
rw₁ :
  Eq (α := ℤˣ) (List.prod (List.map (⇑s : (a : Perm α) → ℤˣ) l) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
rw₂ :
  Eq (α := ℤˣ) (List.prod (List.replicate (List.length (α := ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l)) (-1)) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
rw₃ :
  Eq (α := ℤˣ) (List.prod (List.replicate l.length (-1)) : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
rw₄ : HPow.hPow (α := ℤˣ) (-1) l.length = ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod
rw₅ rw₆ : HPow.hPow (α := ℤˣ) (-1) l.length = HPow.hPow (α := ℤˣ) (-1) l.length
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]

Premises used: Iff.mpr, List.eq_replicate_length, List.length_map, List.prod_hom, Equiv.Perm.sign_prod_list_swap, List.prod_replicate
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
p : α → Prop
inst_2 : DecidablePred p
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
l : { l : List (Perm { x : α // p x }) // l.prod = f.subtypePerm (p := p) h₁ ∧ ∀ g ∈ l, g.IsSwap } :=
  Trunc.out (f.subtypePerm (p := p) h₁).truncSwapFactors
⊢ ∀ (g' : Perm α),
    Membership.mem (γ := List (Perm α))
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))
        g' →
      g'.IsSwap

Tactic:
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
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
p : α → Prop
inst_2 : DecidablePred p
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
l : { l : List (Perm { x : α // p x }) // l.prod = f.subtypePerm (p := p) h₁ ∧ ∀ g ∈ l, g.IsSwap } :=
  Trunc.out (f.subtypePerm (p := p) h₁).truncSwapFactors
hl' :
  ∀ (g' : Perm α),
    Membership.mem (γ := List (Perm α))
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))
        g' →
      g'.IsSwap
rw :
  (ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (↑l : List (Perm { x : α // p x })).prod =
    f
rw₁ : (ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) = f
rw₂ rw₃ : f = f
⊢ List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f

Tactic:
rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]

Premises used: Equiv.Perm.ofSubtype_subtypePerm, And.left, Equiv.Perm.ofSubtype, List.prod_hom, Subtype.val, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
p : α → Prop
inst_2 : DecidablePred p
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
l : { l : List (Perm { x : α // p x }) // l.prod = f.subtypePerm (p := p) h₁ ∧ ∀ g ∈ l, g.IsSwap } :=
  Trunc.out (f.subtypePerm (p := p) h₁).truncSwapFactors
hl' :
  ∀ (g' : Perm α),
    Membership.mem (γ := List (Perm α))
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))
        g' →
      g'.IsSwap
⊢ List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f

Tactic:
have hl'₂ : (l.1.map ofSubtype).prod = f := by
    rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
p : α → Prop
inst_2 : DecidablePred p
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
l : { l : List (Perm { x : α // p x }) // l.prod = f.subtypePerm (p := p) h₁ ∧ ∀ g ∈ l, g.IsSwap } :=
  Trunc.out (f.subtypePerm (p := p) h₁).truncSwapFactors
hl' :
  ∀ (g' : Perm α),
    Membership.mem (γ := List (Perm α))
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))
        g' →
      g'.IsSwap
hl'₂ :
  List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f
a : (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
a₁ : (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
| Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
congr
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
p : α → Prop
inst_2 : DecidablePred p
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
l : { l : List (Perm { x : α // p x }) // l.prod = f.subtypePerm (p := p) h₁ ∧ ∀ g ∈ l, g.IsSwap } :=
  Trunc.out (f.subtypePerm (p := p) h₁).truncSwapFactors
hl' :
  ∀ (g' : Perm α),
    Membership.mem (γ := List (Perm α))
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))
        g' →
      g'.IsSwap
hl'₂ :
  List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f
a :
  (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (↑l : List (Perm { x : α // p x })).prod :
    ℤˣ)
| (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)

Tactic:
rw [← l.2.1]

Premises used: And.left, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
p : α → Prop
inst_2 : DecidablePred p
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
l : { l : List (Perm { x : α // p x }) // l.prod = f.subtypePerm (p := p) h₁ ∧ ∀ g ∈ l, g.IsSwap } :=
  Trunc.out (f.subtypePerm (p := p) h₁).truncSwapFactors
hl' :
  ∀ (g' : Perm α),
    Membership.mem (γ := List (Perm α))
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))
        g' →
      g'.IsSwap
hl'₂ :
  List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f
a :
  (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (↑l : List (Perm { x : α // p x })).prod :
    ℤˣ)
a₁ : (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
| Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
congr
    rw [← l.2.1]

Premises used: And.left, Subtype.property
-- Module: Mathlib.GroupTheory.Perm.Sign
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
p : α → Prop
inst_2 : DecidablePred p
h₁ : ∀ (x : α), p ((f : (a : α) → α) x) ↔ p x
h₂ : ∀ (x : α), (f : (a : α) → α) x ≠ x → p x
l : { l : List (Perm { x : α // p x }) // l.prod = f.subtypePerm (p := p) h₁ ∧ ∀ g ∈ l, g.IsSwap } :=
  Trunc.out (f.subtypePerm (p := p) h₁).truncSwapFactors
hl' :
  ∀ (g' : Perm α),
    Membership.mem (γ := List (Perm α))
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))
        g' →
      g'.IsSwap
hl'₂ :
  List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f
conv :
  Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ)
        (↑l : List (Perm { x : α // p x })).prod :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)

Tactic:
conv =>
    congr
    rw [← l.2.1]

Premises used: And.left, Subtype.property