awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
h : signAux ((e.symm.trans (f * g)).trans e) = signAux2 l f * signAux2 l g
h₁ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux2 l g
h₂ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g
have h₃ : signAux ((e.symm.trans f).trans e * (e.symm.trans g).trans e) =
  signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
h : signAux ((e.symm.trans (f * g)).trans e) = signAux2 l f * signAux2 l g
h₁ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux2 l g
h₂ : signAux ((e.symm.trans (f * g)).trans e) = signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
h₃ :
  signAux ((e.symm.trans f).trans e * (e.symm.trans g).trans e) =
    signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
⊢ signAux2 l (f * g) = signAux2 l f * signAux2 l g
have h₄ : signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e) =
  signAux ((e.symm.trans f).trans e) * signAux ((e.symm.trans g).trans e)
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦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
have hxy₁ : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) y : Fin n)
Tactic: rw [← e.injective.ne_iff] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) y : Fin n)
⊢ signAux2 l (swap x y) = -1
have h : signAux ((e.symm.trans (swap x y)).trans e) = -1
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hxy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) y : Fin n)
h : signAux ((e.symm.trans (swap x y)).trans e) = -1
⊢ signAux2 l (swap x y) = -1
have h₁ : signAux (n := n) (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) y)) = -1
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hxy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Finite α
f g : Perm α
n : ℕ
e : α ≃ Fin n
l : List α
hs : ∀ (x : α), x ∈ ⟦l⟧
hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e
x y : α
hxy : Ne (α := Fin n) ((e : (a : α) → Fin n) x : Fin n) ((e : (a : α) → Fin n) y : Fin n)
h : signAux ((e.symm.trans (swap x y)).trans e) = -1
h₁ : signAux (n := n) (swap ((e : (a : α) → Fin n) x) ((e : (a : α) → Fin n) y)) = -1
⊢ signAux2 l (swap x y) = -1
have h₂ : Eq (α := ℤˣ) (-1) (-1)
Tactic: rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hxy]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
s : Multiset α
t : Multiset β
hs : ∀ (x : α), x ∈ s
ht : ∀ (x : β), x ∈ t
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
have h : ∀ (a : List β) (b : List α) (hs : ∀ (x : α), x ∈ ⟦b⟧) (ht : ∀ (x : β), x ∈ ⟦a⟧),
  signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
