awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 α
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
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw : Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) l.prod : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
Tactic: rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]
-- 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 α
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 : ℤˣ)
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw₁ : Eq (α := ℤˣ) (List.prod (List.map (⇑s : (a : Perm α) → ℤˣ) l) : ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
Tactic: rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]
-- 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 α
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 : ℤˣ)
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw₂ : Eq (α := ℤˣ) (List.prod (List.replicate (List.length (α := ℤˣ) (List.map (⇑s : (a : Perm α) → ℤˣ) l)) (-1)) : ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
Tactic: rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]
-- 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 α
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 : ℤˣ)
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw₃ : Eq (α := ℤˣ) (List.prod (List.replicate l.length (-1)) : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod : ℤˣ)
Tactic: rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]
-- 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 α
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 : ℤˣ)
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw₄ : HPow.hPow (α := ℤˣ) (-1) l.length = ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) l.prod
Tactic: rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]
-- 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 α
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
⊢ Eq (α := ℤˣ) ((s : (a : Perm α) → ℤˣ) f : ℤˣ) (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have rw₅ : HPow.hPow (α := ℤˣ) (-1) l.length = HPow.hPow (α := ℤˣ) (-1) l.length
Tactic: rw [← hl₁, ← l.prod_hom s, List.eq_replicate_length.2 hsl, List.length_map, List.prod_replicate,
      sign_prod_list_swap hl₂]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have 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
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
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
have rw : (ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (↑l : List (Perm { x : α // p x })).prod = f
Tactic: rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f
have rw₁ : (ofSubtype (p := fun (x : α) ↦ p x) : (a : Perm { x : α // p x }) → Perm α) (f.subtypePerm (p := p) h₁) = f
Tactic: rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))) =
    f
have rw₂ : f = f
Tactic: rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (hypothesis)
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
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have hl'₂ : 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₂]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
| Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have a : (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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₁) : ℤˣ)
| Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have a₁ : (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: congr
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
| (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
have a : (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (↑l : List (Perm { x : α // p x })).prod :
  ℤˣ)
Tactic: rw [← l.2.1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
| Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have a : (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (↑l : List (Perm { x : α // p x })).prod :
  ℤˣ)
Tactic: congr
    rw [← l.2.1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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 :
    ℤˣ)
| Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have a₁ : (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: congr
    rw [← l.2.1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (f.subtypePerm (p := p) h₁) : ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have conv : Eq (α := ℤˣ)
  (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (↑l : List (Perm { x : α // p x })).prod :
    ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
Tactic: conv =>
    congr
    rw [← l.2.1]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ)
        (↑l : List (Perm { x : α // p x })).prod :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ) f : ℤˣ)
have simp_rw : Eq (α := ℤˣ)
  (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ) (↑l : List (Perm { x : α // p x })).prod :
    ℤˣ)
  (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
      (List.prod
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x })))) :
    ℤˣ)
Tactic: simp_rw [← hl'₂]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ)
        (↑l : List (Perm { x : α // p x })).prod :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (List.prod
          (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
            (↑l : List (Perm { x : α // p x })))) :
      ℤˣ)
have rw : HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length =
  ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
    (List.prod
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))))
Tactic: rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Perm.Sign (goal)
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
rw :
  HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length =
    ((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
      (List.prod
        (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
          (↑l : List (Perm { x : α // p x }))))
⊢ Eq (α := ℤˣ)
    (((sign : Perm { x : α // p x } →* ℤˣ) : (a : Perm { x : α // p x }) → ℤˣ)
        (↑l : List (Perm { x : α // p x })).prod :
      ℤˣ)
    (((sign : Perm α →* ℤˣ) : (a : Perm α) → ℤˣ)
        (List.prod
          (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
            (↑l : List (Perm { x : α // p x })))) :
      ℤˣ)
have rw₁ : HPow.hPow (α := ℤˣ) (-1) (↑l : List (Perm { x : α // p x })).length =
  HPow.hPow (α := ℤˣ) (-1)
    (List.length (α := Perm α)
      (List.map (⇑(ofSubtype (p := fun (x : α) ↦ p x)) : (a : Perm { x : α // p x }) → Perm α)
        (↑l : List (Perm { x : α // p x }))))
Tactic: rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]