Tactic: induction t, s using Quotient.inductionOn₂
Cleared hypotheses: s, t, hs, ht
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
a : List β
b : List α
hs : ∀ (x : α), x ∈ ⟦b⟧
ht : ∀ (x : β), x ∈ ⟦a⟧
⊢ signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
have h : signAux2 a ((e.symm.trans f).trans e) = signAux2 b f
Tactic: change signAux2 _ _ = signAux2 _ _
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
a : List β
b : List α
hs : ∀ (x : α), x ∈ ⟦b⟧
ht : ∀ (x : β), x ∈ ⟦a⟧
⊢ signAux2 a ((e.symm.trans f).trans e) = signAux2 b f
have h : ∀ (n : ℕ) (e' : β ≃ Fin n), signAux2 a ((e.symm.trans f).trans e) = signAux2 b f
Tactic: rcases Finite.exists_equiv_fin β with ⟨n, ⟨e'⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
β : Type v
inst_1 : Finite α
inst_2 : DecidableEq β
inst_3 : Finite β
f : Perm α
e : α ≃ β
a : List β
b : List α
hs : ∀ (x : α), x ∈ ⟦b⟧
ht : ∀ (x : β), x ∈ ⟦a⟧
n : ℕ
e' : β ≃ Fin n
⊢ signAux2 a ((e.symm.trans f).trans e) = signAux2 b f
have h : signAux ((e'.symm.trans ((e.symm.trans f).trans e)).trans e') = signAux (((e.trans e').symm.trans f).trans (e.trans e'))
Tactic: rw [← signAux_eq_signAux2 _ _ e' fun _ _ => ht _,
    ← signAux_eq_signAux2 _ _ (e.trans e') fun _ _ => hs _]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (Equiv.trans f g) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw : ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (g * f) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: rw [← mul_def, sign_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f g : Perm α
rw :
  ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (g * f) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (Equiv.trans f g) =
    HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
      (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw₁ : HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) =
  HMul.hMul (α := ℤˣ) (β := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) g : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: rw [← mul_def, sign_mul]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f⁻¹ : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw : Eq (α := ℤˣ) ((((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f)⁻¹ : ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: rw [map_inv sign f, Int.units_inv_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw :
  Eq (α := ℤˣ) ((((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f)⁻¹ : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
⊢ Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f⁻¹ : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw₁ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: rw [map_inv sign f, Int.units_inv_eq_self]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
l : List (Perm α)
hl : ∀ g ∈ l, g.IsSwap
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod = HPow.hPow (α := ℤˣ) (-1) l.length
have h₁ : 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⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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))
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod = HPow.hPow (α := ℤˣ) (-1) l.length
have rw : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (List.prod (List.replicate l.length (-1)) : ℤˣ)
Tactic: rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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)) : ℤˣ)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod = HPow.hPow (α := ℤˣ) (-1) l.length
have rw₁ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
  (List.prod (List.map (⇑sign : (a : Perm α) → ℤˣ) l) : ℤˣ)
Tactic: rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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) : ℤˣ)
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod = HPow.hPow (α := ℤˣ) (-1) l.length
have rw₂ : Eq (α := ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
Tactic: rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
⊢ Eq (α := ℤ) |(↑(((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f) : ℤ)| 1
have rw : Eq (α := ℤ) (↑(Int.natAbs (↑(((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f) : ℤ)) : ℤ) 1
Tactic: rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : Eq (α := ℤ) (↑(Int.natAbs (↑(((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f) : ℤ)) : ℤ) 1
⊢ Eq (α := ℤ) |(↑(((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f) : ℤ)| 1
have rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
Tactic: rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
f : Perm α
rw : Eq (α := ℤ) (↑(Int.natAbs (↑(((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f) : ℤ)) : ℤ) 1
rw₁ : Eq (α := ℤ) (↑1 : ℤ) 1
⊢ Eq (α := ℤ) |(↑(((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f) : ℤ)| 1
have rw₂ : Eq (α := ℤ) 1 1
Tactic: rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : Nontrivial α
a : ℤˣ
h : a = -1
x y : α
hxy : x ≠ y
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x y) = a
have rw : -1 = a
Tactic: rw [sign_swap hxy, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
Goal:
α : Type u
inst : DecidableEq α
inst_1 : Fintype α
inst_2 : Nontrivial α
a : ℤˣ
h : a = -1
x y : α
hxy : x ≠ y
rw : -1 = a
⊢ ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) (swap x y) = a
have rw₁ : Eq (α := ℤˣ) (-1) (-1)
Tactic: rw [sign_swap hxy, h]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (1 : ℤˣ)
have rw : IsConj (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap a b) : ℤˣ) ((s : (a : Perm α) → ℤˣ) (swap x y) : ℤˣ)
Tactic: rw [← isConj_iff_eq, ← Or.resolve_right (Int.units_eq_one_or _) h, hab']
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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 : ℤˣ)
⊢ False
have this : ∀ (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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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 : ℤˣ)
⊢ False
have let : ∀ (g : Perm α) (hg : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) g : ℤˣ) (-1 : ℤˣ)), False
Tactic: let ⟨g, hg⟩ := hs (-1)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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 : ℤˣ)
⊢ False
have let : ∀ (l : List (Perm α)) (hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap), False
Tactic: let ⟨l, hl⟩ := (truncSwapFactors g).out
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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
⊢ False
have this₁ : ∀ (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)
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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 : ℤˣ)
have rw : Eq (α := ℤˣ) (List.prod (List.map (⇑s : (a : Perm α) → ℤˣ) l)) 1
Tactic: rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (1 : ℤˣ)
have rw₁ : Eq (α := ℤˣ) (List.prod (List.replicate (List.length (α := ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l)) 1)) 1
Tactic: rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (1 : ℤˣ)
have rw₂ : HPow.hPow (α := ℤˣ) 1 (List.length (α := ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l)) = 1
Tactic: rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (1 : ℤˣ)
have rw₃ : Eq (α := ℤˣ) 1 1
Tactic: rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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
⊢ False
have this₁ : 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]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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 : ℤˣ)
⊢ False
have this₁ : Eq (α := ℤˣ) (-1) 1
Tactic: rw [hl.1, hg] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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 α
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have let : ∀ (l : List (Perm α)) (hl₁ : l.prod = f) (hl₂ : ∀ g ∈ l, g.IsSwap),
  Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: let ⟨l, hl₁, hl₂⟩ := (truncSwapFactors f).out
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have hsl : ∀ (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)